Metamath Proof Explorer

Theorem dvdsrval

Description: Value of the divides relation. (Contributed by Mario Carneiro, 1-Dec-2014) (Revised by Mario Carneiro, 6-Jan-2015)

Ref Expression
Hypotheses dvdsr.1 
|- B = ( Base ` R )
dvdsr.2 
|- .|| = ( ||r ` R )
dvdsr.3 
|- .x. = ( .r ` R )
Assertion dvdsrval 
|- .|| = { <. x , y >. | ( x e. B /\ E. z e. B ( z .x. x ) = y ) }

Proof

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 syl5eq 
 |-  ( 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 syl5eq 
 |-  ( -. 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 syl5eq 
 |-  ( -. 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 ) }