---

Step * 2 2 of Lemma first-eclass-val


1. [Info] : Type
2. [A] : Type
3. u : EClass(A)@i'
4. v : EClass(A) List@i'
5. ∀es:EO+(Info). ∀e:E.  (∃X∈v. (↑e ∈b X) ∧ (first-eclass(v)(e) = X(e) ∈ A)) supposing ↑e ∈b first-eclass(v)@i'
6. es : EO+(Info)@i'
7. e : E@i
8. ↑e ∈b first-eclass([u / v])
9. (↑e ∈b u) ∨ (∃X∈v. ↑e ∈b X)
10. ¬↑e ∈b u
⊢ (∃X∈[u / v]. (↑e ∈b X) ∧ (first-eclass([u / v])(e) = X(e) ∈ A))
BY
{ ((D (-2) THEN Auto) THEN (InstHyp [⌈es⌉;⌈e⌉] 5⋅ THENA (Auto THEN (RWW "in-first-eclass" 0 THEN Auto)⋅))) }

1
1. [Info] : Type
2. [A] : Type
3. u : EClass(A)@i'
4. v : EClass(A) List@i'
5. ∀es:EO+(Info). ∀e:E.  (∃X∈v. (↑e ∈b X) ∧ (first-eclass(v)(e) = X(e) ∈ A)) supposing ↑e ∈b first-eclass(v)@i'
6. es : EO+(Info)@i'
7. e : E@i
8. ↑e ∈b first-eclass([u / v])
9. (∃X∈v. ↑e ∈b X)
10. ¬↑e ∈b u
11. (∃X∈v. (↑e ∈b X) ∧ (first-eclass(v)(e) = X(e) ∈ A))
⊢ (∃X∈[u / v]. (↑e ∈b X) ∧ (first-eclass([u / v])(e) = X(e) ∈ A))

---

Latex:

---

Latex:

1.  [Info]  :  Type
2.  [A]  :  Type
3.  u  :  EClass(A)@i'
4.  v  :  EClass(A)  List@i'
5.  \mforall{}es:EO+(Info).  \mforall{}e:E.
          (\mexists{}X\mmember{}v.  (\muparrow{}e  \mmember{}\msubb{}  X)  \mwedge{}  (first-eclass(v)(e)  =  X(e)))  supposing  \muparrow{}e  \mmember{}\msubb{}  first-eclass(v)@i'
6.  es  :  EO+(Info)@i'
7.  e  :  E@i
8.  \muparrow{}e  \mmember{}\msubb{}  first-eclass([u  /  v])
9.  (\muparrow{}e  \mmember{}\msubb{}  u)  \mvee{}  (\mexists{}X\mmember{}v.  \muparrow{}e  \mmember{}\msubb{}  X)
10.  \mneg{}\muparrow{}e  \mmember{}\msubb{}  u
\mvdash{}  (\mexists{}X\mmember{}[u  /  v].  (\muparrow{}e  \mmember{}\msubb{}  X)  \mwedge{}  (first-eclass([u  /  v])(e)  =  X(e)))


By

---

Latex:
((D  (-2)  THEN  Auto)
  THEN  (InstHyp  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]  5\mcdot{}  THENA  (Auto  THEN  (RWW  "in-first-eclass"  0  THEN  Auto)\mcdot{}))
  )

---

Home Index