---

Step * of Lemma l_exists-interface-predecessors

∀[Info:Type]
  ∀es:EO+(Info). ∀X:EClass(Top).  ∀[P:E(X) ⟶ ℙ]. ∀e:E. ((∃e'∈≤(X)(e). P[e']) ⇐⇒ ∃e':E(X). (e' ≤loc e  ∧ P[e']))
BY
{ WithCumulativity(((UnivCD THENA Auto) THEN RWO "l_exists_iff" 0 THEN Auto THEN ParallelLast THEN Auto)) }

1
1. [Info] : Type
2. es : EO+(Info)@i'
3. X : EClass(Top)@i'
4. [P] : E(X) ⟶ ℙ
5. e : E@i
6. e' : {a:E(X)| loc(a) = loc(e) ∈ Id} @i
7. (e' ∈ ≤(X)(e))@i
8. P[e']@i
⊢ e' ≤loc e 

2
1. [Info] : Type
2. es : EO+(Info)@i'
3. X : EClass(Top)@i'
4. [P] : E(X) ⟶ ℙ
5. e : E@i
6. e' : E(X)@i
7. e' ≤loc e @i
8. P[e']@i
⊢ (e' ∈ ≤(X)(e))

---

Latex:

---

Latex:
\mforall{}[Info:Type]
    \mforall{}es:EO+(Info).  \mforall{}X:EClass(Top).
        \mforall{}[P:E(X)  {}\mrightarrow{}  \mBbbP{}].  \mforall{}e:E.  ((\mexists{}e'\mmember{}\mleq{}(X)(e).  P[e'])  \mLeftarrow{}{}\mRightarrow{}  \mexists{}e':E(X).  (e'  \mleq{}loc  e    \mwedge{}  P[e']))


By

---

Latex:
WithCumulativity(((UnivCD  THENA  Auto)
                                    THEN  RWO  "l\_exists\_iff"  0
                                    THEN  Auto
                                    THEN  ParallelLast
                                    THEN  Auto))

---

Home Index