---

Step * of Lemma prob2.3

∀[U:Type]. ∀[P,Q:U ⟶ ℙ].  (((∃x:U. (P x)) ∨ (∃x:U. (Q x))) ⇒ (∃x:U. ((P x) ∨ (Q x))))
BY
{ Auto }

1
1. [U] : Type
2. [P] : U ⟶ ℙ
3. [Q] : U ⟶ ℙ
4. (∃x:U. (P x)) ∨ (∃x:U. (Q x))@i
⊢ ∃x:U. ((P x) ∨ (Q x))

---

Latex:

---

Latex:
\mforall{}[U:Type].  \mforall{}[P,Q:U  {}\mrightarrow{}  \mBbbP{}].    (((\mexists{}x:U.  (P  x))  \mvee{}  (\mexists{}x:U.  (Q  x)))  {}\mRightarrow{}  (\mexists{}x:U.  ((P  x)  \mvee{}  (Q  x))))


By

---

Latex:
Auto

---

Home Index