---

Step * of Lemma WtoSet_wf

∀[A:Type]. ∀[B:A ⟶ Type]. ∀[x:W(A;a.B[a])].  (WtoSet(a.B[a];x) ∈ Set{i:l})
BY
{ (Auto THEN WElim (-1)) }

1
1. A : Type
2. B : A ⟶ Type
3. a : A
4. f : B[a] ⟶ W(A;a.B[a])
5. ∀b:B[a]. (WtoSet(a.B[a];f b) ∈ Set{i:l})
⊢ WtoSet(a.B[a];Wsup(a;f)) ∈ Set{i:l}

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[x:W(A;a.B[a])].    (WtoSet(a.B[a];x)  \mmember{}  Set\{i:l\})


By

---

Latex:
(Auto  THEN  WElim  (-1))

---

Home Index