---

Step * 1 1 of Lemma type-monotone-union-continuous


1. F : Type ⟶ Type
2. Monotone(T.F T)
3. I : Type
4. X : I ⟶ Type
5. n : I@i
6. F (X n)@i
7. %2 = %2 ∈ (F (X n))
8. x : F (X n)@i
⊢ x ∈ F ⋃n:I.(X n)
BY
{ ((DoSubsume THEN Auto)
   THEN BackThruSomeHyp'
   THEN Try ((BLemma `tunion_wf` THENA Auto))
   THEN D 0
   THEN Auto
   THEN Try ((BLemma `tunion_wf` THENA Auto)))⋅ }

1
.....subterm..... T:t
1:n
1. F : Type ⟶ Type
2. ∀[A,B:Type].  (F A) ⊆r (F B) supposing A ⊆r B
3. I : Type
4. X : I ⟶ Type
5. n : I@i
6. F (X n)@i
7. %2 = %2 ∈ (F (X n))
8. x : F (X n)@i
9. x = x ∈ (F (X n))
10. x1 : X n@i
⊢ x1 ∈ ⋃n:I.(X n)

---

Latex:

---

Latex:

1.  F  :  Type  {}\mrightarrow{}  Type
2.  Monotone(T.F  T)
3.  I  :  Type
4.  X  :  I  {}\mrightarrow{}  Type
5.  n  :  I@i
6.  F  (X  n)@i
7.  \%2  =  \%2
8.  x  :  F  (X  n)@i
\mvdash{}  x  \mmember{}  F  \mcup{}n:I.(X  n)


By

---

Latex:
((DoSubsume  THEN  Auto)
  THEN  BackThruSomeHyp'
  THEN  Try  ((BLemma  `tunion\_wf`  THENA  Auto))
  THEN  D  0
  THEN  Auto
  THEN  Try  ((BLemma  `tunion\_wf`  THENA  Auto)))\mcdot{}

---

Home Index