df-slw

Description: Define the set of Sylow p-subgroups of a group g . A Sylow p-subgroup is a p-group that is not a subgroup of any other p-groups in g . (Contributed by Mario Carneiro, 16-Jan-2015)

		Ref	Expression
	Assertion	df-slw	$⊢ pSyl = (p \in ℙ, g \in Grp ⟼ \{h \in SubGrp (g) \| \forall k \in SubGrp (g) ((h \subseteq k \land p pGrp (g ↾_{𝑠} k)) \leftrightarrow h = k)\})$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cslw	$class pSyl$
1		vp	$setvar p$
2		cprime	$class ℙ$
3		vg	$setvar g$
4		cgrp	$class Grp$
5		vh	$setvar h$
6		csubg	$class SubGrp$
7	3	cv	$setvar g$
8	7 6	cfv	$class SubGrp (g)$
9		vk	$setvar k$
10	5	cv	$setvar h$
11	9	cv	$setvar k$
12	10 11	wss	$wff h \subseteq k$
13	1	cv	$setvar p$
14		cpgp	$class pGrp$
15		cress	$class ↾_{𝑠}$
16	7 11 15	co	$class (g ↾_{𝑠} k)$
17	13 16 14	wbr	$wff p pGrp (g ↾_{𝑠} k)$
18	12 17	wa	$wff (h \subseteq k \land p pGrp (g ↾_{𝑠} k))$
19	10 11	wceq	$wff h = k$
20	18 19	wb	$wff ((h \subseteq k \land p pGrp (g ↾_{𝑠} k)) \leftrightarrow h = k)$
21	20 9 8	wral	$wff \forall k \in SubGrp (g) ((h \subseteq k \land p pGrp (g ↾_{𝑠} k)) \leftrightarrow h = k)$
22	21 5 8	crab	$class \{h \in SubGrp (g) \| \forall k \in SubGrp (g) ((h \subseteq k \land p pGrp (g ↾_{𝑠} k)) \leftrightarrow h = k)\}$
23	1 3 2 4 22	cmpo	$class (p \in ℙ, g \in Grp ⟼ \{h \in SubGrp (g) \| \forall k \in SubGrp (g) ((h \subseteq k \land p pGrp (g ↾_{𝑠} k)) \leftrightarrow h = k)\})$
24	0 23	wceq	$wff pSyl = (p \in ℙ, g \in Grp ⟼ \{h \in SubGrp (g) \| \forall k \in SubGrp (g) ((h \subseteq k \land p pGrp (g ↾_{𝑠} k)) \leftrightarrow h = k)\})$

Metamath Proof Explorer

Definition df-slw

Detailed syntax breakdown