Metamath Proof Explorer

Theorem dvdsr

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

Ref Expression
Hypotheses dvdsr.1 
|- B = ( Base ` R )
dvdsr.2 
|- .|| = ( ||r ` R )
dvdsr.3 
|- .x. = ( .r ` R )
Assertion dvdsr 
|- ( 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 2 reldvdsr 
 |-  Rel .||
5 4 brrelex12i 
 |-  ( X .|| Y -> ( X e. _V /\ Y e. _V ) )
6 elex 
 |-  ( X e. B -> X e. _V )
7 id 
 |-  ( ( z .x. X ) = Y -> ( z .x. X ) = Y )
8 ovex 
 |-  ( z .x. X ) e. _V
9 7 8 eqeltrrdi 
 |-  ( ( z .x. X ) = Y -> Y e. _V )
10 9 rexlimivw 
 |-  ( E. z e. B ( z .x. X ) = Y -> Y e. _V )
11 6 10 anim12i 
 |-  ( ( X e. B /\ E. z e. B ( z .x. X ) = Y ) -> ( X e. _V /\ Y e. _V ) )
12 simpl 
 |-  ( ( x = X /\ y = Y ) -> x = X )
13 12 eleq1d 
 |-  ( ( x = X /\ y = Y ) -> ( x e. B <-> X e. B ) )
14 12 oveq2d 
 |-  ( ( x = X /\ y = Y ) -> ( z .x. x ) = ( z .x. X ) )
15 simpr 
 |-  ( ( x = X /\ y = Y ) -> y = Y )
16 14 15 eqeq12d 
 |-  ( ( x = X /\ y = Y ) -> ( ( z .x. x ) = y <-> ( z .x. X ) = Y ) )
17 16 rexbidv 
 |-  ( ( x = X /\ y = Y ) -> ( E. z e. B ( z .x. x ) = y <-> E. z e. B ( z .x. X ) = Y ) )
18 13 17 anbi12d 
 |-  ( ( x = X /\ y = Y ) -> ( ( x e. B /\ E. z e. B ( z .x. x ) = y ) <-> ( X e. B /\ E. z e. B ( z .x. X ) = Y ) ) )
19 1 2 3 dvdsrval 
 |-  .|| = { <. x , y >. | ( x e. B /\ E. z e. B ( z .x. x ) = y ) }
20 18 19 brabga 
 |-  ( ( X e. _V /\ Y e. _V ) -> ( X .|| Y <-> ( X e. B /\ E. z e. B ( z .x. X ) = Y ) ) )
21 5 11 20 pm5.21nii 
 |-  ( X .|| Y <-> ( X e. B /\ E. z e. B ( z .x. X ) = Y ) )