Theorem cntzssv

Description: The centralizer is unconditionally a subset. (Contributed by Stefan O'Rear, 6-Sep-2015)

	Ref	Expression
Hypotheses	cntzrcl.b	|- B = ( Base ` M )
	cntzrcl.z	|- Z = ( Cntz ` M )
Assertion	cntzssv	|- ( Z ` S ) C_ B

Proof

Step	Hyp	Ref	Expression
1		cntzrcl.b	|- B = ( Base ` M )
2		cntzrcl.z	|- Z = ( Cntz ` M )
3		0ss	|- (/) C_ B
4		sseq1	|- ( ( Z ` S ) = (/) -> ( ( Z ` S ) C_ B <-> (/) C_ B ) )
5	3 4	mpbiri	|- ( ( Z ` S ) = (/) -> ( Z ` S ) C_ B )
6		n0	|- ( ( Z ` S ) =/= (/) <-> E. x x e. ( Z ` S ) )
7	1 2	cntzrcl	|- ( x e. ( Z ` S ) -> ( M e. _V /\ S C_ B ) )
8		eqid	|- ( +g ` M ) = ( +g ` M )
9	1 8 2	cntzval	|- ( S C_ B -> ( Z ` S ) = { x e. B | A. y e. S ( x ( +g ` M ) y ) = ( y ( +g ` M ) x ) } )
10	7 9	simpl2im	|- ( x e. ( Z ` S ) -> ( Z ` S ) = { x e. B | A. y e. S ( x ( +g ` M ) y ) = ( y ( +g ` M ) x ) } )
11		ssrab2	|- { x e. B | A. y e. S ( x ( +g ` M ) y ) = ( y ( +g ` M ) x ) } C_ B
12	10 11	eqsstrdi	|- ( x e. ( Z ` S ) -> ( Z ` S ) C_ B )
13	12	exlimiv	|- ( E. x x e. ( Z ` S ) -> ( Z ` S ) C_ B )
14	6 13	sylbi	|- ( ( Z ` S ) =/= (/) -> ( Z ` S ) C_ B )
15	5 14	pm2.61ine	|- ( Z ` S ) C_ B