---

Step * 1 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]))
⊢ E1 ∈ (x,y:T//(↑E2[x;y])) ⟶ (x,y:T//(↑E2[x;y])) ⟶ 𝔹
BY
{ (Unhide
   THEN (ExtWith [`a'] [T ⟶ T ⟶ 𝔹]⋅ THEN Auto THEN (D (-1) THENA Auto))
   THEN ExtWith [`b'] [T ⟶ 𝔹]⋅
   THEN Auto
   THEN (quotD (-1) THENA Auto)
   THEN SqExRepD
   THEN BLemma `iff_imp_equal_bool`
   THEN Auto
   THEN All (Unfold `so_apply`)) }

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. 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 a b)
⊢ ↑(E1 a1 b1)

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

---

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]))
\mvdash{}  E1  \mmember{}  (x,y:T//(\muparrow{}E2[x;y]))  {}\mrightarrow{}  (x,y:T//(\muparrow{}E2[x;y]))  {}\mrightarrow{}  \mBbbB{}


By

---

Latex:
(Unhide
  THEN  (ExtWith  [`a']  [T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}]\mcdot{}  THEN  Auto  THEN  (D  (-1)  THENA  Auto))
  THEN  ExtWith  [`b']  [T  {}\mrightarrow{}  \mBbbB{}]\mcdot{}
  THEN  Auto
  THEN  (quotD  (-1)  THENA  Auto)
  THEN  SqExRepD
  THEN  BLemma  `iff\_imp\_equal\_bool`
  THEN  Auto
  THEN  All  (Unfold  `so\_apply`))

---

Home Index