---

Step * 1 1 of Lemma W_iterate_functor_wf


1. A : Type
2. B : A ⟶ Type
3. F : Type ⟶ Type
4. a : A
5. f : B[a] ⟶ W(A;a.B[a])
6. ∀b:B[a]. ∀x:W(A;a.B[a]).  ((x ≤  (f b)) ⇒ (W_iterate_functor(A;a.B[a];T.F[T];x) ∈ Type))
7. x : W(A;a.B[a])
8. v : x ≤  Wsup(a;f)
9. ∀b:W(A;a.B[a]). (b <  x ∈ Type)
10. x1 : W(A;a.B[a])
11. x1 <  x
⊢ W_iterate_functor(A;a.B[a];T.F[T];x1) ∈ Type
BY
{ Assert ⌜x1 <  Wsup(a;f)⌝⋅ }

1
.....assertion..... 
1. A : Type
2. B : A ⟶ Type
3. F : Type ⟶ Type
4. a : A
5. f : B[a] ⟶ W(A;a.B[a])
6. ∀b:B[a]. ∀x:W(A;a.B[a]).  ((x ≤  (f b)) ⇒ (W_iterate_functor(A;a.B[a];T.F[T];x) ∈ Type))
7. x : W(A;a.B[a])
8. v : x ≤  Wsup(a;f)
9. ∀b:W(A;a.B[a]). (b <  x ∈ Type)
10. x1 : W(A;a.B[a])
11. x1 <  x
⊢ x1 <  Wsup(a;f)

2
1. A : Type
2. B : A ⟶ Type
3. F : Type ⟶ Type
4. a : A
5. f : B[a] ⟶ W(A;a.B[a])
6. ∀b:B[a]. ∀x:W(A;a.B[a]).  ((x ≤  (f b)) ⇒ (W_iterate_functor(A;a.B[a];T.F[T];x) ∈ Type))
7. x : W(A;a.B[a])
8. v : x ≤  Wsup(a;f)
9. ∀b:W(A;a.B[a]). (b <  x ∈ Type)
10. x1 : W(A;a.B[a])
11. x1 <  x
12. x1 <  Wsup(a;f)
⊢ W_iterate_functor(A;a.B[a];T.F[T];x1) ∈ Type

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  A  {}\mrightarrow{}  Type
3.  F  :  Type  {}\mrightarrow{}  Type
4.  a  :  A
5.  f  :  B[a]  {}\mrightarrow{}  W(A;a.B[a])
6.  \mforall{}b:B[a].  \mforall{}x:W(A;a.B[a]).    ((x  \mleq{}    (f  b))  {}\mRightarrow{}  (W\_iterate\_functor(A;a.B[a];T.F[T];x)  \mmember{}  Type))
7.  x  :  W(A;a.B[a])
8.  v  :  x  \mleq{}    Wsup(a;f)
9.  \mforall{}b:W(A;a.B[a]).  (b  <    x  \mmember{}  Type)
10.  x1  :  W(A;a.B[a])
11.  x1  <    x
\mvdash{}  W\_iterate\_functor(A;a.B[a];T.F[T];x1)  \mmember{}  Type


By

---

Latex:
Assert  \mkleeneopen{}x1  <    Wsup(a;f)\mkleeneclose{}\mcdot{}

---

Home Index