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 ((D 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