---

Step * 2 of Lemma pair-order


1. A : Type
2. B : Type
3. Ra : A ⟶ A ⟶ ℙ
4. Rb : B ⟶ B ⟶ ℙ
5. Refl(A;a,a'.Ra[a;a'])
6. Trans(A;a,a'.Ra[a;a'])
7. AntiSym(A;a,a'.Ra[a;a'])
8. Refl(B;b,b'.Rb[b;b'])
9. Trans(B;b,b'.Rb[b;b'])
10. AntiSym(B;b,b'.Rb[b;b'])
11. Refl(A × B;x,y.Ra[fst(x);fst(y)] ∧ ((¬((fst(x)) = (fst(y)) ∈ A)) ∨ Rb[snd(x);snd(y)]))
12. Trans(A × B;x,y.Ra[fst(x);fst(y)] ∧ ((¬((fst(x)) = (fst(y)) ∈ A)) ∨ Rb[snd(x);snd(y)]))
13. x : A × B
14. y : A × B
15. Ra[fst(x);fst(y)]
16. (¬((fst(x)) = (fst(y)) ∈ A)) ∨ Rb[snd(x);snd(y)]
17. Ra[fst(y);fst(x)]
18. (¬((fst(y)) = (fst(x)) ∈ A)) ∨ Rb[snd(y);snd(x)]
⊢ x = y ∈ (A × B)
BY
{ ((Assert (fst(x)) = (fst(y)) ∈ A BY Auto) THEN SplitOrHyps THEN Auto THEN (Assert (snd(x)) = (snd(y)) ∈ B BY Auto)) }

1
1. A : Type
2. B : Type
3. Ra : A ⟶ A ⟶ ℙ
4. Rb : B ⟶ B ⟶ ℙ
5. Refl(A;a,a'.Ra[a;a'])
6. Trans(A;a,a'.Ra[a;a'])
7. AntiSym(A;a,a'.Ra[a;a'])
8. Refl(B;b,b'.Rb[b;b'])
9. Trans(B;b,b'.Rb[b;b'])
10. AntiSym(B;b,b'.Rb[b;b'])
11. Refl(A × B;x,y.Ra[fst(x);fst(y)] ∧ ((¬((fst(x)) = (fst(y)) ∈ A)) ∨ Rb[snd(x);snd(y)]))
12. Trans(A × B;x,y.Ra[fst(x);fst(y)] ∧ ((¬((fst(x)) = (fst(y)) ∈ A)) ∨ Rb[snd(x);snd(y)]))
13. x : A × B
14. y : A × B
15. Ra[fst(x);fst(y)]
16. Rb[snd(x);snd(y)]
17. Ra[fst(y);fst(x)]
18. Rb[snd(y);snd(x)]
19. (fst(x)) = (fst(y)) ∈ A
20. (snd(x)) = (snd(y)) ∈ B
⊢ x = y ∈ (A × B)

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  Ra  :  A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}
4.  Rb  :  B  {}\mrightarrow{}  B  {}\mrightarrow{}  \mBbbP{}
5.  Refl(A;a,a'.Ra[a;a'])
6.  Trans(A;a,a'.Ra[a;a'])
7.  AntiSym(A;a,a'.Ra[a;a'])
8.  Refl(B;b,b'.Rb[b;b'])
9.  Trans(B;b,b'.Rb[b;b'])
10.  AntiSym(B;b,b'.Rb[b;b'])
11.  Refl(A  \mtimes{}  B;x,y.Ra[fst(x);fst(y)]  \mwedge{}  ((\mneg{}((fst(x))  =  (fst(y))))  \mvee{}  Rb[snd(x);snd(y)]))
12.  Trans(A  \mtimes{}  B;x,y.Ra[fst(x);fst(y)]  \mwedge{}  ((\mneg{}((fst(x))  =  (fst(y))))  \mvee{}  Rb[snd(x);snd(y)]))
13.  x  :  A  \mtimes{}  B
14.  y  :  A  \mtimes{}  B
15.  Ra[fst(x);fst(y)]
16.  (\mneg{}((fst(x))  =  (fst(y))))  \mvee{}  Rb[snd(x);snd(y)]
17.  Ra[fst(y);fst(x)]
18.  (\mneg{}((fst(y))  =  (fst(x))))  \mvee{}  Rb[snd(y);snd(x)]
\mvdash{}  x  =  y


By

---

Latex:
((Assert  (fst(x))  =  (fst(y))  BY
                Auto)
  THEN  SplitOrHyps
  THEN  Auto
  THEN  (Assert  (snd(x))  =  (snd(y))  BY
                          Auto))

---

Home Index