Theorem dvdsr 16864

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

Hypotheses

Ref	Expression
dvdsr.1	|- B = ( Base ` R )
dvdsr.2	|- .|| = ( ||r ` R )
dvdsr.3	|- .x. = ( .r ` R )

Assertion

Ref	Expression
dvdsr	|- ( X .|| Y <-> ( X e. B /\ E. z e. B ( z .x. X ) = Y ) )

Distinct variable groups:   z, B   z, X   z, Y   z, R   z, .x.

Allowed substitution hint:   .|| ( z)

Proof of Theorem dvdsr

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dvdsr.2	. . . 4 |- .|| = ( ||r ` R )
2	1	reldvdsr 16862	. . 3 |- Rel .||
3		brrelex12 4987	. . 3 |- ( ( Rel .|| /\ X .|| Y ) -> ( X e. _V /\ Y e. _V ) )
4	2, 3	mpan 670	. 2 |- ( X .|| Y -> ( X e. _V /\ Y e. _V ) )
5		elex 3087	. . 3 |- ( X e. B -> X e. _V )
6		id 22	. . . . 5 |- ( ( z .x. X ) = Y -> ( z .x. X ) = Y )
7		ovex 6228	. . . . 5 |- ( z .x. X ) e. _V
8	6, 7	syl6eqelr 2551	. . . 4 |- ( ( z .x. X ) = Y -> Y e. _V )
9	8	rexlimivw 2943	. . 3 |- ( E. z e. B ( z .x. X ) = Y -> Y e. _V )
10	5, 9	anim12i 566	. 2 |- ( ( X e. B /\ E. z e. B ( z .x. X ) = Y ) -> ( X e. _V /\ Y e. _V ) )
11		simpl 457	. . . . 5 |- ( ( x = X /\ y = Y ) -> x = X )
12	11	eleq1d 2523	. . . 4 |- ( ( x = X /\ y = Y ) -> ( x e. B <-> X e. B ) )
13	11	oveq2d 6219	. . . . . 6 |- ( ( x = X /\ y = Y ) -> ( z .x. x ) = ( z .x. X ) )
14		simpr 461	. . . . . 6 |- ( ( x = X /\ y = Y ) -> y = Y )
15	13, 14	eqeq12d 2476	. . . . 5 |- ( ( x = X /\ y = Y ) -> ( ( z .x. x ) = y <-> ( z .x. X ) = Y ) )
16	15	rexbidv 2868	. . . 4 |- ( ( x = X /\ y = Y ) -> ( E. z e. B ( z .x. x ) = y <-> E. z e. B ( z .x. X ) = Y ) )
17	12, 16	anbi12d 710	. . 3 |- ( ( 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 ) ) )
18		dvdsr.1	. . . 4 |- B = ( Base ` R )
19		dvdsr.3	. . . 4 |- .x. = ( .r ` R )
20	18, 1, 19	dvdsrval 16863	. . 3 |- .|| = { <. x , y >. | ( x e. B /\ E. z e. B ( z .x. x ) = y ) }
21	17, 20	brabga 4714	. 2 |- ( ( X e. _V /\ Y e. _V ) -> ( X .|| Y <-> ( X e. B /\ E. z e. B ( z .x. X ) = Y ) ) )
22	4, 10, 21	pm5.21nii 353	1 |- ( X .|| Y <-> ( X e. B /\ E. z e. B ( z .x. X ) = Y ) )

Syntax hints:   <-> wb 184   /\ wa 369   = wceq 1370   e. wcel 1758   E.wrex 2800   _Vcvv 3078   class class class wbr 4403   Rel wrel 4956   ` cfv 5529  (class class class)co 6203   Basecbs 14295   .rcmulr 14361   ||_rcdsr 16856

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-rep 4514  ax-sep 4524  ax-nul 4532  ax-pow 4581  ax-pr 4642  ax-un 6485

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-ral 2804  df-rex 2805  df-reu 2806  df-rab 2808  df-v 3080  df-sbc 3295  df-csb 3399  df-dif 3442  df-un 3444  df-in 3446  df-ss 3453  df-nul 3749  df-if 3903  df-pw 3973  df-sn 3989  df-pr 3991  df-op 3995  df-uni 4203  df-iun 4284  df-br 4404  df-opab 4462  df-mpt 4463  df-id 4747  df-xp 4957  df-rel 4958  df-cnv 4959  df-co 4960  df-dm 4961  df-rn 4962  df-res 4963  df-ima 4964  df-iota 5492  df-fun 5531  df-fn 5532  df-f 5533  df-f1 5534  df-fo 5535  df-f1o 5536  df-fv 5537  df-ov 6206  df-dvdsr 16859

This theorem is referenced by:  dvdsr2  16865  dvdsrmul  16866  dvdsrcl  16867  dvdsrcl2  16868  dvdsrtr  16870  dvdsrmul1  16871  opprunit  16879  crngunit  16880  subrgdvds  17005  rhmdvdsr  26451