---

Step * 4 of Lemma mk-s-subgroup_wf


1. sg : s-Group
2. P : Point ⟶ ℙ
3. P[1]
4. ∀x:Point. (P[x] ⇒ P[x^-1])
5. ∀x,y:Point.  (P[x] ⇒ P[y] ⇒ P[(x y)])
⊢ λx,y. (x y) ∈ {f:{x:Point| P[x]}  ⟶ {x:Point| P[x]}  ⟶ {x:Point| P[x]} | 
             (∀x,y,z:{x:Point| P[x]} .  f x (f y z) ≡ f (f x y) z)
             ∧ (∀x:{x:Point| P[x]} . f x 1 ≡ x)
             ∧ (∀x:{x:Point| P[x]} . f x ((λx.x^-1) x) ≡ 1)} 
BY
{ (MemTypeCD THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

1.  sg  :  s-Group
2.  P  :  Point  {}\mrightarrow{}  \mBbbP{}
3.  P[1]
4.  \mforall{}x:Point.  (P[x]  {}\mRightarrow{}  P[x\^{}-1])
5.  \mforall{}x,y:Point.    (P[x]  {}\mRightarrow{}  P[y]  {}\mRightarrow{}  P[(x  y)])
\mvdash{}  \mlambda{}x,y.  (x  y)  \mmember{}  \{f:\{x:Point|  P[x]\}    {}\mrightarrow{}  \{x:Point|  P[x]\}    {}\mrightarrow{}  \{x:Point|  P[x]\}  | 
                          (\mforall{}x,y,z:\{x:Point|  P[x]\}  .    f  x  (f  y  z)  \mequiv{}  f  (f  x  y)  z)
                          \mwedge{}  (\mforall{}x:\{x:Point|  P[x]\}  .  f  x  1  \mequiv{}  x)
                          \mwedge{}  (\mforall{}x:\{x:Point|  P[x]\}  .  f  x  ((\mlambda{}x.x\^{}-1)  x)  \mequiv{}  1)\} 


By

---

Latex:
(MemTypeCD  THEN  Reduce  0  THEN  Auto)

---

Home Index