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 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 ) }