| Step | Hyp | Ref
| Expression |
| 1 | | elex 3501 |
. 2
⊢ (𝑅 ∈ 𝑉 → 𝑅 ∈ V) |
| 2 | | dmeq 5914 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → dom 𝑟 = dom 𝑅) |
| 3 | | ordtval.1 |
. . . . . . . 8
⊢ 𝑋 = dom 𝑅 |
| 4 | 2, 3 | eqtr4di 2795 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → dom 𝑟 = 𝑋) |
| 5 | 4 | sneqd 4638 |
. . . . . 6
⊢ (𝑟 = 𝑅 → {dom 𝑟} = {𝑋}) |
| 6 | | rnun 6165 |
. . . . . . 7
⊢ ran
((𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥}) ∪ (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦})) = (ran (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥}) ∪ ran (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦})) |
| 7 | | breq 5145 |
. . . . . . . . . . . . 13
⊢ (𝑟 = 𝑅 → (𝑦𝑟𝑥 ↔ 𝑦𝑅𝑥)) |
| 8 | 7 | notbid 318 |
. . . . . . . . . . . 12
⊢ (𝑟 = 𝑅 → (¬ 𝑦𝑟𝑥 ↔ ¬ 𝑦𝑅𝑥)) |
| 9 | 4, 8 | rabeqbidv 3455 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑅 → {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥} = {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥}) |
| 10 | 4, 9 | mpteq12dv 5233 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑅 → (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥}) = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥})) |
| 11 | 10 | rneqd 5949 |
. . . . . . . . 9
⊢ (𝑟 = 𝑅 → ran (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥}) = ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥})) |
| 12 | | ordtval.2 |
. . . . . . . . 9
⊢ 𝐴 = ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥}) |
| 13 | 11, 12 | eqtr4di 2795 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → ran (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥}) = 𝐴) |
| 14 | | breq 5145 |
. . . . . . . . . . . . 13
⊢ (𝑟 = 𝑅 → (𝑥𝑟𝑦 ↔ 𝑥𝑅𝑦)) |
| 15 | 14 | notbid 318 |
. . . . . . . . . . . 12
⊢ (𝑟 = 𝑅 → (¬ 𝑥𝑟𝑦 ↔ ¬ 𝑥𝑅𝑦)) |
| 16 | 4, 15 | rabeqbidv 3455 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑅 → {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦} = {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦}) |
| 17 | 4, 16 | mpteq12dv 5233 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑅 → (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦}) = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦})) |
| 18 | 17 | rneqd 5949 |
. . . . . . . . 9
⊢ (𝑟 = 𝑅 → ran (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦}) = ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦})) |
| 19 | | ordtval.3 |
. . . . . . . . 9
⊢ 𝐵 = ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦}) |
| 20 | 18, 19 | eqtr4di 2795 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → ran (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦}) = 𝐵) |
| 21 | 13, 20 | uneq12d 4169 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → (ran (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥}) ∪ ran (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦})) = (𝐴 ∪ 𝐵)) |
| 22 | 6, 21 | eqtrid 2789 |
. . . . . 6
⊢ (𝑟 = 𝑅 → ran ((𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥}) ∪ (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦})) = (𝐴 ∪ 𝐵)) |
| 23 | 5, 22 | uneq12d 4169 |
. . . . 5
⊢ (𝑟 = 𝑅 → ({dom 𝑟} ∪ ran ((𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥}) ∪ (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦}))) = ({𝑋} ∪ (𝐴 ∪ 𝐵))) |
| 24 | 23 | fveq2d 6910 |
. . . 4
⊢ (𝑟 = 𝑅 → (fi‘({dom 𝑟} ∪ ran ((𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥}) ∪ (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦})))) = (fi‘({𝑋} ∪ (𝐴 ∪ 𝐵)))) |
| 25 | 24 | fveq2d 6910 |
. . 3
⊢ (𝑟 = 𝑅 → (topGen‘(fi‘({dom 𝑟} ∪ ran ((𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥}) ∪ (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦}))))) = (topGen‘(fi‘({𝑋} ∪ (𝐴 ∪ 𝐵))))) |
| 26 | | df-ordt 17546 |
. . 3
⊢ ordTop =
(𝑟 ∈ V ↦
(topGen‘(fi‘({dom 𝑟} ∪ ran ((𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥}) ∪ (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦})))))) |
| 27 | | fvex 6919 |
. . 3
⊢
(topGen‘(fi‘({𝑋} ∪ (𝐴 ∪ 𝐵)))) ∈ V |
| 28 | 25, 26, 27 | fvmpt 7016 |
. 2
⊢ (𝑅 ∈ V →
(ordTop‘𝑅) =
(topGen‘(fi‘({𝑋} ∪ (𝐴 ∪ 𝐵))))) |
| 29 | 1, 28 | syl 17 |
1
⊢ (𝑅 ∈ 𝑉 → (ordTop‘𝑅) = (topGen‘(fi‘({𝑋} ∪ (𝐴 ∪ 𝐵))))) |