---

Step * 1 1 of Lemma unique-awf

.....assertion..... 
1. [A] : Type
2. [I] : Type
3. G : ⋂T:{T:Type| ((A + (T List)) ⊆r T) ∧ (awf(A) ⊆r T)} . ((I ⟶ T) ⟶ I ⟶ (A + (T List))) ⋂ Top ⟶ I ⟶ Top@i'
4. ∃!s:I ⟶ awf(A). (s = (G s) ∈ (I ⟶ awf(A)))
⊢ G ∈ (I ⟶ awf(A)) ⟶ I ⟶ awf(A)
BY
{ (Thin (-1) THEN Isect2HD (-1)) }

1
1. [A] : Type
2. [I] : Type
3. G : ⋂T:{T:Type| ((A + (T List)) ⊆r T) ∧ (awf(A) ⊆r T)} . ((I ⟶ T) ⟶ I ⟶ (A + (T List))) ⋂ Top ⟶ I ⟶ Top@i'
4. G ∈ Top ⟶ I ⟶ Top
5. G ∈ ⋂T:{T:Type| ((A + (T List)) ⊆r T) ∧ (awf(A) ⊆r T)} . ((I ⟶ T) ⟶ I ⟶ (A + (T List)))
⊢ G ∈ (I ⟶ awf(A)) ⟶ I ⟶ awf(A)

---

Latex:

---

Latex:
.....assertion..... 
1.  [A]  :  Type
2.  [I]  :  Type
3.  G  :  \mcap{}T:\{T:Type|  ((A  +  (T  List))  \msubseteq{}r  T)  \mwedge{}  (awf(A)  \msubseteq{}r  T)\}  .  ((I  {}\mrightarrow{}  T)  {}\mrightarrow{}  I  {}\mrightarrow{}  (A  +  (T  List)))  \mcap{}  Top
{}\mrightarrow{}  I
{}\mrightarrow{}  Top@i'
4.  \mexists{}!s:I  {}\mrightarrow{}  awf(A).  (s  =  (G  s))
\mvdash{}  G  \mmember{}  (I  {}\mrightarrow{}  awf(A))  {}\mrightarrow{}  I  {}\mrightarrow{}  awf(A)


By

---

Latex:
(Thin  (-1)  THEN  Isect2HD  (-1))

---

Home Index