---

Step * 1 of Lemma prob2.3


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))
BY
{ D 4 }

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

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

---

Latex:

---

Latex:

1.  [U]  :  Type
2.  [P]  :  U  {}\mrightarrow{}  \mBbbP{}
3.  [Q]  :  U  {}\mrightarrow{}  \mBbbP{}
4.  (\mexists{}x:U.  (P  x))  \mvee{}  (\mexists{}x:U.  (Q  x))@i
\mvdash{}  \mexists{}x:U.  ((P  x)  \mvee{}  (Q  x))


By

---

Latex:
D  4

---

Home Index