---

Step * 3 of Lemma es-interface-implies-decidable


1. Info : Type
2. es : EO+(Info)@i'
3. A : Type@i'
4. X : EClass(A)@i'
5. ∀e:E. Dec(∃a:A. ((↑e ∈b X) ∧ (a = X(e) ∈ A)))
6. e : E@i
7. ∃a:A. ((↑e ∈b X) ∧ (a = X(e) ∈ A))@i
⊢ ↑e ∈b X
BY
{ (ExRepD THEN Auto) }

---

Latex:



1.  Info  :  Type
2.  es  :  EO+(Info)@i'
3.  A  :  Type@i'
4.  X  :  EClass(A)@i'
5.  \mforall{}e:E.  Dec(\mexists{}a:A.  ((\muparrow{}e  \mmember{}\msubb{}  X)  \mwedge{}  (a  =  X(e))))
6.  e  :  E@i
7.  \mexists{}a:A.  ((\muparrow{}e  \mmember{}\msubb{}  X)  \mwedge{}  (a  =  X(e)))@i
\mvdash{}  \muparrow{}e  \mmember{}\msubb{}  X


By

(ExRepD  THEN  Auto)

---

Home Index