This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 eqtrid ⊢ ( 𝑅 ∈ V → ∥ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐵 ∧ ∃ 𝑧 ∈ 𝐵 ( 𝑧 · 𝑥 ) = 𝑦 ) } )
28 fvprc ⊢ ( ¬ 𝑅 ∈ V → ( ∥r ‘ 𝑅 ) = ∅ )
29 2 28 eqtrid ⊢ ( ¬ 𝑅 ∈ V → ∥ = ∅ )
30 opabn0 ⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐵 ∧ ∃ 𝑧 ∈ 𝐵 ( 𝑧 · 𝑥 ) = 𝑦 ) } ≠ ∅ ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑥 ∈ 𝐵 ∧ ∃ 𝑧 ∈ 𝐵 ( 𝑧 · 𝑥 ) = 𝑦 ) )
31 n0i ⊢ ( 𝑥 ∈ 𝐵 → ¬ 𝐵 = ∅ )
32 fvprc ⊢ ( ¬ 𝑅 ∈ V → ( Base ‘ 𝑅 ) = ∅ )
33 1 32 eqtrid ⊢ ( ¬ 𝑅 ∈ 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 ⊢ ∥ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐵 ∧ ∃ 𝑧 ∈ 𝐵 ( 𝑧 · 𝑥 ) = 𝑦 ) }