---

Step * of Lemma inj_into_ocmon

∀[g:GrpSig]
  g ∈ OCMon 
  supposing ∃h:OCMon
             ∃f:|g| ⟶ |h|
              (IsMonHomInj(g;h;f)
              ∧ RelsIso(|g|;|h|;x,y.↑(x =b y);x,y.↑(x =b y);f)
              ∧ RelsIso(|g|;|h|;x,y.↑(x ≤b y);x,y.↑(x ≤b y);f))
BY
{ ((GenExRepD) THENA Auto) }

1
1. g : GrpSig
2. h : OCMon
3. f : |g| ⟶ |h|
4. IsMonHomInj(g;h;f)
5. RelsIso(|g|;|h|;x,y.↑(x =b y);x,y.↑(x =b y);f)
6. RelsIso(|g|;|h|;x,y.↑(x ≤b y);x,y.↑(x ≤b y);f)
⊢ g ∈ OCMon

---

Latex:

---

Latex:
\mforall{}[g:GrpSig]
    g  \mmember{}  OCMon 
    supposing  \mexists{}h:OCMon
                          \mexists{}f:|g|  {}\mrightarrow{}  |h|
                            (IsMonHomInj(g;h;f)
                            \mwedge{}  RelsIso(|g|;|h|;x,y.\muparrow{}(x  =\msubb{}  y);x,y.\muparrow{}(x  =\msubb{}  y);f)
                            \mwedge{}  RelsIso(|g|;|h|;x,y.\muparrow{}(x  \mleq{}\msubb{}  y);x,y.\muparrow{}(x  \mleq{}\msubb{}  y);f))


By

---

Latex:
((GenExRepD)  THENA  Auto)

---

Home Index