Theorem dvdsr

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

	Ref	Expression
Hypotheses	dvdsr.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
	dvdsr.2	⊢ ∥ = ( ∥r ‘ 𝑅 )
	dvdsr.3	⊢ · = ( .r ‘ 𝑅 )
Assertion	dvdsr	⊢ ( 𝑋 ∥ 𝑌 ↔ ( 𝑋 ∈ 𝐵 ∧ ∃ 𝑧 ∈ 𝐵 ( 𝑧 · 𝑋 ) = 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		dvdsr.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		dvdsr.2	⊢ ∥ = ( ∥r ‘ 𝑅 )
3		dvdsr.3	⊢ · = ( .r ‘ 𝑅 )
4	2	reldvdsr	⊢ Rel ∥
5	4	brrelex12i	⊢ ( 𝑋 ∥ 𝑌 → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) )
6		elex	⊢ ( 𝑋 ∈ 𝐵 → 𝑋 ∈ V )
7		id	⊢ ( ( 𝑧 · 𝑋 ) = 𝑌 → ( 𝑧 · 𝑋 ) = 𝑌 )
8		ovex	⊢ ( 𝑧 · 𝑋 ) ∈ V
9	7 8	eqeltrrdi	⊢ ( ( 𝑧 · 𝑋 ) = 𝑌 → 𝑌 ∈ V )
10	9	rexlimivw	⊢ ( ∃ 𝑧 ∈ 𝐵 ( 𝑧 · 𝑋 ) = 𝑌 → 𝑌 ∈ V )
11	6 10	anim12i	⊢ ( ( 𝑋 ∈ 𝐵 ∧ ∃ 𝑧 ∈ 𝐵 ( 𝑧 · 𝑋 ) = 𝑌 ) → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) )
12		simpl	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → 𝑥 = 𝑋 )
13	12	eleq1d	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( 𝑥 ∈ 𝐵 ↔ 𝑋 ∈ 𝐵 ) )
14	12	oveq2d	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( 𝑧 · 𝑥 ) = ( 𝑧 · 𝑋 ) )
15		simpr	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → 𝑦 = 𝑌 )
16	14 15	eqeq12d	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( ( 𝑧 · 𝑥 ) = 𝑦 ↔ ( 𝑧 · 𝑋 ) = 𝑌 ) )
17	16	rexbidv	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( ∃ 𝑧 ∈ 𝐵 ( 𝑧 · 𝑥 ) = 𝑦 ↔ ∃ 𝑧 ∈ 𝐵 ( 𝑧 · 𝑋 ) = 𝑌 ) )
18	13 17	anbi12d	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( ( 𝑥 ∈ 𝐵 ∧ ∃ 𝑧 ∈ 𝐵 ( 𝑧 · 𝑥 ) = 𝑦 ) ↔ ( 𝑋 ∈ 𝐵 ∧ ∃ 𝑧 ∈ 𝐵 ( 𝑧 · 𝑋 ) = 𝑌 ) ) )
19	1 2 3	dvdsrval	⊢ ∥ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐵 ∧ ∃ 𝑧 ∈ 𝐵 ( 𝑧 · 𝑥 ) = 𝑦 ) }
20	18 19	brabga	⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → ( 𝑋 ∥ 𝑌 ↔ ( 𝑋 ∈ 𝐵 ∧ ∃ 𝑧 ∈ 𝐵 ( 𝑧 · 𝑋 ) = 𝑌 ) ) )
21	5 11 20	pm5.21nii	⊢ ( 𝑋 ∥ 𝑌 ↔ ( 𝑋 ∈ 𝐵 ∧ ∃ 𝑧 ∈ 𝐵 ( 𝑧 · 𝑋 ) = 𝑌 ) )