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
|
cntzfval |
|- ( M e. _V -> Z = ( s e. ~P B |-> { x e. B | A. y e. s ( x .+ y ) = ( y .+ x ) } ) ) |
5 |
4
|
fveq1d |
|- ( M e. _V -> ( Z ` S ) = ( ( s e. ~P B |-> { x e. B | A. y e. s ( x .+ y ) = ( y .+ x ) } ) ` S ) ) |
6 |
1
|
fvexi |
|- B e. _V |
7 |
6
|
elpw2 |
|- ( S e. ~P B <-> S C_ B ) |
8 |
|
raleq |
|- ( s = S -> ( A. y e. s ( x .+ y ) = ( y .+ x ) <-> A. y e. S ( x .+ y ) = ( y .+ x ) ) ) |
9 |
8
|
rabbidv |
|- ( s = S -> { x e. B | A. y e. s ( x .+ y ) = ( y .+ x ) } = { x e. B | A. y e. S ( x .+ y ) = ( y .+ x ) } ) |
10 |
|
eqid |
|- ( s e. ~P B |-> { x e. B | A. y e. s ( x .+ y ) = ( y .+ x ) } ) = ( s e. ~P B |-> { x e. B | A. y e. s ( x .+ y ) = ( y .+ x ) } ) |
11 |
6
|
rabex |
|- { x e. B | A. y e. S ( x .+ y ) = ( y .+ x ) } e. _V |
12 |
9 10 11
|
fvmpt |
|- ( S e. ~P B -> ( ( s e. ~P B |-> { x e. B | A. y e. s ( x .+ y ) = ( y .+ x ) } ) ` S ) = { x e. B | A. y e. S ( x .+ y ) = ( y .+ x ) } ) |
13 |
7 12
|
sylbir |
|- ( S C_ B -> ( ( s e. ~P B |-> { x e. B | A. y e. s ( x .+ y ) = ( y .+ x ) } ) ` S ) = { x e. B | A. y e. S ( x .+ y ) = ( y .+ x ) } ) |
14 |
5 13
|
sylan9eq |
|- ( ( M e. _V /\ S C_ B ) -> ( Z ` S ) = { x e. B | A. y e. S ( x .+ y ) = ( y .+ x ) } ) |
15 |
|
0fv |
|- ( (/) ` S ) = (/) |
16 |
|
fvprc |
|- ( -. M e. _V -> ( Cntz ` M ) = (/) ) |
17 |
3 16
|
eqtrid |
|- ( -. M e. _V -> Z = (/) ) |
18 |
17
|
fveq1d |
|- ( -. M e. _V -> ( Z ` S ) = ( (/) ` S ) ) |
19 |
|
ssrab2 |
|- { x e. B | A. y e. S ( x .+ y ) = ( y .+ x ) } C_ B |
20 |
|
fvprc |
|- ( -. M e. _V -> ( Base ` M ) = (/) ) |
21 |
1 20
|
eqtrid |
|- ( -. M e. _V -> B = (/) ) |
22 |
19 21
|
sseqtrid |
|- ( -. M e. _V -> { x e. B | A. y e. S ( x .+ y ) = ( y .+ x ) } C_ (/) ) |
23 |
|
ss0 |
|- ( { x e. B | A. y e. S ( x .+ y ) = ( y .+ x ) } C_ (/) -> { x e. B | A. y e. S ( x .+ y ) = ( y .+ x ) } = (/) ) |
24 |
22 23
|
syl |
|- ( -. M e. _V -> { x e. B | A. y e. S ( x .+ y ) = ( y .+ x ) } = (/) ) |
25 |
15 18 24
|
3eqtr4a |
|- ( -. M e. _V -> ( Z ` S ) = { x e. B | A. y e. S ( x .+ y ) = ( y .+ x ) } ) |
26 |
25
|
adantr |
|- ( ( -. M e. _V /\ S C_ B ) -> ( Z ` S ) = { x e. B | A. y e. S ( x .+ y ) = ( y .+ x ) } ) |
27 |
14 26
|
pm2.61ian |
|- ( S C_ B -> ( Z ` S ) = { x e. B | A. y e. S ( x .+ y ) = ( y .+ x ) } ) |