Step |
Hyp |
Ref |
Expression |
1 |
|
cntzfval.b |
|- B = ( Base ` M ) |
2 |
|
cntzfval.p |
|- .+ = ( +g ` M ) |
3 |
|
cntzfval.z |
|- Z = ( Cntz ` M ) |
4 |
|
elex |
|- ( M e. V -> M e. _V ) |
5 |
|
fveq2 |
|- ( m = M -> ( Base ` m ) = ( Base ` M ) ) |
6 |
5 1
|
eqtr4di |
|- ( m = M -> ( Base ` m ) = B ) |
7 |
6
|
pweqd |
|- ( m = M -> ~P ( Base ` m ) = ~P B ) |
8 |
|
fveq2 |
|- ( m = M -> ( +g ` m ) = ( +g ` M ) ) |
9 |
8 2
|
eqtr4di |
|- ( m = M -> ( +g ` m ) = .+ ) |
10 |
9
|
oveqd |
|- ( m = M -> ( x ( +g ` m ) y ) = ( x .+ y ) ) |
11 |
9
|
oveqd |
|- ( m = M -> ( y ( +g ` m ) x ) = ( y .+ x ) ) |
12 |
10 11
|
eqeq12d |
|- ( m = M -> ( ( x ( +g ` m ) y ) = ( y ( +g ` m ) x ) <-> ( x .+ y ) = ( y .+ x ) ) ) |
13 |
12
|
ralbidv |
|- ( m = M -> ( A. y e. s ( x ( +g ` m ) y ) = ( y ( +g ` m ) x ) <-> A. y e. s ( x .+ y ) = ( y .+ x ) ) ) |
14 |
6 13
|
rabeqbidv |
|- ( m = M -> { x e. ( Base ` m ) | A. y e. s ( x ( +g ` m ) y ) = ( y ( +g ` m ) x ) } = { x e. B | A. y e. s ( x .+ y ) = ( y .+ x ) } ) |
15 |
7 14
|
mpteq12dv |
|- ( m = M -> ( s e. ~P ( Base ` m ) |-> { x e. ( Base ` m ) | A. y e. s ( x ( +g ` m ) y ) = ( y ( +g ` m ) x ) } ) = ( s e. ~P B |-> { x e. B | A. y e. s ( x .+ y ) = ( y .+ x ) } ) ) |
16 |
|
df-cntz |
|- Cntz = ( m e. _V |-> ( s e. ~P ( Base ` m ) |-> { x e. ( Base ` m ) | A. y e. s ( x ( +g ` m ) y ) = ( y ( +g ` m ) x ) } ) ) |
17 |
1
|
fvexi |
|- B e. _V |
18 |
17
|
pwex |
|- ~P B e. _V |
19 |
18
|
mptex |
|- ( s e. ~P B |-> { x e. B | A. y e. s ( x .+ y ) = ( y .+ x ) } ) e. _V |
20 |
15 16 19
|
fvmpt |
|- ( M e. _V -> ( Cntz ` M ) = ( s e. ~P B |-> { x e. B | A. y e. s ( x .+ y ) = ( y .+ x ) } ) ) |
21 |
4 20
|
syl |
|- ( M e. V -> ( Cntz ` M ) = ( s e. ~P B |-> { x e. B | A. y e. s ( x .+ y ) = ( y .+ x ) } ) ) |
22 |
3 21
|
eqtrid |
|- ( M e. V -> Z = ( s e. ~P B |-> { x e. B | A. y e. s ( x .+ y ) = ( y .+ x ) } ) ) |