---

Step * 3 of Lemma W-type-induction


1. A : Type
2. ∀x,y:A.  Dec(x = y ∈ A)
3. B : A ⟶ Type
4. P : W-type(A; a.B[a]) ⟶ ℙ
5. ∀a:A. ∀f:B[a] ⟶ W-type(A; a.B[a]).  ((∀b:B[a]. P[f b]) ⇒ P[W-sup(a;f)])
6. w : W-type(A; a.B[a])@i
7. alpha : ℕ ⟶ a:A ⟶ (B[a]?)@i
⊢ ↓∃n:ℕ. (↑isr(Wselect(w;map(alpha;upto(n)))))
BY
{ (Unfold `Wselect` 0 THEN D -2 THEN Fold `W-bars` 0 THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  A  :  Type
2.  \mforall{}x,y:A.    Dec(x  =  y)
3.  B  :  A  {}\mrightarrow{}  Type
4.  P  :  W-type(A;  a.B[a])  {}\mrightarrow{}  \mBbbP{}
5.  \mforall{}a:A.  \mforall{}f:B[a]  {}\mrightarrow{}  W-type(A;  a.B[a]).    ((\mforall{}b:B[a].  P[f  b])  {}\mRightarrow{}  P[W-sup(a;f)])
6.  w  :  W-type(A;  a.B[a])@i
7.  alpha  :  \mBbbN{}  {}\mrightarrow{}  a:A  {}\mrightarrow{}  (B[a]?)@i
\mvdash{}  \mdownarrow{}\mexists{}n:\mBbbN{}.  (\muparrow{}isr(Wselect(w;map(alpha;upto(n)))))


By

---

Latex:
(Unfold  `Wselect`  0  THEN  D  -2  THEN  Fold  `W-bars`  0  THEN  Auto)\mcdot{}

---

Home Index