---

Step * of Lemma FormOr_wf2

∀[C:Type]. ∀[a,b:PZF-Formula(C)].  (a ∨ b ∈ PZF-Formula(C))
BY
{ (Auto THEN RepeatFor 2 (D 2) THEN RepeatFor 2 (D 5) THEN RepeatFor 2 ((MemTypeCD THEN Auto))) }

1
1. C : Type
2. a : Form(C)
3. ↑wfForm(a)
4. ↑SafeForm(a)
5. ¬↑termForm(a)
6. b : Form(C)
7. ↑wfForm(b)
8. ↑SafeForm(b)
9. ¬↑termForm(b)
⊢ ↑wfForm(a ∨ b)

2
1. C : Type
2. a : Form(C)
3. ↑wfForm(a)
4. ↑SafeForm(a)
5. ¬↑termForm(a)
6. b : Form(C)
7. ↑wfForm(b)
8. ↑SafeForm(b)
9. ¬↑termForm(b)
10. ↑wfForm(a ∨ b)
⊢ ↑SafeForm(a ∨ b)

---

Latex:

---

Latex:
\mforall{}[C:Type].  \mforall{}[a,b:PZF-Formula(C)].    (a  \mvee{}  b  \mmember{}  PZF-Formula(C))


By

---

Latex:
(Auto  THEN  RepeatFor  2  (D  2)  THEN  RepeatFor  2  (D  5)  THEN  RepeatFor  2  ((MemTypeCD  THEN  Auto)))

---

Home Index