---

Step * 2 of Lemma prod-Leibniz-type


1. A : Type
2. B : Type
3. s1 : A ⟶ A ⟶ ℙ
4. ∀x,y:A.  ((s1 x y) ⇒ (∀z:A. ((s1 x z) ∨ (s1 y z))))
5. ∀x,y:A.  (x = y ∈ A ⇐⇒ ¬(s1 x y))
6. sep : B ⟶ B ⟶ ℙ
7. ∀x,y:B.  ((sep x y) ⇒ (∀z:B. ((sep x z) ∨ (sep y z))))
8. ∀x,y:B.  (x = y ∈ B ⇐⇒ ¬(sep x y))
9. x1 : A
10. x2 : B
11. y1 : A
12. y2 : B
⊢ <x1, x2> = <y1, y2> ∈ (A × B) ⇐⇒ ¬((s1 x1 y1) ∨ (sep x2 y2))
BY
{ Auto }

1
1. A : Type
2. B : Type
3. s1 : A ⟶ A ⟶ ℙ
4. ∀x,y:A.  ((s1 x y) ⇒ (∀z:A. ((s1 x z) ∨ (s1 y z))))
5. ∀x,y:A.  (x = y ∈ A ⇐⇒ ¬(s1 x y))
6. sep : B ⟶ B ⟶ ℙ
7. ∀x,y:B.  ((sep x y) ⇒ (∀z:B. ((sep x z) ∨ (sep y z))))
8. ∀x,y:B.  (x = y ∈ B ⇐⇒ ¬(sep x y))
9. x1 : A
10. x2 : B
11. y1 : A
12. y2 : B
13. <x1, x2> = <y1, y2> ∈ (A × B)
⊢ ¬((s1 x1 y1) ∨ (sep x2 y2))

2
1. A : Type
2. B : Type
3. s1 : A ⟶ A ⟶ ℙ
4. ∀x,y:A.  ((s1 x y) ⇒ (∀z:A. ((s1 x z) ∨ (s1 y z))))
5. ∀x,y:A.  (x = y ∈ A ⇐⇒ ¬(s1 x y))
6. sep : B ⟶ B ⟶ ℙ
7. ∀x,y:B.  ((sep x y) ⇒ (∀z:B. ((sep x z) ∨ (sep y z))))
8. ∀x,y:B.  (x = y ∈ B ⇐⇒ ¬(sep x y))
9. x1 : A
10. x2 : B
11. y1 : A
12. y2 : B
13. ¬((s1 x1 y1) ∨ (sep x2 y2))
⊢ <x1, x2> = <y1, y2> ∈ (A × B)

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  s1  :  A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}
4.  \mforall{}x,y:A.    ((s1  x  y)  {}\mRightarrow{}  (\mforall{}z:A.  ((s1  x  z)  \mvee{}  (s1  y  z))))
5.  \mforall{}x,y:A.    (x  =  y  \mLeftarrow{}{}\mRightarrow{}  \mneg{}(s1  x  y))
6.  sep  :  B  {}\mrightarrow{}  B  {}\mrightarrow{}  \mBbbP{}
7.  \mforall{}x,y:B.    ((sep  x  y)  {}\mRightarrow{}  (\mforall{}z:B.  ((sep  x  z)  \mvee{}  (sep  y  z))))
8.  \mforall{}x,y:B.    (x  =  y  \mLeftarrow{}{}\mRightarrow{}  \mneg{}(sep  x  y))
9.  x1  :  A
10.  x2  :  B
11.  y1  :  A
12.  y2  :  B
\mvdash{}  <x1,  x2>  =  <y1,  y2>  \mLeftarrow{}{}\mRightarrow{}  \mneg{}((s1  x1  y1)  \mvee{}  (sep  x2  y2))


By

---

Latex:
Auto

---

Home Index