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	⊢ 𝐵 = ( Base ‘ 𝑅 )
	dvdsr.2	⊢ ∥ = ( ∥r ‘ 𝑅 )
	dvdsr.3	⊢ · = ( .r ‘ 𝑅 )
Assertion	dvdsrval	⊢ ∥ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐵 ∧ ∃ 𝑧 ∈ 𝐵 ( 𝑧 · 𝑥 ) = 𝑦 ) }

Proof

Step	Hyp	Ref	Expression
1		dvdsr.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		dvdsr.2	⊢ ∥ = ( ∥r ‘ 𝑅 )
3		dvdsr.3	⊢ · = ( .r ‘ 𝑅 )
4		fveq2	⊢ ( 𝑟 = 𝑅 → ( Base ‘ 𝑟 ) = ( Base ‘ 𝑅 ) )
5	4 1	eqtr4di	⊢ ( 𝑟 = 𝑅 → ( Base ‘ 𝑟 ) = 𝐵 )
6	5	eleq2d	⊢ ( 𝑟 = 𝑅 → ( 𝑥 ∈ ( Base ‘ 𝑟 ) ↔ 𝑥 ∈ 𝐵 ) )
7	5	rexeqdv	⊢ ( 𝑟 = 𝑅 → ( ∃ 𝑧 ∈ ( Base ‘ 𝑟 ) ( 𝑧 ( .r ‘ 𝑟 ) 𝑥 ) = 𝑦 ↔ ∃ 𝑧 ∈ 𝐵 ( 𝑧 ( .r ‘ 𝑟 ) 𝑥 ) = 𝑦 ) )
8	6 7	anbi12d	⊢ ( 𝑟 = 𝑅 → ( ( 𝑥 ∈ ( Base ‘ 𝑟 ) ∧ ∃ 𝑧 ∈ ( Base ‘ 𝑟 ) ( 𝑧 ( .r ‘ 𝑟 ) 𝑥 ) = 𝑦 ) ↔ ( 𝑥 ∈ 𝐵 ∧ ∃ 𝑧 ∈ 𝐵 ( 𝑧 ( .r ‘ 𝑟 ) 𝑥 ) = 𝑦 ) ) )
9		fveq2	⊢ ( 𝑟 = 𝑅 → ( .r ‘ 𝑟 ) = ( .r ‘ 𝑅 ) )
10	9 3	eqtr4di	⊢ ( 𝑟 = 𝑅 → ( .r ‘ 𝑟 ) = · )
11	10	oveqd	⊢ ( 𝑟 = 𝑅 → ( 𝑧 ( .r ‘ 𝑟 ) 𝑥 ) = ( 𝑧 · 𝑥 ) )
12	11	eqeq1d	⊢ ( 𝑟 = 𝑅 → ( ( 𝑧 ( .r ‘ 𝑟 ) 𝑥 ) = 𝑦 ↔ ( 𝑧 · 𝑥 ) = 𝑦 ) )
13	12	rexbidv	⊢ ( 𝑟 = 𝑅 → ( ∃ 𝑧 ∈ 𝐵 ( 𝑧 ( .r ‘ 𝑟 ) 𝑥 ) = 𝑦 ↔ ∃ 𝑧 ∈ 𝐵 ( 𝑧 · 𝑥 ) = 𝑦 ) )
14	13	anbi2d	⊢ ( 𝑟 = 𝑅 → ( ( 𝑥 ∈ 𝐵 ∧ ∃ 𝑧 ∈ 𝐵 ( 𝑧 ( .r ‘ 𝑟 ) 𝑥 ) = 𝑦 ) ↔ ( 𝑥 ∈ 𝐵 ∧ ∃ 𝑧 ∈ 𝐵 ( 𝑧 · 𝑥 ) = 𝑦 ) ) )
15	8 14	bitrd	⊢ ( 𝑟 = 𝑅 → ( ( 𝑥 ∈ ( Base ‘ 𝑟 ) ∧ ∃ 𝑧 ∈ ( Base ‘ 𝑟 ) ( 𝑧 ( .r ‘ 𝑟 ) 𝑥 ) = 𝑦 ) ↔ ( 𝑥 ∈ 𝐵 ∧ ∃ 𝑧 ∈ 𝐵 ( 𝑧 · 𝑥 ) = 𝑦 ) ) )
16	15	opabbidv	⊢ ( 𝑟 = 𝑅 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( Base ‘ 𝑟 ) ∧ ∃ 𝑧 ∈ ( Base ‘ 𝑟 ) ( 𝑧 ( .r ‘ 𝑟 ) 𝑥 ) = 𝑦 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐵 ∧ ∃ 𝑧 ∈ 𝐵 ( 𝑧 · 𝑥 ) = 𝑦 ) } )
17		df-dvdsr	⊢ ∥r = ( 𝑟 ∈ V ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( Base ‘ 𝑟 ) ∧ ∃ 𝑧 ∈ ( Base ‘ 𝑟 ) ( 𝑧 ( .r ‘ 𝑟 ) 𝑥 ) = 𝑦 ) } )
18	1	fvexi	⊢ 𝐵 ∈ V
19		eqcom	⊢ ( ( 𝑧 · 𝑥 ) = 𝑦 ↔ 𝑦 = ( 𝑧 · 𝑥 ) )
20	19	rexbii	⊢ ( ∃ 𝑧 ∈ 𝐵 ( 𝑧 · 𝑥 ) = 𝑦 ↔ ∃ 𝑧 ∈ 𝐵 𝑦 = ( 𝑧 · 𝑥 ) )
21	20	abbii	⊢ { 𝑦 ∣ ∃ 𝑧 ∈ 𝐵 ( 𝑧 · 𝑥 ) = 𝑦 } = { 𝑦 ∣ ∃ 𝑧 ∈ 𝐵 𝑦 = ( 𝑧 · 𝑥 ) }
22	18	abrexex	⊢ { 𝑦 ∣ ∃ 𝑧 ∈ 𝐵 𝑦 = ( 𝑧 · 𝑥 ) } ∈ V
23	21 22	eqeltri	⊢ { 𝑦 ∣ ∃ 𝑧 ∈ 𝐵 ( 𝑧 · 𝑥 ) = 𝑦 } ∈ V
24	23	a1i	⊢ ( 𝑥 ∈ 𝐵 → { 𝑦 ∣ ∃ 𝑧 ∈ 𝐵 ( 𝑧 · 𝑥 ) = 𝑦 } ∈ V )
25	18 24	opabex3	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐵 ∧ ∃ 𝑧 ∈ 𝐵 ( 𝑧 · 𝑥 ) = 𝑦 ) } ∈ V
26	16 17 25	fvmpt	⊢ ( 𝑅 ∈ V → ( ∥r ‘ 𝑅 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐵 ∧ ∃ 𝑧 ∈ 𝐵 ( 𝑧 · 𝑥 ) = 𝑦 ) } )
27	2 26	syl5eq	⊢ ( 𝑅 ∈ V → ∥ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐵 ∧ ∃ 𝑧 ∈ 𝐵 ( 𝑧 · 𝑥 ) = 𝑦 ) } )
28		fvprc	⊢ ( ¬ 𝑅 ∈ V → ( ∥r ‘ 𝑅 ) = ∅ )
29	2 28	syl5eq	⊢ ( ¬ 𝑅 ∈ V → ∥ = ∅ )
30		opabn0	⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐵 ∧ ∃ 𝑧 ∈ 𝐵 ( 𝑧 · 𝑥 ) = 𝑦 ) } ≠ ∅ ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑥 ∈ 𝐵 ∧ ∃ 𝑧 ∈ 𝐵 ( 𝑧 · 𝑥 ) = 𝑦 ) )
31		n0i	⊢ ( 𝑥 ∈ 𝐵 → ¬ 𝐵 = ∅ )
32		fvprc	⊢ ( ¬ 𝑅 ∈ V → ( Base ‘ 𝑅 ) = ∅ )
33	1 32	syl5eq	⊢ ( ¬ 𝑅 ∈ V → 𝐵 = ∅ )
34	31 33	nsyl2	⊢ ( 𝑥 ∈ 𝐵 → 𝑅 ∈ V )
35	34	adantr	⊢ ( ( 𝑥 ∈ 𝐵 ∧ ∃ 𝑧 ∈ 𝐵 ( 𝑧 · 𝑥 ) = 𝑦 ) → 𝑅 ∈ V )
36	35	exlimivv	⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 ∈ 𝐵 ∧ ∃ 𝑧 ∈ 𝐵 ( 𝑧 · 𝑥 ) = 𝑦 ) → 𝑅 ∈ V )
37	30 36	sylbi	⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐵 ∧ ∃ 𝑧 ∈ 𝐵 ( 𝑧 · 𝑥 ) = 𝑦 ) } ≠ ∅ → 𝑅 ∈ V )
38	37	necon1bi	⊢ ( ¬ 𝑅 ∈ V → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐵 ∧ ∃ 𝑧 ∈ 𝐵 ( 𝑧 · 𝑥 ) = 𝑦 ) } = ∅ )
39	29 38	eqtr4d	⊢ ( ¬ 𝑅 ∈ V → ∥ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐵 ∧ ∃ 𝑧 ∈ 𝐵 ( 𝑧 · 𝑥 ) = 𝑦 ) } )
40	27 39	pm2.61i	⊢ ∥ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐵 ∧ ∃ 𝑧 ∈ 𝐵 ( 𝑧 · 𝑥 ) = 𝑦 ) }