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={\mathrm{Base}}_R$$
	dvdsr.2	$$⊢\underset{\dot{}}{\parallel }={\parallel }_r\left(R\right)$$
	dvdsr.3	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
Assertion	dvdsrval	$$⊢\underset{\dot{}}{\parallel }=\left\{⟨x,y⟩|\left(x\in B\wedge \exists z\in Bz\underset{\dot{}}{·}x=y\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		dvdsr.1	$$⊢B={\mathrm{Base}}_R$$
2		dvdsr.2	$$⊢\underset{\dot{}}{\parallel }={\parallel }_r\left(R\right)$$
3		dvdsr.3	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
4		fveq2	$$⊢r=R\to {\mathrm{Base}}_r={\mathrm{Base}}_R$$
5	4 1	syl6eqr	$$⊢r=R\to {\mathrm{Base}}_r=B$$
6	5	eleq2d	$$⊢r=R\to \left(x\in {\mathrm{Base}}_r\leftrightarrow x\in B\right)$$
7	5	rexeqdv	$$⊢r=R\to \left(\exists z\in {\mathrm{Base}}_{r}z{\cdot }_{r}x=y\leftrightarrow \exists z\in Bz{\cdot }_{r}x=y\right)$$
8	6 7	anbi12d	$$⊢r=R\to \left(\left(x\in {\mathrm{Base}}_r\wedge \exists z\in {\mathrm{Base}}_{r}z{\cdot }_{r}x=y\right)\leftrightarrow \left(x\in B\wedge \exists z\in Bz{\cdot }_{r}x=y\right)\right)$$
9		fveq2	$$⊢r=R\to {\cdot }_r={\cdot }_R$$
10	9 3	syl6eqr	$$⊢r=R\to {\cdot }_r=\underset{\dot{}}{·}$$
11	10	oveqd	$$⊢r=R\to z{\cdot }_{r}x=z\underset{\dot{}}{·}x$$
12	11	eqeq1d	$$⊢r=R\to \left(z{\cdot }_{r}x=y\leftrightarrow z\underset{\dot{}}{·}x=y\right)$$
13	12	rexbidv	$$⊢r=R\to \left(\exists z\in Bz{\cdot }_{r}x=y\leftrightarrow \exists z\in Bz\underset{\dot{}}{·}x=y\right)$$
14	13	anbi2d	$$⊢r=R\to \left(\left(x\in B\wedge \exists z\in Bz{\cdot }_{r}x=y\right)\leftrightarrow \left(x\in B\wedge \exists z\in Bz\underset{\dot{}}{·}x=y\right)\right)$$
15	8 14	bitrd	$$⊢r=R\to \left(\left(x\in {\mathrm{Base}}_r\wedge \exists z\in {\mathrm{Base}}_{r}z{\cdot }_{r}x=y\right)\leftrightarrow \left(x\in B\wedge \exists z\in Bz\underset{\dot{}}{·}x=y\right)\right)$$
16	15	opabbidv	$$⊢r=R\to \left\{⟨x,y⟩|\left(x\in {\mathrm{Base}}_r\wedge \exists z\in {\mathrm{Base}}_{r}z{\cdot }_{r}x=y\right)\right\}=\left\{⟨x,y⟩|\left(x\in B\wedge \exists z\in Bz\underset{\dot{}}{·}x=y\right)\right\}$$
17		df-dvdsr	$$⊢{\parallel }_r=\left(r\in \mathrm{V}⟼\left\{⟨x,y⟩|\left(x\in {\mathrm{Base}}_r\wedge \exists z\in {\mathrm{Base}}_{r}z{\cdot }_{r}x=y\right)\right\}\right)$$
18	1	fvexi	$$⊢B\in \mathrm{V}$$
19		eqcom	$$⊢z\underset{\dot{}}{·}x=y\leftrightarrow y=z\underset{\dot{}}{·}x$$
20	19	rexbii	$$⊢\exists z\in Bz\underset{\dot{}}{·}x=y\leftrightarrow \exists z\in By=z\underset{\dot{}}{·}x$$
21	20	abbii	$$⊢\left\{y|\exists z\in Bz\underset{\dot{}}{·}x=y\right\}=\left\{y|\exists z\in By=z\underset{\dot{}}{·}x\right\}$$
22	18	abrexex	$$⊢\left\{y|\exists z\in By=z\underset{\dot{}}{·}x\right\}\in \mathrm{V}$$
23	21 22	eqeltri	$$⊢\left\{y|\exists z\in Bz\underset{\dot{}}{·}x=y\right\}\in \mathrm{V}$$
24	23	a1i	$$⊢x\in B\to \left\{y|\exists z\in Bz\underset{\dot{}}{·}x=y\right\}\in \mathrm{V}$$
25	18 24	opabex3	$$⊢\left\{⟨x,y⟩|\left(x\in B\wedge \exists z\in Bz\underset{\dot{}}{·}x=y\right)\right\}\in \mathrm{V}$$
26	16 17 25	fvmpt	$$⊢R\in \mathrm{V}\to {\parallel }_r\left(R\right)=\left\{⟨x,y⟩|\left(x\in B\wedge \exists z\in Bz\underset{\dot{}}{·}x=y\right)\right\}$$
27	2 26	syl5eq	$$⊢R\in \mathrm{V}\to \underset{\dot{}}{\parallel }=\left\{⟨x,y⟩|\left(x\in B\wedge \exists z\in Bz\underset{\dot{}}{·}x=y\right)\right\}$$
28		fvprc	$$⊢\neg R\in \mathrm{V}\to {\parallel }_r\left(R\right)=\varnothing$$
29	2 28	syl5eq	$$⊢\neg R\in \mathrm{V}\to \underset{\dot{}}{\parallel }=\varnothing$$
30		opabn0	$$⊢\left\{⟨x,y⟩|\left(x\in B\wedge \exists z\in Bz\underset{\dot{}}{·}x=y\right)\right\}\ne \varnothing \leftrightarrow \exists x\exists y\left(x\in B\wedge \exists z\in Bz\underset{\dot{}}{·}x=y\right)$$
31		n0i	$$⊢x\in B\to \neg B=\varnothing$$
32		fvprc	$$⊢\neg R\in \mathrm{V}\to {\mathrm{Base}}_R=\varnothing$$
33	1 32	syl5eq	$$⊢\neg R\in \mathrm{V}\to B=\varnothing$$
34	31 33	nsyl2	$$⊢x\in B\to R\in \mathrm{V}$$
35	34	adantr	$$⊢\left(x\in B\wedge \exists z\in Bz\underset{\dot{}}{·}x=y\right)\to R\in \mathrm{V}$$
36	35	exlimivv	$$⊢\exists x\exists y\left(x\in B\wedge \exists z\in Bz\underset{\dot{}}{·}x=y\right)\to R\in \mathrm{V}$$
37	30 36	sylbi	$$⊢\left\{⟨x,y⟩|\left(x\in B\wedge \exists z\in Bz\underset{\dot{}}{·}x=y\right)\right\}\ne \varnothing \to R\in \mathrm{V}$$
38	37	necon1bi	$$⊢\neg R\in \mathrm{V}\to \left\{⟨x,y⟩|\left(x\in B\wedge \exists z\in Bz\underset{\dot{}}{·}x=y\right)\right\}=\varnothing$$
39	29 38	eqtr4d	$$⊢\neg R\in \mathrm{V}\to \underset{\dot{}}{\parallel }=\left\{⟨x,y⟩|\left(x\in B\wedge \exists z\in Bz\underset{\dot{}}{·}x=y\right)\right\}$$
40	27 39	pm2.61i	$$⊢\underset{\dot{}}{\parallel }=\left\{⟨x,y⟩|\left(x\in B\wedge \exists z\in Bz\underset{\dot{}}{·}x=y\right)\right\}$$