---

Step * of Lemma exists-pair

∀[A,B:Type]. ∀[P:(A × B) ⟶ ℙ].  (∃p:A × B. P[p] ⇐⇒ ∃a:A. ∃b:B. P[<a, b>])
BY
{ (Auto THEN ExRepD) }

1
1. [A] : Type
2. [B] : Type
3. [P] : (A × B) ⟶ ℙ
4. p : A × B@i
5. P[p]@i
⊢ ∃a:A. ∃b:B. P[<a, b>]

2
1. [A] : Type
2. [B] : Type
3. [P] : (A × B) ⟶ ℙ
4. a : A@i
5. b : B@i
6. P[<a, b>]@i
⊢ ∃p:A × B. P[p]

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[P:(A  \mtimes{}  B)  {}\mrightarrow{}  \mBbbP{}].    (\mexists{}p:A  \mtimes{}  B.  P[p]  \mLeftarrow{}{}\mRightarrow{}  \mexists{}a:A.  \mexists{}b:B.  P[<a,  b>])


By

---

Latex:
(Auto  THEN  ExRepD)

---

Home Index