---

Step * 1 2 of Lemma product-Leibniz-type


1. A : Type
2. B : A ⟶ Type
3. ∀x,y:A.  Dec(x = y ∈ A)
4. ∀a:A
     ∃sep:B[a] ⟶ B[a] ⟶ ℙ
      ((∀x,y:B[a].  ((sep x y) ⇒ (∀z:B[a]. ((sep x z) ∨ (sep y z))))) ∧ (∀x,y:B[a].  (x = y ∈ B[a] ⇐⇒ ¬(sep x y))))
5. s : a:A ⟶ B[a] ⟶ B[a] ⟶ ℙ
6. ∀a:A. ((∀x,y:B[a].  ((s a x y) ⇒ (∀z:B[a]. ((s a x z) ∨ (s a y z))))) ∧ (∀x,y:B[a].  (x = y ∈ B[a] ⇐⇒ ¬(s a x y))))
7. a : A
8. x1 : B[a]
9. a1 : A
10. y1 : B[a1]
⊢ <a, x1> = <a1, y1> ∈ (a:A × B[a]) ⇐⇒ ¬((a = a1 ∈ A) ⇒ (s a x1 y1))
BY
{ Auto }

1
1. A : Type
2. B : A ⟶ Type
3. ∀x,y:A.  Dec(x = y ∈ A)
4. ∀a:A
     ∃sep:B[a] ⟶ B[a] ⟶ ℙ
      ((∀x,y:B[a].  ((sep x y) ⇒ (∀z:B[a]. ((sep x z) ∨ (sep y z))))) ∧ (∀x,y:B[a].  (x = y ∈ B[a] ⇐⇒ ¬(sep x y))))
5. s : a:A ⟶ B[a] ⟶ B[a] ⟶ ℙ
6. ∀a:A. ((∀x,y:B[a].  ((s a x y) ⇒ (∀z:B[a]. ((s a x z) ∨ (s a y z))))) ∧ (∀x,y:B[a].  (x = y ∈ B[a] ⇐⇒ ¬(s a x y))))
7. a : A
8. x1 : B[a]
9. a1 : A
10. y1 : B[a1]
11. <a, x1> = <a1, y1> ∈ (a:A × B[a])
⊢ ¬((a = a1 ∈ A) ⇒ (s a x1 y1))

2
1. A : Type
2. B : A ⟶ Type
3. ∀x,y:A.  Dec(x = y ∈ A)
4. ∀a:A
     ∃sep:B[a] ⟶ B[a] ⟶ ℙ
      ((∀x,y:B[a].  ((sep x y) ⇒ (∀z:B[a]. ((sep x z) ∨ (sep y z))))) ∧ (∀x,y:B[a].  (x = y ∈ B[a] ⇐⇒ ¬(sep x y))))
5. s : a:A ⟶ B[a] ⟶ B[a] ⟶ ℙ
6. ∀a:A. ((∀x,y:B[a].  ((s a x y) ⇒ (∀z:B[a]. ((s a x z) ∨ (s a y z))))) ∧ (∀x,y:B[a].  (x = y ∈ B[a] ⇐⇒ ¬(s a x y))))
7. a : A
8. x1 : B[a]
9. a1 : A
10. y1 : B[a1]
11. ¬((a = a1 ∈ A) ⇒ (s a x1 y1))
⊢ <a, x1> = <a1, y1> ∈ (a:A × B[a])

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  A  {}\mrightarrow{}  Type
3.  \mforall{}x,y:A.    Dec(x  =  y)
4.  \mforall{}a:A
          \mexists{}sep:B[a]  {}\mrightarrow{}  B[a]  {}\mrightarrow{}  \mBbbP{}
            ((\mforall{}x,y:B[a].    ((sep  x  y)  {}\mRightarrow{}  (\mforall{}z:B[a].  ((sep  x  z)  \mvee{}  (sep  y  z)))))
            \mwedge{}  (\mforall{}x,y:B[a].    (x  =  y  \mLeftarrow{}{}\mRightarrow{}  \mneg{}(sep  x  y))))
5.  s  :  a:A  {}\mrightarrow{}  B[a]  {}\mrightarrow{}  B[a]  {}\mrightarrow{}  \mBbbP{}
6.  \mforall{}a:A
          ((\mforall{}x,y:B[a].    ((s  a  x  y)  {}\mRightarrow{}  (\mforall{}z:B[a].  ((s  a  x  z)  \mvee{}  (s  a  y  z)))))
          \mwedge{}  (\mforall{}x,y:B[a].    (x  =  y  \mLeftarrow{}{}\mRightarrow{}  \mneg{}(s  a  x  y))))
7.  a  :  A
8.  x1  :  B[a]
9.  a1  :  A
10.  y1  :  B[a1]
\mvdash{}  <a,  x1>  =  <a1,  y1>  \mLeftarrow{}{}\mRightarrow{}  \mneg{}((a  =  a1)  {}\mRightarrow{}  (s  a  x1  y1))


By

---

Latex:
Auto

---

Home Index