This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elcntzsn

Description: Value of the centralizer of a singleton. (Contributed by Mario Carneiro, 25-Apr-2016)

Ref Expression
Hypotheses cntzfval.b 
|- B = ( Base ` M )
cntzfval.p 
|- .+ = ( +g ` M )
cntzfval.z 
|- Z = ( Cntz ` M )
Assertion elcntzsn 
|- ( Y e. B -> ( X e. ( Z ` { Y } ) <-> ( X e. B /\ ( X .+ Y ) = ( Y .+ X ) ) ) )

Proof

Step Hyp Ref Expression
1 cntzfval.b 
 |-  B = ( Base ` M )
2 cntzfval.p 
 |-  .+ = ( +g ` M )
3 cntzfval.z 
 |-  Z = ( Cntz ` M )
4 1 2 3 cntzsnval 
 |-  ( Y e. B -> ( Z ` { Y } ) = { x e. B | ( x .+ Y ) = ( Y .+ x ) } )
5 4 eleq2d 
 |-  ( Y e. B -> ( X e. ( Z ` { Y } ) <-> X e. { x e. B | ( x .+ Y ) = ( Y .+ x ) } ) )
6 oveq1 
 |-  ( x = X -> ( x .+ Y ) = ( X .+ Y ) )
7 oveq2 
 |-  ( x = X -> ( Y .+ x ) = ( Y .+ X ) )
8 6 7 eqeq12d 
 |-  ( x = X -> ( ( x .+ Y ) = ( Y .+ x ) <-> ( X .+ Y ) = ( Y .+ X ) ) )
9 8 elrab 
 |-  ( X e. { x e. B | ( x .+ Y ) = ( Y .+ x ) } <-> ( X e. B /\ ( X .+ Y ) = ( Y .+ X ) ) )
10 5 9 bitrdi 
 |-  ( Y e. B -> ( X e. ( Z ` { Y } ) <-> ( X e. B /\ ( X .+ Y ) = ( Y .+ X ) ) ) )