| Step | Hyp | Ref
| Expression |
| 1 | | elfvdm 6943 |
. . . 4
⊢ (𝑋 ∈ (Irred‘𝑅) → 𝑅 ∈ dom Irred) |
| 2 | | irred.3 |
. . . 4
⊢ 𝐼 = (Irred‘𝑅) |
| 3 | 1, 2 | eleq2s 2859 |
. . 3
⊢ (𝑋 ∈ 𝐼 → 𝑅 ∈ dom Irred) |
| 4 | 3 | elexd 3504 |
. 2
⊢ (𝑋 ∈ 𝐼 → 𝑅 ∈ V) |
| 5 | | eldifi 4131 |
. . . . . 6
⊢ (𝑋 ∈ (𝐵 ∖ 𝑈) → 𝑋 ∈ 𝐵) |
| 6 | | irred.4 |
. . . . . 6
⊢ 𝑁 = (𝐵 ∖ 𝑈) |
| 7 | 5, 6 | eleq2s 2859 |
. . . . 5
⊢ (𝑋 ∈ 𝑁 → 𝑋 ∈ 𝐵) |
| 8 | | irred.1 |
. . . . 5
⊢ 𝐵 = (Base‘𝑅) |
| 9 | 7, 8 | eleqtrdi 2851 |
. . . 4
⊢ (𝑋 ∈ 𝑁 → 𝑋 ∈ (Base‘𝑅)) |
| 10 | 9 | elfvexd 6945 |
. . 3
⊢ (𝑋 ∈ 𝑁 → 𝑅 ∈ V) |
| 11 | 10 | adantr 480 |
. 2
⊢ ((𝑋 ∈ 𝑁 ∧ ∀𝑥 ∈ 𝑁 ∀𝑦 ∈ 𝑁 (𝑥 · 𝑦) ≠ 𝑋) → 𝑅 ∈ V) |
| 12 | | fvex 6919 |
. . . . . . . 8
⊢
(Base‘𝑟)
∈ V |
| 13 | | difexg 5329 |
. . . . . . . 8
⊢
((Base‘𝑟)
∈ V → ((Base‘𝑟) ∖ (Unit‘𝑟)) ∈ V) |
| 14 | 12, 13 | mp1i 13 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → ((Base‘𝑟) ∖ (Unit‘𝑟)) ∈ V) |
| 15 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → 𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) |
| 16 | | simpl 482 |
. . . . . . . . . . . . 13
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → 𝑟 = 𝑅) |
| 17 | 16 | fveq2d 6910 |
. . . . . . . . . . . 12
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → (Base‘𝑟) = (Base‘𝑅)) |
| 18 | 17, 8 | eqtr4di 2795 |
. . . . . . . . . . 11
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → (Base‘𝑟) = 𝐵) |
| 19 | 16 | fveq2d 6910 |
. . . . . . . . . . . 12
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → (Unit‘𝑟) = (Unit‘𝑅)) |
| 20 | | irred.2 |
. . . . . . . . . . . 12
⊢ 𝑈 = (Unit‘𝑅) |
| 21 | 19, 20 | eqtr4di 2795 |
. . . . . . . . . . 11
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → (Unit‘𝑟) = 𝑈) |
| 22 | 18, 21 | difeq12d 4127 |
. . . . . . . . . 10
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → ((Base‘𝑟) ∖ (Unit‘𝑟)) = (𝐵 ∖ 𝑈)) |
| 23 | 22, 6 | eqtr4di 2795 |
. . . . . . . . 9
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → ((Base‘𝑟) ∖ (Unit‘𝑟)) = 𝑁) |
| 24 | 15, 23 | eqtrd 2777 |
. . . . . . . 8
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → 𝑏 = 𝑁) |
| 25 | 16 | fveq2d 6910 |
. . . . . . . . . . . . 13
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → (.r‘𝑟) = (.r‘𝑅)) |
| 26 | | irred.5 |
. . . . . . . . . . . . 13
⊢ · =
(.r‘𝑅) |
| 27 | 25, 26 | eqtr4di 2795 |
. . . . . . . . . . . 12
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → (.r‘𝑟) = · ) |
| 28 | 27 | oveqd 7448 |
. . . . . . . . . . 11
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → (𝑥(.r‘𝑟)𝑦) = (𝑥 · 𝑦)) |
| 29 | 28 | neeq1d 3000 |
. . . . . . . . . 10
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → ((𝑥(.r‘𝑟)𝑦) ≠ 𝑧 ↔ (𝑥 · 𝑦) ≠ 𝑧)) |
| 30 | 24, 29 | raleqbidv 3346 |
. . . . . . . . 9
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → (∀𝑦 ∈ 𝑏 (𝑥(.r‘𝑟)𝑦) ≠ 𝑧 ↔ ∀𝑦 ∈ 𝑁 (𝑥 · 𝑦) ≠ 𝑧)) |
| 31 | 24, 30 | raleqbidv 3346 |
. . . . . . . 8
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → (∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥(.r‘𝑟)𝑦) ≠ 𝑧 ↔ ∀𝑥 ∈ 𝑁 ∀𝑦 ∈ 𝑁 (𝑥 · 𝑦) ≠ 𝑧)) |
| 32 | 24, 31 | rabeqbidv 3455 |
. . . . . . 7
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → {𝑧 ∈ 𝑏 ∣ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥(.r‘𝑟)𝑦) ≠ 𝑧} = {𝑧 ∈ 𝑁 ∣ ∀𝑥 ∈ 𝑁 ∀𝑦 ∈ 𝑁 (𝑥 · 𝑦) ≠ 𝑧}) |
| 33 | 14, 32 | csbied 3935 |
. . . . . 6
⊢ (𝑟 = 𝑅 → ⦋((Base‘𝑟) ∖ (Unit‘𝑟)) / 𝑏⦌{𝑧 ∈ 𝑏 ∣ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥(.r‘𝑟)𝑦) ≠ 𝑧} = {𝑧 ∈ 𝑁 ∣ ∀𝑥 ∈ 𝑁 ∀𝑦 ∈ 𝑁 (𝑥 · 𝑦) ≠ 𝑧}) |
| 34 | | df-irred 20359 |
. . . . . 6
⊢ Irred =
(𝑟 ∈ V ↦
⦋((Base‘𝑟) ∖ (Unit‘𝑟)) / 𝑏⦌{𝑧 ∈ 𝑏 ∣ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥(.r‘𝑟)𝑦) ≠ 𝑧}) |
| 35 | | fvex 6919 |
. . . . . . . . . 10
⊢
(Base‘𝑅)
∈ V |
| 36 | 8, 35 | eqeltri 2837 |
. . . . . . . . 9
⊢ 𝐵 ∈ V |
| 37 | 36 | difexi 5330 |
. . . . . . . 8
⊢ (𝐵 ∖ 𝑈) ∈ V |
| 38 | 6, 37 | eqeltri 2837 |
. . . . . . 7
⊢ 𝑁 ∈ V |
| 39 | 38 | rabex 5339 |
. . . . . 6
⊢ {𝑧 ∈ 𝑁 ∣ ∀𝑥 ∈ 𝑁 ∀𝑦 ∈ 𝑁 (𝑥 · 𝑦) ≠ 𝑧} ∈ V |
| 40 | 33, 34, 39 | fvmpt 7016 |
. . . . 5
⊢ (𝑅 ∈ V →
(Irred‘𝑅) = {𝑧 ∈ 𝑁 ∣ ∀𝑥 ∈ 𝑁 ∀𝑦 ∈ 𝑁 (𝑥 · 𝑦) ≠ 𝑧}) |
| 41 | 2, 40 | eqtrid 2789 |
. . . 4
⊢ (𝑅 ∈ V → 𝐼 = {𝑧 ∈ 𝑁 ∣ ∀𝑥 ∈ 𝑁 ∀𝑦 ∈ 𝑁 (𝑥 · 𝑦) ≠ 𝑧}) |
| 42 | 41 | eleq2d 2827 |
. . 3
⊢ (𝑅 ∈ V → (𝑋 ∈ 𝐼 ↔ 𝑋 ∈ {𝑧 ∈ 𝑁 ∣ ∀𝑥 ∈ 𝑁 ∀𝑦 ∈ 𝑁 (𝑥 · 𝑦) ≠ 𝑧})) |
| 43 | | neeq2 3004 |
. . . . 5
⊢ (𝑧 = 𝑋 → ((𝑥 · 𝑦) ≠ 𝑧 ↔ (𝑥 · 𝑦) ≠ 𝑋)) |
| 44 | 43 | 2ralbidv 3221 |
. . . 4
⊢ (𝑧 = 𝑋 → (∀𝑥 ∈ 𝑁 ∀𝑦 ∈ 𝑁 (𝑥 · 𝑦) ≠ 𝑧 ↔ ∀𝑥 ∈ 𝑁 ∀𝑦 ∈ 𝑁 (𝑥 · 𝑦) ≠ 𝑋)) |
| 45 | 44 | elrab 3692 |
. . 3
⊢ (𝑋 ∈ {𝑧 ∈ 𝑁 ∣ ∀𝑥 ∈ 𝑁 ∀𝑦 ∈ 𝑁 (𝑥 · 𝑦) ≠ 𝑧} ↔ (𝑋 ∈ 𝑁 ∧ ∀𝑥 ∈ 𝑁 ∀𝑦 ∈ 𝑁 (𝑥 · 𝑦) ≠ 𝑋)) |
| 46 | 42, 45 | bitrdi 287 |
. 2
⊢ (𝑅 ∈ V → (𝑋 ∈ 𝐼 ↔ (𝑋 ∈ 𝑁 ∧ ∀𝑥 ∈ 𝑁 ∀𝑦 ∈ 𝑁 (𝑥 · 𝑦) ≠ 𝑋))) |
| 47 | 4, 11, 46 | pm5.21nii 378 |
1
⊢ (𝑋 ∈ 𝐼 ↔ (𝑋 ∈ 𝑁 ∧ ∀𝑥 ∈ 𝑁 ∀𝑦 ∈ 𝑁 (𝑥 · 𝑦) ≠ 𝑋)) |