---

Step * 1 1 2 2 of Lemma inj_into_ocmon


1. g : GrpSig
2. h : OCMon
3. Assoc(|h|;*)
4. Ident(|h|;*;e)
5. Comm(|h|;*)
6. UniformlyRefl(|h|;x,y.↑(x ≤b y))
7. UniformlyTrans(|h|;x,y.↑(x ≤b y))
8. UniformlyAntiSym(|h|;x,y.↑(x ≤b y))
9. Connex(|h|;x,y.↑(x ≤b y))
10. Cancel(|h|;|h|;*)
11. ∀[z:|h|]. monot(|h|;x,y.↑(x ≤b y);λw.(z * w))
12. f : |g| ⟶ |h|
13. FunThru2op(|g|;|h|;*;*;f)
14. (f e) = e ∈ |h|
15. Inj(|g|;|h|;f)
16. RelsIso(|g|;|h|;x,y.↑(x =b y);x,y.↑(x =b y);f)
17. RelsIso(|g|;|h|;x,y.↑(x ≤b y);x,y.↑(x ≤b y);f)
18. UniformLinorder(|g|;x,y.↑(x ≤b y))
⊢ =b = (λx,y. ((x ≤b y) ∧b (y ≤b x))) ∈ (|g| ⟶ |g| ⟶ 𝔹)
BY
{ (RepeatFor 2 ((Ext THEN Auto)) THEN Reduce 0 THEN (BLemma `iff_imp_equal_bool` THENA Auto) THEN Fold `infix_ap` 0) }

1
1. g : GrpSig
2. h : OCMon
3. Assoc(|h|;*)
4. Ident(|h|;*;e)
5. Comm(|h|;*)
6. UniformlyRefl(|h|;x,y.↑(x ≤b y))
7. UniformlyTrans(|h|;x,y.↑(x ≤b y))
8. UniformlyAntiSym(|h|;x,y.↑(x ≤b y))
9. Connex(|h|;x,y.↑(x ≤b y))
10. Cancel(|h|;|h|;*)
11. ∀[z:|h|]. monot(|h|;x,y.↑(x ≤b y);λw.(z * w))
12. f : |g| ⟶ |h|
13. FunThru2op(|g|;|h|;*;*;f)
14. (f e) = e ∈ |h|
15. Inj(|g|;|h|;f)
16. RelsIso(|g|;|h|;x,y.↑(x =b y);x,y.↑(x =b y);f)
17. RelsIso(|g|;|h|;x,y.↑(x ≤b y);x,y.↑(x ≤b y);f)
18. UniformLinorder(|g|;x,y.↑(x ≤b y))
19. x : |g|
20. x1 : |g|
⊢ ↑(x =b x1) ⇐⇒ ↑((x ≤b x1) ∧b (x1 ≤b x))

---

Latex:

---

Latex:

1.  g  :  GrpSig
2.  h  :  OCMon
3.  Assoc(|h|;*)
4.  Ident(|h|;*;e)
5.  Comm(|h|;*)
6.  UniformlyRefl(|h|;x,y.\muparrow{}(x  \mleq{}\msubb{}  y))
7.  UniformlyTrans(|h|;x,y.\muparrow{}(x  \mleq{}\msubb{}  y))
8.  UniformlyAntiSym(|h|;x,y.\muparrow{}(x  \mleq{}\msubb{}  y))
9.  Connex(|h|;x,y.\muparrow{}(x  \mleq{}\msubb{}  y))
10.  Cancel(|h|;|h|;*)
11.  \mforall{}[z:|h|].  monot(|h|;x,y.\muparrow{}(x  \mleq{}\msubb{}  y);\mlambda{}w.(z  *  w))
12.  f  :  |g|  {}\mrightarrow{}  |h|
13.  FunThru2op(|g|;|h|;*;*;f)
14.  (f  e)  =  e
15.  Inj(|g|;|h|;f)
16.  RelsIso(|g|;|h|;x,y.\muparrow{}(x  =\msubb{}  y);x,y.\muparrow{}(x  =\msubb{}  y);f)
17.  RelsIso(|g|;|h|;x,y.\muparrow{}(x  \mleq{}\msubb{}  y);x,y.\muparrow{}(x  \mleq{}\msubb{}  y);f)
18.  UniformLinorder(|g|;x,y.\muparrow{}(x  \mleq{}\msubb{}  y))
\mvdash{}  =\msubb{}  =  (\mlambda{}x,y.  ((x  \mleq{}\msubb{}  y)  \mwedge{}\msubb{}  (y  \mleq{}\msubb{}  x)))


By

---

Latex:
(RepeatFor  2  ((Ext  THEN  Auto))
  THEN  Reduce  0
  THEN  (BLemma  `iff\_imp\_equal\_bool`  THENA  Auto)
  THEN  Fold  `infix\_ap`  0)

---

Home Index