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