Step
*
of Lemma
equiv_rel-wf-quotient
∀[T:Type]. ∀[E1,E2:T ⟶ T ⟶ 𝔹].
  (EquivRel(T;x,y.↑E2[x;y])
  
⇒ EquivRel(T;x,y.↑E1[x;y])
  
⇒ (∀x,y:T.  ((↑E2[x;y]) 
⇒ (↑E1[x;y])))
  
⇒ (E1 ∈ (x,y:T//(↑E2[x;y])) ⟶ (x,y:T//(↑E2[x;y])) ⟶ 𝔹))
BY
{ (BasicUniformUnivCD Auto THEN RepeatFor 3 ((D 0 THENA 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]))
⊢ E1 ∈ (x,y:T//(↑E2[x;y])) ⟶ (x,y:T//(↑E2[x;y])) ⟶ 𝔹
Latex:
Latex:
\mforall{}[T:Type].  \mforall{}[E1,E2:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}].
    (EquivRel(T;x,y.\muparrow{}E2[x;y])
    {}\mRightarrow{}  EquivRel(T;x,y.\muparrow{}E1[x;y])
    {}\mRightarrow{}  (\mforall{}x,y:T.    ((\muparrow{}E2[x;y])  {}\mRightarrow{}  (\muparrow{}E1[x;y])))
    {}\mRightarrow{}  (E1  \mmember{}  (x,y:T//(\muparrow{}E2[x;y]))  {}\mrightarrow{}  (x,y:T//(\muparrow{}E2[x;y]))  {}\mrightarrow{}  \mBbbB{}))
By
Latex:
(BasicUniformUnivCD  Auto  THEN  RepeatFor  3  ((D  0  THENA  Auto)))
Home
Index