---

Step * 1 2 of Lemma equiv_rel-wf-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. a : Base
8. a1 : Base
9. a = a1 ∈ pertype(λx,y. ((x ∈ T) ∧ (y ∈ T) ∧ (↑(E2 x y))))
10. a ∈ T
11. a1 ∈ T
12. ↑(E2 a a1)
13. b : T
14. b1 : T
15. ↑(E2 b b1)
16. ↑(E1 a1 b1)
⊢ ↑(E1 a b)
BY
{ UseTrans ⌜a1⌝⋅ }

---

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.  a  :  Base
8.  a1  :  Base
9.  a  =  a1
10.  a  \mmember{}  T
11.  a1  \mmember{}  T
12.  \muparrow{}(E2  a  a1)
13.  b  :  T
14.  b1  :  T
15.  \muparrow{}(E2  b  b1)
16.  \muparrow{}(E1  a1  b1)
\mvdash{}  \muparrow{}(E1  a  b)


By

---

Latex:
UseTrans  \mkleeneopen{}a1\mkleeneclose{}\mcdot{}

---

Home Index