Metamath Proof Explorer

Theorem cntz2ss

Description: Centralizers reverse the subset relation. (Contributed by Mario Carneiro, 3-Oct-2015)

Ref Expression
Hypotheses cntzrec.b 
|- B = ( Base ` M )
cntzrec.z 
|- Z = ( Cntz ` M )
Assertion cntz2ss 
|- ( ( S C_ B /\ T C_ S ) -> ( Z ` S ) C_ ( Z ` T ) )

Proof

Step Hyp Ref Expression
1 cntzrec.b 
 |-  B = ( Base ` M )
2 cntzrec.z 
 |-  Z = ( Cntz ` M )
3 eqid 
 |-  ( +g ` M ) = ( +g ` M )
4 3 2 cntzi 
 |-  ( ( x e. ( Z ` S ) /\ y e. S ) -> ( x ( +g ` M ) y ) = ( y ( +g ` M ) x ) )
5 4 ralrimiva 
 |-  ( x e. ( Z ` S ) -> A. y e. S ( x ( +g ` M ) y ) = ( y ( +g ` M ) x ) )
6 ssralv 
 |-  ( T C_ S -> ( A. y e. S ( x ( +g ` M ) y ) = ( y ( +g ` M ) x ) -> A. y e. T ( x ( +g ` M ) y ) = ( y ( +g ` M ) x ) ) )
7 6 adantl 
 |-  ( ( S C_ B /\ T C_ S ) -> ( A. y e. S ( x ( +g ` M ) y ) = ( y ( +g ` M ) x ) -> A. y e. T ( x ( +g ` M ) y ) = ( y ( +g ` M ) x ) ) )
8 5 7 syl5 
 |-  ( ( S C_ B /\ T C_ S ) -> ( x e. ( Z ` S ) -> A. y e. T ( x ( +g ` M ) y ) = ( y ( +g ` M ) x ) ) )
9 8 ralrimiv 
 |-  ( ( S C_ B /\ T C_ S ) -> A. x e. ( Z ` S ) A. y e. T ( x ( +g ` M ) y ) = ( y ( +g ` M ) x ) )
10 1 2 cntzssv 
 |-  ( Z ` S ) C_ B
11 sstr 
 |-  ( ( T C_ S /\ S C_ B ) -> T C_ B )
12 11 ancoms 
 |-  ( ( S C_ B /\ T C_ S ) -> T C_ B )
13 1 3 2 sscntz 
 |-  ( ( ( Z ` S ) C_ B /\ T C_ B ) -> ( ( Z ` S ) C_ ( Z ` T ) <-> A. x e. ( Z ` S ) A. y e. T ( x ( +g ` M ) y ) = ( y ( +g ` M ) x ) ) )
14 10 12 13 sylancr 
 |-  ( ( S C_ B /\ T C_ S ) -> ( ( Z ` S ) C_ ( Z ` T ) <-> A. x e. ( Z ` S ) A. y e. T ( x ( +g ` M ) y ) = ( y ( +g ` M ) x ) ) )
15 9 14 mpbird 
 |-  ( ( S C_ B /\ T C_ S ) -> ( Z ` S ) C_ ( Z ` T ) )