Step | Hyp | Ref
| Expression |
1 | | dvdsr.2 |
. . 3
⊢ ∥ =
(∥r‘𝑅) |
2 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑟 = 𝑅 → (Base‘𝑟) = (Base‘𝑅)) |
3 | | dvdsr.1 |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝑅) |
4 | 2, 3 | syl6eqr 2674 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → (Base‘𝑟) = 𝐵) |
5 | 4 | eleq2d 2687 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → (𝑥 ∈ (Base‘𝑟) ↔ 𝑥 ∈ 𝐵)) |
6 | 4 | rexeqdv 3145 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → (∃𝑧 ∈ (Base‘𝑟)(𝑧(.r‘𝑟)𝑥) = 𝑦 ↔ ∃𝑧 ∈ 𝐵 (𝑧(.r‘𝑟)𝑥) = 𝑦)) |
7 | 5, 6 | anbi12d 747 |
. . . . . 6
⊢ (𝑟 = 𝑅 → ((𝑥 ∈ (Base‘𝑟) ∧ ∃𝑧 ∈ (Base‘𝑟)(𝑧(.r‘𝑟)𝑥) = 𝑦) ↔ (𝑥 ∈ 𝐵 ∧ ∃𝑧 ∈ 𝐵 (𝑧(.r‘𝑟)𝑥) = 𝑦))) |
8 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑅 → (.r‘𝑟) = (.r‘𝑅)) |
9 | | dvdsr.3 |
. . . . . . . . . . 11
⊢ · =
(.r‘𝑅) |
10 | 8, 9 | syl6eqr 2674 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑅 → (.r‘𝑟) = · ) |
11 | 10 | oveqd 6667 |
. . . . . . . . 9
⊢ (𝑟 = 𝑅 → (𝑧(.r‘𝑟)𝑥) = (𝑧 · 𝑥)) |
12 | 11 | eqeq1d 2624 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → ((𝑧(.r‘𝑟)𝑥) = 𝑦 ↔ (𝑧 · 𝑥) = 𝑦)) |
13 | 12 | rexbidv 3052 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → (∃𝑧 ∈ 𝐵 (𝑧(.r‘𝑟)𝑥) = 𝑦 ↔ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑥) = 𝑦)) |
14 | 13 | anbi2d 740 |
. . . . . 6
⊢ (𝑟 = 𝑅 → ((𝑥 ∈ 𝐵 ∧ ∃𝑧 ∈ 𝐵 (𝑧(.r‘𝑟)𝑥) = 𝑦) ↔ (𝑥 ∈ 𝐵 ∧ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑥) = 𝑦))) |
15 | 7, 14 | bitrd 268 |
. . . . 5
⊢ (𝑟 = 𝑅 → ((𝑥 ∈ (Base‘𝑟) ∧ ∃𝑧 ∈ (Base‘𝑟)(𝑧(.r‘𝑟)𝑥) = 𝑦) ↔ (𝑥 ∈ 𝐵 ∧ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑥) = 𝑦))) |
16 | 15 | opabbidv 4716 |
. . . 4
⊢ (𝑟 = 𝑅 → {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ (Base‘𝑟) ∧ ∃𝑧 ∈ (Base‘𝑟)(𝑧(.r‘𝑟)𝑥) = 𝑦)} = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐵 ∧ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑥) = 𝑦)}) |
17 | | df-dvdsr 18641 |
. . . 4
⊢
∥r = (𝑟 ∈ V ↦ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ (Base‘𝑟) ∧ ∃𝑧 ∈ (Base‘𝑟)(𝑧(.r‘𝑟)𝑥) = 𝑦)}) |
18 | | fvex 6201 |
. . . . . 6
⊢
(Base‘𝑅)
∈ V |
19 | 3, 18 | eqeltri 2697 |
. . . . 5
⊢ 𝐵 ∈ V |
20 | | eqcom 2629 |
. . . . . . . . 9
⊢ ((𝑧 · 𝑥) = 𝑦 ↔ 𝑦 = (𝑧 · 𝑥)) |
21 | 20 | rexbii 3041 |
. . . . . . . 8
⊢
(∃𝑧 ∈
𝐵 (𝑧 · 𝑥) = 𝑦 ↔ ∃𝑧 ∈ 𝐵 𝑦 = (𝑧 · 𝑥)) |
22 | 21 | abbii 2739 |
. . . . . . 7
⊢ {𝑦 ∣ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑥) = 𝑦} = {𝑦 ∣ ∃𝑧 ∈ 𝐵 𝑦 = (𝑧 · 𝑥)} |
23 | 19 | abrexex 7141 |
. . . . . . 7
⊢ {𝑦 ∣ ∃𝑧 ∈ 𝐵 𝑦 = (𝑧 · 𝑥)} ∈ V |
24 | 22, 23 | eqeltri 2697 |
. . . . . 6
⊢ {𝑦 ∣ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑥) = 𝑦} ∈ V |
25 | 24 | a1i 11 |
. . . . 5
⊢ (𝑥 ∈ 𝐵 → {𝑦 ∣ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑥) = 𝑦} ∈ V) |
26 | 19, 25 | opabex3 7146 |
. . . 4
⊢
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐵 ∧ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑥) = 𝑦)} ∈ V |
27 | 16, 17, 26 | fvmpt 6282 |
. . 3
⊢ (𝑅 ∈ V →
(∥r‘𝑅) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐵 ∧ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑥) = 𝑦)}) |
28 | 1, 27 | syl5eq 2668 |
. 2
⊢ (𝑅 ∈ V → ∥ =
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐵 ∧ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑥) = 𝑦)}) |
29 | | fvprc 6185 |
. . . 4
⊢ (¬
𝑅 ∈ V →
(∥r‘𝑅) = ∅) |
30 | 1, 29 | syl5eq 2668 |
. . 3
⊢ (¬
𝑅 ∈ V → ∥ =
∅) |
31 | | opabn0 5006 |
. . . . 5
⊢
({〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐵 ∧ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑥) = 𝑦)} ≠ ∅ ↔ ∃𝑥∃𝑦(𝑥 ∈ 𝐵 ∧ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑥) = 𝑦)) |
32 | | n0i 3920 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐵 → ¬ 𝐵 = ∅) |
33 | | fvprc 6185 |
. . . . . . . . 9
⊢ (¬
𝑅 ∈ V →
(Base‘𝑅) =
∅) |
34 | 3, 33 | syl5eq 2668 |
. . . . . . . 8
⊢ (¬
𝑅 ∈ V → 𝐵 = ∅) |
35 | 32, 34 | nsyl2 142 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐵 → 𝑅 ∈ V) |
36 | 35 | adantr 481 |
. . . . . 6
⊢ ((𝑥 ∈ 𝐵 ∧ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑥) = 𝑦) → 𝑅 ∈ V) |
37 | 36 | exlimivv 1860 |
. . . . 5
⊢
(∃𝑥∃𝑦(𝑥 ∈ 𝐵 ∧ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑥) = 𝑦) → 𝑅 ∈ V) |
38 | 31, 37 | sylbi 207 |
. . . 4
⊢
({〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐵 ∧ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑥) = 𝑦)} ≠ ∅ → 𝑅 ∈ V) |
39 | 38 | necon1bi 2822 |
. . 3
⊢ (¬
𝑅 ∈ V →
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐵 ∧ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑥) = 𝑦)} = ∅) |
40 | 30, 39 | eqtr4d 2659 |
. 2
⊢ (¬
𝑅 ∈ V → ∥ =
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐵 ∧ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑥) = 𝑦)}) |
41 | 28, 40 | pm2.61i 176 |
1
⊢ ∥ =
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐵 ∧ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑥) = 𝑦)} |