---

Step * 3 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.x^-1 ∈ {x:Point| P[x]}  ⟶ {x:Point| P[x]} 
BY
{ 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.x\^{}-1  \mmember{}  \{x:Point|  P[x]\}    {}\mrightarrow{}  \{x:Point|  P[x]\} 


By

---

Latex:
Auto

---

Home Index