---

Step * 1 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. a : A × B
13. b : A × B
14. c : A × B
15. Ra[fst(a);fst(b)]
16. (¬((fst(a)) = (fst(b)) ∈ A)) ∨ Rb[snd(a);snd(b)]
17. Ra[fst(b);fst(c)]
18. (¬((fst(b)) = (fst(c)) ∈ A)) ∨ Rb[snd(b);snd(c)]
19. Ra[fst(a);fst(c)]
⊢ (¬((fst(a)) = (fst(c)) ∈ A)) ∨ Rb[snd(a);snd(c)]
BY
{ (SplitOrHyps THEN Auto) }

---

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.  a  :  A  \mtimes{}  B
13.  b  :  A  \mtimes{}  B
14.  c  :  A  \mtimes{}  B
15.  Ra[fst(a);fst(b)]
16.  (\mneg{}((fst(a))  =  (fst(b))))  \mvee{}  Rb[snd(a);snd(b)]
17.  Ra[fst(b);fst(c)]
18.  (\mneg{}((fst(b))  =  (fst(c))))  \mvee{}  Rb[snd(b);snd(c)]
19.  Ra[fst(a);fst(c)]
\mvdash{}  (\mneg{}((fst(a))  =  (fst(c))))  \mvee{}  Rb[snd(a);snd(c)]


By

---

Latex:
(SplitOrHyps  THEN  Auto)

---

Home Index