| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . . . . . . 8
⊢ dom 𝑅 = dom 𝑅 |
| 2 | 1 | psrn 18620 |
. . . . . . 7
⊢ (𝑅 ∈ PosetRel → dom
𝑅 = ran 𝑅) |
| 3 | 2 | eqcomd 2743 |
. . . . . 6
⊢ (𝑅 ∈ PosetRel → ran
𝑅 = dom 𝑅) |
| 4 | 3 | sneqd 4638 |
. . . . 5
⊢ (𝑅 ∈ PosetRel → {ran
𝑅} = {dom 𝑅}) |
| 5 | | vex 3484 |
. . . . . . . . . . . . 13
⊢ 𝑦 ∈ V |
| 6 | | vex 3484 |
. . . . . . . . . . . . 13
⊢ 𝑥 ∈ V |
| 7 | 5, 6 | brcnv 5893 |
. . . . . . . . . . . 12
⊢ (𝑦◡𝑅𝑥 ↔ 𝑥𝑅𝑦) |
| 8 | 7 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ PosetRel → (𝑦◡𝑅𝑥 ↔ 𝑥𝑅𝑦)) |
| 9 | 8 | notbid 318 |
. . . . . . . . . 10
⊢ (𝑅 ∈ PosetRel → (¬
𝑦◡𝑅𝑥 ↔ ¬ 𝑥𝑅𝑦)) |
| 10 | 3, 9 | rabeqbidv 3455 |
. . . . . . . . 9
⊢ (𝑅 ∈ PosetRel → {𝑦 ∈ ran 𝑅 ∣ ¬ 𝑦◡𝑅𝑥} = {𝑦 ∈ dom 𝑅 ∣ ¬ 𝑥𝑅𝑦}) |
| 11 | 3, 10 | mpteq12dv 5233 |
. . . . . . . 8
⊢ (𝑅 ∈ PosetRel → (𝑥 ∈ ran 𝑅 ↦ {𝑦 ∈ ran 𝑅 ∣ ¬ 𝑦◡𝑅𝑥}) = (𝑥 ∈ dom 𝑅 ↦ {𝑦 ∈ dom 𝑅 ∣ ¬ 𝑥𝑅𝑦})) |
| 12 | 11 | rneqd 5949 |
. . . . . . 7
⊢ (𝑅 ∈ PosetRel → ran
(𝑥 ∈ ran 𝑅 ↦ {𝑦 ∈ ran 𝑅 ∣ ¬ 𝑦◡𝑅𝑥}) = ran (𝑥 ∈ dom 𝑅 ↦ {𝑦 ∈ dom 𝑅 ∣ ¬ 𝑥𝑅𝑦})) |
| 13 | 6, 5 | brcnv 5893 |
. . . . . . . . . . . 12
⊢ (𝑥◡𝑅𝑦 ↔ 𝑦𝑅𝑥) |
| 14 | 13 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ PosetRel → (𝑥◡𝑅𝑦 ↔ 𝑦𝑅𝑥)) |
| 15 | 14 | notbid 318 |
. . . . . . . . . 10
⊢ (𝑅 ∈ PosetRel → (¬
𝑥◡𝑅𝑦 ↔ ¬ 𝑦𝑅𝑥)) |
| 16 | 3, 15 | rabeqbidv 3455 |
. . . . . . . . 9
⊢ (𝑅 ∈ PosetRel → {𝑦 ∈ ran 𝑅 ∣ ¬ 𝑥◡𝑅𝑦} = {𝑦 ∈ dom 𝑅 ∣ ¬ 𝑦𝑅𝑥}) |
| 17 | 3, 16 | mpteq12dv 5233 |
. . . . . . . 8
⊢ (𝑅 ∈ PosetRel → (𝑥 ∈ ran 𝑅 ↦ {𝑦 ∈ ran 𝑅 ∣ ¬ 𝑥◡𝑅𝑦}) = (𝑥 ∈ dom 𝑅 ↦ {𝑦 ∈ dom 𝑅 ∣ ¬ 𝑦𝑅𝑥})) |
| 18 | 17 | rneqd 5949 |
. . . . . . 7
⊢ (𝑅 ∈ PosetRel → ran
(𝑥 ∈ ran 𝑅 ↦ {𝑦 ∈ ran 𝑅 ∣ ¬ 𝑥◡𝑅𝑦}) = ran (𝑥 ∈ dom 𝑅 ↦ {𝑦 ∈ dom 𝑅 ∣ ¬ 𝑦𝑅𝑥})) |
| 19 | 12, 18 | uneq12d 4169 |
. . . . . 6
⊢ (𝑅 ∈ PosetRel → (ran
(𝑥 ∈ ran 𝑅 ↦ {𝑦 ∈ ran 𝑅 ∣ ¬ 𝑦◡𝑅𝑥}) ∪ ran (𝑥 ∈ ran 𝑅 ↦ {𝑦 ∈ ran 𝑅 ∣ ¬ 𝑥◡𝑅𝑦})) = (ran (𝑥 ∈ dom 𝑅 ↦ {𝑦 ∈ dom 𝑅 ∣ ¬ 𝑥𝑅𝑦}) ∪ ran (𝑥 ∈ dom 𝑅 ↦ {𝑦 ∈ dom 𝑅 ∣ ¬ 𝑦𝑅𝑥}))) |
| 20 | | uncom 4158 |
. . . . . 6
⊢ (ran
(𝑥 ∈ dom 𝑅 ↦ {𝑦 ∈ dom 𝑅 ∣ ¬ 𝑥𝑅𝑦}) ∪ ran (𝑥 ∈ dom 𝑅 ↦ {𝑦 ∈ dom 𝑅 ∣ ¬ 𝑦𝑅𝑥})) = (ran (𝑥 ∈ dom 𝑅 ↦ {𝑦 ∈ dom 𝑅 ∣ ¬ 𝑦𝑅𝑥}) ∪ ran (𝑥 ∈ dom 𝑅 ↦ {𝑦 ∈ dom 𝑅 ∣ ¬ 𝑥𝑅𝑦})) |
| 21 | 19, 20 | eqtrdi 2793 |
. . . . 5
⊢ (𝑅 ∈ PosetRel → (ran
(𝑥 ∈ ran 𝑅 ↦ {𝑦 ∈ ran 𝑅 ∣ ¬ 𝑦◡𝑅𝑥}) ∪ ran (𝑥 ∈ ran 𝑅 ↦ {𝑦 ∈ ran 𝑅 ∣ ¬ 𝑥◡𝑅𝑦})) = (ran (𝑥 ∈ dom 𝑅 ↦ {𝑦 ∈ dom 𝑅 ∣ ¬ 𝑦𝑅𝑥}) ∪ ran (𝑥 ∈ dom 𝑅 ↦ {𝑦 ∈ dom 𝑅 ∣ ¬ 𝑥𝑅𝑦}))) |
| 22 | 4, 21 | uneq12d 4169 |
. . . 4
⊢ (𝑅 ∈ PosetRel → ({ran
𝑅} ∪ (ran (𝑥 ∈ ran 𝑅 ↦ {𝑦 ∈ ran 𝑅 ∣ ¬ 𝑦◡𝑅𝑥}) ∪ ran (𝑥 ∈ ran 𝑅 ↦ {𝑦 ∈ ran 𝑅 ∣ ¬ 𝑥◡𝑅𝑦}))) = ({dom 𝑅} ∪ (ran (𝑥 ∈ dom 𝑅 ↦ {𝑦 ∈ dom 𝑅 ∣ ¬ 𝑦𝑅𝑥}) ∪ ran (𝑥 ∈ dom 𝑅 ↦ {𝑦 ∈ dom 𝑅 ∣ ¬ 𝑥𝑅𝑦})))) |
| 23 | 22 | fveq2d 6910 |
. . 3
⊢ (𝑅 ∈ PosetRel →
(fi‘({ran 𝑅} ∪
(ran (𝑥 ∈ ran 𝑅 ↦ {𝑦 ∈ ran 𝑅 ∣ ¬ 𝑦◡𝑅𝑥}) ∪ ran (𝑥 ∈ ran 𝑅 ↦ {𝑦 ∈ ran 𝑅 ∣ ¬ 𝑥◡𝑅𝑦})))) = (fi‘({dom 𝑅} ∪ (ran (𝑥 ∈ dom 𝑅 ↦ {𝑦 ∈ dom 𝑅 ∣ ¬ 𝑦𝑅𝑥}) ∪ ran (𝑥 ∈ dom 𝑅 ↦ {𝑦 ∈ dom 𝑅 ∣ ¬ 𝑥𝑅𝑦}))))) |
| 24 | 23 | fveq2d 6910 |
. 2
⊢ (𝑅 ∈ PosetRel →
(topGen‘(fi‘({ran 𝑅} ∪ (ran (𝑥 ∈ ran 𝑅 ↦ {𝑦 ∈ ran 𝑅 ∣ ¬ 𝑦◡𝑅𝑥}) ∪ ran (𝑥 ∈ ran 𝑅 ↦ {𝑦 ∈ ran 𝑅 ∣ ¬ 𝑥◡𝑅𝑦}))))) = (topGen‘(fi‘({dom 𝑅} ∪ (ran (𝑥 ∈ dom 𝑅 ↦ {𝑦 ∈ dom 𝑅 ∣ ¬ 𝑦𝑅𝑥}) ∪ ran (𝑥 ∈ dom 𝑅 ↦ {𝑦 ∈ dom 𝑅 ∣ ¬ 𝑥𝑅𝑦})))))) |
| 25 | | cnvps 18623 |
. . 3
⊢ (𝑅 ∈ PosetRel → ◡𝑅 ∈ PosetRel) |
| 26 | | df-rn 5696 |
. . . 4
⊢ ran 𝑅 = dom ◡𝑅 |
| 27 | | eqid 2737 |
. . . 4
⊢ ran
(𝑥 ∈ ran 𝑅 ↦ {𝑦 ∈ ran 𝑅 ∣ ¬ 𝑦◡𝑅𝑥}) = ran (𝑥 ∈ ran 𝑅 ↦ {𝑦 ∈ ran 𝑅 ∣ ¬ 𝑦◡𝑅𝑥}) |
| 28 | | eqid 2737 |
. . . 4
⊢ ran
(𝑥 ∈ ran 𝑅 ↦ {𝑦 ∈ ran 𝑅 ∣ ¬ 𝑥◡𝑅𝑦}) = ran (𝑥 ∈ ran 𝑅 ↦ {𝑦 ∈ ran 𝑅 ∣ ¬ 𝑥◡𝑅𝑦}) |
| 29 | 26, 27, 28 | ordtval 23197 |
. . 3
⊢ (◡𝑅 ∈ PosetRel → (ordTop‘◡𝑅) = (topGen‘(fi‘({ran 𝑅} ∪ (ran (𝑥 ∈ ran 𝑅 ↦ {𝑦 ∈ ran 𝑅 ∣ ¬ 𝑦◡𝑅𝑥}) ∪ ran (𝑥 ∈ ran 𝑅 ↦ {𝑦 ∈ ran 𝑅 ∣ ¬ 𝑥◡𝑅𝑦})))))) |
| 30 | 25, 29 | syl 17 |
. 2
⊢ (𝑅 ∈ PosetRel →
(ordTop‘◡𝑅) = (topGen‘(fi‘({ran 𝑅} ∪ (ran (𝑥 ∈ ran 𝑅 ↦ {𝑦 ∈ ran 𝑅 ∣ ¬ 𝑦◡𝑅𝑥}) ∪ ran (𝑥 ∈ ran 𝑅 ↦ {𝑦 ∈ ran 𝑅 ∣ ¬ 𝑥◡𝑅𝑦})))))) |
| 31 | | eqid 2737 |
. . 3
⊢ ran
(𝑥 ∈ dom 𝑅 ↦ {𝑦 ∈ dom 𝑅 ∣ ¬ 𝑦𝑅𝑥}) = ran (𝑥 ∈ dom 𝑅 ↦ {𝑦 ∈ dom 𝑅 ∣ ¬ 𝑦𝑅𝑥}) |
| 32 | | eqid 2737 |
. . 3
⊢ ran
(𝑥 ∈ dom 𝑅 ↦ {𝑦 ∈ dom 𝑅 ∣ ¬ 𝑥𝑅𝑦}) = ran (𝑥 ∈ dom 𝑅 ↦ {𝑦 ∈ dom 𝑅 ∣ ¬ 𝑥𝑅𝑦}) |
| 33 | 1, 31, 32 | ordtval 23197 |
. 2
⊢ (𝑅 ∈ PosetRel →
(ordTop‘𝑅) =
(topGen‘(fi‘({dom 𝑅} ∪ (ran (𝑥 ∈ dom 𝑅 ↦ {𝑦 ∈ dom 𝑅 ∣ ¬ 𝑦𝑅𝑥}) ∪ ran (𝑥 ∈ dom 𝑅 ↦ {𝑦 ∈ dom 𝑅 ∣ ¬ 𝑥𝑅𝑦})))))) |
| 34 | 24, 30, 33 | 3eqtr4d 2787 |
1
⊢ (𝑅 ∈ PosetRel →
(ordTop‘◡𝑅) = (ordTop‘𝑅)) |