---

Step * of Lemma pair-order

∀[A,B:Type]. ∀[Ra:A ⟶ A ⟶ ℙ]. ∀[Rb:B ⟶ B ⟶ ℙ].
  (Order(A;a,a'.Ra[a;a'])
  ⇒ Order(B;b,b'.Rb[b;b'])
  ⇒ Order(A × B;x,y.Ra[fst(x);fst(y)] ∧ ((¬((fst(x)) = (fst(y)) ∈ A)) ∨ Rb[snd(x);snd(y)])))
BY
{ (Auto THEN All (Unfold `order`)⋅ THEN Auto THEN D 0 THEN 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. 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)]

2
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)

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[Ra:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[Rb:B  {}\mrightarrow{}  B  {}\mrightarrow{}  \mBbbP{}].
    (Order(A;a,a'.Ra[a;a'])
    {}\mRightarrow{}  Order(B;b,b'.Rb[b;b'])
    {}\mRightarrow{}  Order(A  \mtimes{}  B;x,y.Ra[fst(x);fst(y)]  \mwedge{}  ((\mneg{}((fst(x))  =  (fst(y))))  \mvee{}  Rb[snd(x);snd(y)])))


By

---

Latex:
(Auto  THEN  All  (Unfold  `order`)\mcdot{}  THEN  Auto  THEN  D  0  THEN  Auto)

---

Home Index