Step |
Hyp |
Ref |
Expression |
1 |
|
dvdsr.1 |
|- B = ( Base ` R ) |
2 |
|
dvdsr.2 |
|- .|| = ( ||r ` R ) |
3 |
|
dvdsr.3 |
|- .x. = ( .r ` R ) |
4 |
|
fveq2 |
|- ( r = R -> ( Base ` r ) = ( Base ` R ) ) |
5 |
4 1
|
eqtr4di |
|- ( r = R -> ( Base ` r ) = B ) |
6 |
5
|
eleq2d |
|- ( r = R -> ( x e. ( Base ` r ) <-> x e. B ) ) |
7 |
5
|
rexeqdv |
|- ( r = R -> ( E. z e. ( Base ` r ) ( z ( .r ` r ) x ) = y <-> E. z e. B ( z ( .r ` r ) x ) = y ) ) |
8 |
6 7
|
anbi12d |
|- ( r = R -> ( ( x e. ( Base ` r ) /\ E. z e. ( Base ` r ) ( z ( .r ` r ) x ) = y ) <-> ( x e. B /\ E. z e. B ( z ( .r ` r ) x ) = y ) ) ) |
9 |
|
fveq2 |
|- ( r = R -> ( .r ` r ) = ( .r ` R ) ) |
10 |
9 3
|
eqtr4di |
|- ( r = R -> ( .r ` r ) = .x. ) |
11 |
10
|
oveqd |
|- ( r = R -> ( z ( .r ` r ) x ) = ( z .x. x ) ) |
12 |
11
|
eqeq1d |
|- ( r = R -> ( ( z ( .r ` r ) x ) = y <-> ( z .x. x ) = y ) ) |
13 |
12
|
rexbidv |
|- ( r = R -> ( E. z e. B ( z ( .r ` r ) x ) = y <-> E. z e. B ( z .x. x ) = y ) ) |
14 |
13
|
anbi2d |
|- ( r = R -> ( ( x e. B /\ E. z e. B ( z ( .r ` r ) x ) = y ) <-> ( x e. B /\ E. z e. B ( z .x. x ) = y ) ) ) |
15 |
8 14
|
bitrd |
|- ( r = R -> ( ( x e. ( Base ` r ) /\ E. z e. ( Base ` r ) ( z ( .r ` r ) x ) = y ) <-> ( x e. B /\ E. z e. B ( z .x. x ) = y ) ) ) |
16 |
15
|
opabbidv |
|- ( r = R -> { <. x , y >. | ( x e. ( Base ` r ) /\ E. z e. ( Base ` r ) ( z ( .r ` r ) x ) = y ) } = { <. x , y >. | ( x e. B /\ E. z e. B ( z .x. x ) = y ) } ) |
17 |
|
df-dvdsr |
|- ||r = ( r e. _V |-> { <. x , y >. | ( x e. ( Base ` r ) /\ E. z e. ( Base ` r ) ( z ( .r ` r ) x ) = y ) } ) |
18 |
1
|
fvexi |
|- B e. _V |
19 |
|
eqcom |
|- ( ( z .x. x ) = y <-> y = ( z .x. x ) ) |
20 |
19
|
rexbii |
|- ( E. z e. B ( z .x. x ) = y <-> E. z e. B y = ( z .x. x ) ) |
21 |
20
|
abbii |
|- { y | E. z e. B ( z .x. x ) = y } = { y | E. z e. B y = ( z .x. x ) } |
22 |
18
|
abrexex |
|- { y | E. z e. B y = ( z .x. x ) } e. _V |
23 |
21 22
|
eqeltri |
|- { y | E. z e. B ( z .x. x ) = y } e. _V |
24 |
23
|
a1i |
|- ( x e. B -> { y | E. z e. B ( z .x. x ) = y } e. _V ) |
25 |
18 24
|
opabex3 |
|- { <. x , y >. | ( x e. B /\ E. z e. B ( z .x. x ) = y ) } e. _V |
26 |
16 17 25
|
fvmpt |
|- ( R e. _V -> ( ||r ` R ) = { <. x , y >. | ( x e. B /\ E. z e. B ( z .x. x ) = y ) } ) |
27 |
2 26
|
eqtrid |
|- ( R e. _V -> .|| = { <. x , y >. | ( x e. B /\ E. z e. B ( z .x. x ) = y ) } ) |
28 |
|
fvprc |
|- ( -. R e. _V -> ( ||r ` R ) = (/) ) |
29 |
2 28
|
eqtrid |
|- ( -. R e. _V -> .|| = (/) ) |
30 |
|
opabn0 |
|- ( { <. x , y >. | ( x e. B /\ E. z e. B ( z .x. x ) = y ) } =/= (/) <-> E. x E. y ( x e. B /\ E. z e. B ( z .x. x ) = y ) ) |
31 |
|
n0i |
|- ( x e. B -> -. B = (/) ) |
32 |
|
fvprc |
|- ( -. R e. _V -> ( Base ` R ) = (/) ) |
33 |
1 32
|
eqtrid |
|- ( -. R e. _V -> B = (/) ) |
34 |
31 33
|
nsyl2 |
|- ( x e. B -> R e. _V ) |
35 |
34
|
adantr |
|- ( ( x e. B /\ E. z e. B ( z .x. x ) = y ) -> R e. _V ) |
36 |
35
|
exlimivv |
|- ( E. x E. y ( x e. B /\ E. z e. B ( z .x. x ) = y ) -> R e. _V ) |
37 |
30 36
|
sylbi |
|- ( { <. x , y >. | ( x e. B /\ E. z e. B ( z .x. x ) = y ) } =/= (/) -> R e. _V ) |
38 |
37
|
necon1bi |
|- ( -. R e. _V -> { <. x , y >. | ( x e. B /\ E. z e. B ( z .x. x ) = y ) } = (/) ) |
39 |
29 38
|
eqtr4d |
|- ( -. R e. _V -> .|| = { <. x , y >. | ( x e. B /\ E. z e. B ( z .x. x ) = y ) } ) |
40 |
27 39
|
pm2.61i |
|- .|| = { <. x , y >. | ( x e. B /\ E. z e. B ( z .x. x ) = y ) } |