| Step | Hyp | Ref
| Expression |
| 1 | | dvdsr.2 |
. . 3
⊢ ∥ =
(∥r‘𝑅) |
| 2 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑟 = 𝑅 → (Base‘𝑟) = (Base‘𝑅)) |
| 3 | | dvdsr.1 |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝑅) |
| 4 | 2, 3 | eqtr4di 2795 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → (Base‘𝑟) = 𝐵) |
| 5 | 4 | eleq2d 2827 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → (𝑥 ∈ (Base‘𝑟) ↔ 𝑥 ∈ 𝐵)) |
| 6 | 4 | rexeqdv 3327 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → (∃𝑧 ∈ (Base‘𝑟)(𝑧(.r‘𝑟)𝑥) = 𝑦 ↔ ∃𝑧 ∈ 𝐵 (𝑧(.r‘𝑟)𝑥) = 𝑦)) |
| 7 | 5, 6 | anbi12d 632 |
. . . . . 6
⊢ (𝑟 = 𝑅 → ((𝑥 ∈ (Base‘𝑟) ∧ ∃𝑧 ∈ (Base‘𝑟)(𝑧(.r‘𝑟)𝑥) = 𝑦) ↔ (𝑥 ∈ 𝐵 ∧ ∃𝑧 ∈ 𝐵 (𝑧(.r‘𝑟)𝑥) = 𝑦))) |
| 8 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑅 → (.r‘𝑟) = (.r‘𝑅)) |
| 9 | | dvdsr.3 |
. . . . . . . . . . 11
⊢ · =
(.r‘𝑅) |
| 10 | 8, 9 | eqtr4di 2795 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑅 → (.r‘𝑟) = · ) |
| 11 | 10 | oveqd 7448 |
. . . . . . . . 9
⊢ (𝑟 = 𝑅 → (𝑧(.r‘𝑟)𝑥) = (𝑧 · 𝑥)) |
| 12 | 11 | eqeq1d 2739 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → ((𝑧(.r‘𝑟)𝑥) = 𝑦 ↔ (𝑧 · 𝑥) = 𝑦)) |
| 13 | 12 | rexbidv 3179 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → (∃𝑧 ∈ 𝐵 (𝑧(.r‘𝑟)𝑥) = 𝑦 ↔ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑥) = 𝑦)) |
| 14 | 13 | anbi2d 630 |
. . . . . 6
⊢ (𝑟 = 𝑅 → ((𝑥 ∈ 𝐵 ∧ ∃𝑧 ∈ 𝐵 (𝑧(.r‘𝑟)𝑥) = 𝑦) ↔ (𝑥 ∈ 𝐵 ∧ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑥) = 𝑦))) |
| 15 | 7, 14 | bitrd 279 |
. . . . 5
⊢ (𝑟 = 𝑅 → ((𝑥 ∈ (Base‘𝑟) ∧ ∃𝑧 ∈ (Base‘𝑟)(𝑧(.r‘𝑟)𝑥) = 𝑦) ↔ (𝑥 ∈ 𝐵 ∧ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑥) = 𝑦))) |
| 16 | 15 | opabbidv 5209 |
. . . 4
⊢ (𝑟 = 𝑅 → {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ (Base‘𝑟) ∧ ∃𝑧 ∈ (Base‘𝑟)(𝑧(.r‘𝑟)𝑥) = 𝑦)} = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐵 ∧ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑥) = 𝑦)}) |
| 17 | | df-dvdsr 20357 |
. . . 4
⊢
∥r = (𝑟 ∈ V ↦ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ (Base‘𝑟) ∧ ∃𝑧 ∈ (Base‘𝑟)(𝑧(.r‘𝑟)𝑥) = 𝑦)}) |
| 18 | 3 | fvexi 6920 |
. . . . 5
⊢ 𝐵 ∈ V |
| 19 | | eqcom 2744 |
. . . . . . . . 9
⊢ ((𝑧 · 𝑥) = 𝑦 ↔ 𝑦 = (𝑧 · 𝑥)) |
| 20 | 19 | rexbii 3094 |
. . . . . . . 8
⊢
(∃𝑧 ∈
𝐵 (𝑧 · 𝑥) = 𝑦 ↔ ∃𝑧 ∈ 𝐵 𝑦 = (𝑧 · 𝑥)) |
| 21 | 20 | abbii 2809 |
. . . . . . 7
⊢ {𝑦 ∣ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑥) = 𝑦} = {𝑦 ∣ ∃𝑧 ∈ 𝐵 𝑦 = (𝑧 · 𝑥)} |
| 22 | 18 | abrexex 7987 |
. . . . . . 7
⊢ {𝑦 ∣ ∃𝑧 ∈ 𝐵 𝑦 = (𝑧 · 𝑥)} ∈ V |
| 23 | 21, 22 | eqeltri 2837 |
. . . . . 6
⊢ {𝑦 ∣ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑥) = 𝑦} ∈ V |
| 24 | 23 | a1i 11 |
. . . . 5
⊢ (𝑥 ∈ 𝐵 → {𝑦 ∣ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑥) = 𝑦} ∈ V) |
| 25 | 18, 24 | opabex3 7992 |
. . . 4
⊢
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐵 ∧ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑥) = 𝑦)} ∈ V |
| 26 | 16, 17, 25 | fvmpt 7016 |
. . 3
⊢ (𝑅 ∈ V →
(∥r‘𝑅) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐵 ∧ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑥) = 𝑦)}) |
| 27 | 1, 26 | eqtrid 2789 |
. 2
⊢ (𝑅 ∈ V → ∥ =
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐵 ∧ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑥) = 𝑦)}) |
| 28 | | fvprc 6898 |
. . . 4
⊢ (¬
𝑅 ∈ V →
(∥r‘𝑅) = ∅) |
| 29 | 1, 28 | eqtrid 2789 |
. . 3
⊢ (¬
𝑅 ∈ V → ∥ =
∅) |
| 30 | | opabn0 5558 |
. . . . 5
⊢
({〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐵 ∧ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑥) = 𝑦)} ≠ ∅ ↔ ∃𝑥∃𝑦(𝑥 ∈ 𝐵 ∧ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑥) = 𝑦)) |
| 31 | | n0i 4340 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐵 → ¬ 𝐵 = ∅) |
| 32 | | fvprc 6898 |
. . . . . . . . 9
⊢ (¬
𝑅 ∈ V →
(Base‘𝑅) =
∅) |
| 33 | 3, 32 | eqtrid 2789 |
. . . . . . . 8
⊢ (¬
𝑅 ∈ V → 𝐵 = ∅) |
| 34 | 31, 33 | nsyl2 141 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐵 → 𝑅 ∈ V) |
| 35 | 34 | adantr 480 |
. . . . . 6
⊢ ((𝑥 ∈ 𝐵 ∧ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑥) = 𝑦) → 𝑅 ∈ V) |
| 36 | 35 | exlimivv 1932 |
. . . . 5
⊢
(∃𝑥∃𝑦(𝑥 ∈ 𝐵 ∧ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑥) = 𝑦) → 𝑅 ∈ V) |
| 37 | 30, 36 | sylbi 217 |
. . . 4
⊢
({〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐵 ∧ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑥) = 𝑦)} ≠ ∅ → 𝑅 ∈ V) |
| 38 | 37 | necon1bi 2969 |
. . 3
⊢ (¬
𝑅 ∈ V →
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐵 ∧ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑥) = 𝑦)} = ∅) |
| 39 | 29, 38 | eqtr4d 2780 |
. 2
⊢ (¬
𝑅 ∈ V → ∥ =
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐵 ∧ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑥) = 𝑦)}) |
| 40 | 27, 39 | pm2.61i 182 |
1
⊢ ∥ =
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐵 ∧ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑥) = 𝑦)} |