---

Step * 1 1 1 1 of Lemma unique-awf


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)))
6. awf(A) ⊆r (A + (awf(A) List))
7. (A + (awf(A) List)) ⊆r awf(A)
⊢ G ∈ (I ⟶ awf(A)) ⟶ I ⟶ awf(A)
BY
{ (IsectHD ⌜awf(A)⌝ (-3)⋅ THEN Auto) }

---

Latex:

---

Latex:

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.  G  \mmember{}  Top  {}\mrightarrow{}  I  {}\mrightarrow{}  Top
5.  G  \mmember{}  \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)))
6.  awf(A)  \msubseteq{}r  (A  +  (awf(A)  List))
7.  (A  +  (awf(A)  List))  \msubseteq{}r  awf(A)
\mvdash{}  G  \mmember{}  (I  {}\mrightarrow{}  awf(A))  {}\mrightarrow{}  I  {}\mrightarrow{}  awf(A)


By

---

Latex:
(IsectHD  \mkleeneopen{}awf(A)\mkleeneclose{}  (-3)\mcdot{}  THEN  Auto)

---

Home Index