---

Step * 3 of Lemma equiv_rel_quotient


1. T : Type
2. E1 : T ⟶ T ⟶ 𝔹
3. E2 : T ⟶ T ⟶ 𝔹
4. EquivRel(T;x,y.↑E2[x;y])
5. EquivRel(T;x,y.↑E1[x;y])
6. ∀x,y:T.  ((↑E2[x;y]) ⇒ (↑E1[x;y]))
7. E1 ∈ (x,y:T//(↑E2[x;y])) ⟶ (x,y:T//(↑E2[x;y])) ⟶ 𝔹
8. Sym(x,y:T//(↑E2[x;y]);x,y.↑E1[x;y])
9. a : x,y:T//(↑E2[x;y])
10. b : x,y:T//(↑E2[x;y])
11. c : x,y:T//(↑E2[x;y])
12. ↑E1[a;b]
13. ↑E1[b;c]
⊢ ↑E1[a;c]
BY
{ (MoveToConcl (-1)⋅
   THEN MoveToConcl (-1)
   THEN UseWitness ⌜λx,y. Ax⌝⋅
   THEN OnVar `a' quotD
   THEN OnVar `b' quotD
   THEN OnVar `c' quotD
   THEN Auto) }

1
1. T : Type
2. E1 : T ⟶ T ⟶ 𝔹
3. E2 : T ⟶ T ⟶ 𝔹
4. EquivRel(T;x,y.↑E2[x;y])
5. EquivRel(T;x,y.↑E1[x;y])
6. ∀x,y:T.  ((↑E2[x;y]) ⇒ (↑E1[x;y]))
7. E1 ∈ (x,y:T//(↑E2[x;y])) ⟶ (x,y:T//(↑E2[x;y])) ⟶ 𝔹
8. Sym(x,y:T//(↑E2[x;y]);x,y.↑E1[x;y])
9. a : T
10. a1 : T
11. ↑E2[a;a1]
12. b : T
13. b1 : T
14. ↑E2[b;b1]
15. c : T
16. c1 : T
17. ↑E2[c;c1]
18. x : ↑E1[a;b]
19. y : ↑E1[b;c]
⊢ ↑E1[a;c]

---

Latex:

---

Latex:

1.  T  :  Type
2.  E1  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}
3.  E2  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}
4.  EquivRel(T;x,y.\muparrow{}E2[x;y])
5.  EquivRel(T;x,y.\muparrow{}E1[x;y])
6.  \mforall{}x,y:T.    ((\muparrow{}E2[x;y])  {}\mRightarrow{}  (\muparrow{}E1[x;y]))
7.  E1  \mmember{}  (x,y:T//(\muparrow{}E2[x;y]))  {}\mrightarrow{}  (x,y:T//(\muparrow{}E2[x;y]))  {}\mrightarrow{}  \mBbbB{}
8.  Sym(x,y:T//(\muparrow{}E2[x;y]);x,y.\muparrow{}E1[x;y])
9.  a  :  x,y:T//(\muparrow{}E2[x;y])
10.  b  :  x,y:T//(\muparrow{}E2[x;y])
11.  c  :  x,y:T//(\muparrow{}E2[x;y])
12.  \muparrow{}E1[a;b]
13.  \muparrow{}E1[b;c]
\mvdash{}  \muparrow{}E1[a;c]


By

---

Latex:
(MoveToConcl  (-1)\mcdot{}
  THEN  MoveToConcl  (-1)
  THEN  UseWitness  \mkleeneopen{}\mlambda{}x,y.  Ax\mkleeneclose{}\mcdot{}
  THEN  OnVar  `a'  quotD
  THEN  OnVar  `b'  quotD
  THEN  OnVar  `c'  quotD
  THEN  Auto)

---

Home Index