Theorem dvdsr

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

	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	dvdsr	$$⊢X\underset{\dot{}}{\parallel }Y\leftrightarrow \left(X\in B\wedge \exists z\in Bz\underset{\dot{}}{·}X=Y\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	2	reldvdsr	$$⊢\mathrm{Rel}\underset{\dot{}}{\parallel }$$
5	4	brrelex12i	$$⊢X\underset{\dot{}}{\parallel }Y\to \left(X\in \mathrm{V}\wedge Y\in \mathrm{V}\right)$$
6		elex	$$⊢X\in B\to X\in \mathrm{V}$$
7		id	$$⊢z\underset{\dot{}}{·}X=Y\to z\underset{\dot{}}{·}X=Y$$
8		ovex	$$⊢z\underset{\dot{}}{·}X\in \mathrm{V}$$
9	7 8	eqeltrrdi	$$⊢z\underset{\dot{}}{·}X=Y\to Y\in \mathrm{V}$$
10	9	rexlimivw	$$⊢\exists z\in Bz\underset{\dot{}}{·}X=Y\to Y\in \mathrm{V}$$
11	6 10	anim12i	$$⊢\left(X\in B\wedge \exists z\in Bz\underset{\dot{}}{·}X=Y\right)\to \left(X\in \mathrm{V}\wedge Y\in \mathrm{V}\right)$$
12		simpl	$$⊢\left(x=X\wedge y=Y\right)\to x=X$$
13	12	eleq1d	$$⊢\left(x=X\wedge y=Y\right)\to \left(x\in B\leftrightarrow X\in B\right)$$
14	12	oveq2d	$$⊢\left(x=X\wedge y=Y\right)\to z\underset{\dot{}}{·}x=z\underset{\dot{}}{·}X$$
15		simpr	$$⊢\left(x=X\wedge y=Y\right)\to y=Y$$
16	14 15	eqeq12d	$$⊢\left(x=X\wedge y=Y\right)\to \left(z\underset{\dot{}}{·}x=y\leftrightarrow z\underset{\dot{}}{·}X=Y\right)$$
17	16	rexbidv	$$⊢\left(x=X\wedge y=Y\right)\to \left(\exists z\in Bz\underset{\dot{}}{·}x=y\leftrightarrow \exists z\in Bz\underset{\dot{}}{·}X=Y\right)$$
18	13 17	anbi12d	$$⊢\left(x=X\wedge y=Y\right)\to \left(\left(x\in B\wedge \exists z\in Bz\underset{\dot{}}{·}x=y\right)\leftrightarrow \left(X\in B\wedge \exists z\in Bz\underset{\dot{}}{·}X=Y\right)\right)$$
19	1 2 3	dvdsrval	$$⊢\underset{\dot{}}{\parallel }=\left\{⟨x,y⟩|\left(x\in B\wedge \exists z\in Bz\underset{\dot{}}{·}x=y\right)\right\}$$
20	18 19	brabga	$$⊢\left(X\in \mathrm{V}\wedge Y\in \mathrm{V}\right)\to \left(X\underset{\dot{}}{\parallel }Y\leftrightarrow \left(X\in B\wedge \exists z\in Bz\underset{\dot{}}{·}X=Y\right)\right)$$
21	5 11 20	pm5.21nii	$$⊢X\underset{\dot{}}{\parallel }Y\leftrightarrow \left(X\in B\wedge \exists z\in Bz\underset{\dot{}}{·}X=Y\right)$$