---

Step * of Lemma altW-item_wf

∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w:altW(A;a.B[a])]. ∀[b:coW-dom(a.B[a];w)].  (altW-item(w;b) ∈ altW(A;a.B[a]))
BY
{ (Auto THEN D -2 THEN MemTypeCD THEN Auto) }

1
1. A : 𝕌'
2. B : A ⟶ Type
3. w : coW(A;a.B[a])
4. coW-wfdd(a.B[a];w)
5. b : coW-dom(a.B[a];w)
⊢ altW-item(w;b) ∈ coW(A;a.B[a])

2
.....set predicate..... 
1. A : 𝕌'
2. B : A ⟶ Type
3. w : coW(A;a.B[a])
4. coW-wfdd(a.B[a];w)
5. b : coW-dom(a.B[a];w)
⊢ coW-wfdd(a.B[a];altW-item(w;b))

---

Latex:

---

Latex:
\mforall{}[A:\mBbbU{}'].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[w:altW(A;a.B[a])].  \mforall{}[b:coW-dom(a.B[a];w)].
    (altW-item(w;b)  \mmember{}  altW(A;a.B[a]))


By

---

Latex:
(Auto  THEN  D  -2  THEN  MemTypeCD  THEN  Auto)

---

Home Index