Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . . . . . 8
β’ dom π
= dom π
|
2 | 1 | psrn 18528 |
. . . . . . 7
β’ (π
β PosetRel β dom
π
= ran π
) |
3 | 2 | eqcomd 2739 |
. . . . . 6
β’ (π
β PosetRel β ran
π
= dom π
) |
4 | 3 | sneqd 4641 |
. . . . 5
β’ (π
β PosetRel β {ran
π
} = {dom π
}) |
5 | | vex 3479 |
. . . . . . . . . . . . 13
β’ π¦ β V |
6 | | vex 3479 |
. . . . . . . . . . . . 13
β’ π₯ β V |
7 | 5, 6 | brcnv 5883 |
. . . . . . . . . . . 12
β’ (π¦β‘π
π₯ β π₯π
π¦) |
8 | 7 | a1i 11 |
. . . . . . . . . . 11
β’ (π
β PosetRel β (π¦β‘π
π₯ β π₯π
π¦)) |
9 | 8 | notbid 318 |
. . . . . . . . . 10
β’ (π
β PosetRel β (Β¬
π¦β‘π
π₯ β Β¬ π₯π
π¦)) |
10 | 3, 9 | rabeqbidv 3450 |
. . . . . . . . 9
β’ (π
β PosetRel β {π¦ β ran π
β£ Β¬ π¦β‘π
π₯} = {π¦ β dom π
β£ Β¬ π₯π
π¦}) |
11 | 3, 10 | mpteq12dv 5240 |
. . . . . . . 8
β’ (π
β PosetRel β (π₯ β ran π
β¦ {π¦ β ran π
β£ Β¬ π¦β‘π
π₯}) = (π₯ β dom π
β¦ {π¦ β dom π
β£ Β¬ π₯π
π¦})) |
12 | 11 | rneqd 5938 |
. . . . . . 7
β’ (π
β PosetRel β ran
(π₯ β ran π
β¦ {π¦ β ran π
β£ Β¬ π¦β‘π
π₯}) = ran (π₯ β dom π
β¦ {π¦ β dom π
β£ Β¬ π₯π
π¦})) |
13 | 6, 5 | brcnv 5883 |
. . . . . . . . . . . 12
β’ (π₯β‘π
π¦ β π¦π
π₯) |
14 | 13 | a1i 11 |
. . . . . . . . . . 11
β’ (π
β PosetRel β (π₯β‘π
π¦ β π¦π
π₯)) |
15 | 14 | notbid 318 |
. . . . . . . . . 10
β’ (π
β PosetRel β (Β¬
π₯β‘π
π¦ β Β¬ π¦π
π₯)) |
16 | 3, 15 | rabeqbidv 3450 |
. . . . . . . . 9
β’ (π
β PosetRel β {π¦ β ran π
β£ Β¬ π₯β‘π
π¦} = {π¦ β dom π
β£ Β¬ π¦π
π₯}) |
17 | 3, 16 | mpteq12dv 5240 |
. . . . . . . 8
β’ (π
β PosetRel β (π₯ β ran π
β¦ {π¦ β ran π
β£ Β¬ π₯β‘π
π¦}) = (π₯ β dom π
β¦ {π¦ β dom π
β£ Β¬ π¦π
π₯})) |
18 | 17 | rneqd 5938 |
. . . . . . 7
β’ (π
β PosetRel β ran
(π₯ β ran π
β¦ {π¦ β ran π
β£ Β¬ π₯β‘π
π¦}) = ran (π₯ β dom π
β¦ {π¦ β dom π
β£ Β¬ π¦π
π₯})) |
19 | 12, 18 | uneq12d 4165 |
. . . . . 6
β’ (π
β PosetRel β (ran
(π₯ β ran π
β¦ {π¦ β ran π
β£ Β¬ π¦β‘π
π₯}) βͺ ran (π₯ β ran π
β¦ {π¦ β ran π
β£ Β¬ π₯β‘π
π¦})) = (ran (π₯ β dom π
β¦ {π¦ β dom π
β£ Β¬ π₯π
π¦}) βͺ ran (π₯ β dom π
β¦ {π¦ β dom π
β£ Β¬ π¦π
π₯}))) |
20 | | uncom 4154 |
. . . . . 6
β’ (ran
(π₯ β dom π
β¦ {π¦ β dom π
β£ Β¬ π₯π
π¦}) βͺ ran (π₯ β dom π
β¦ {π¦ β dom π
β£ Β¬ π¦π
π₯})) = (ran (π₯ β dom π
β¦ {π¦ β dom π
β£ Β¬ π¦π
π₯}) βͺ ran (π₯ β dom π
β¦ {π¦ β dom π
β£ Β¬ π₯π
π¦})) |
21 | 19, 20 | eqtrdi 2789 |
. . . . 5
β’ (π
β PosetRel β (ran
(π₯ β ran π
β¦ {π¦ β ran π
β£ Β¬ π¦β‘π
π₯}) βͺ ran (π₯ β ran π
β¦ {π¦ β ran π
β£ Β¬ π₯β‘π
π¦})) = (ran (π₯ β dom π
β¦ {π¦ β dom π
β£ Β¬ π¦π
π₯}) βͺ ran (π₯ β dom π
β¦ {π¦ β dom π
β£ Β¬ π₯π
π¦}))) |
22 | 4, 21 | uneq12d 4165 |
. . . 4
β’ (π
β PosetRel β ({ran
π
} βͺ (ran (π₯ β ran π
β¦ {π¦ β ran π
β£ Β¬ π¦β‘π
π₯}) βͺ ran (π₯ β ran π
β¦ {π¦ β ran π
β£ Β¬ π₯β‘π
π¦}))) = ({dom π
} βͺ (ran (π₯ β dom π
β¦ {π¦ β dom π
β£ Β¬ π¦π
π₯}) βͺ ran (π₯ β dom π
β¦ {π¦ β dom π
β£ Β¬ π₯π
π¦})))) |
23 | 22 | fveq2d 6896 |
. . 3
β’ (π
β PosetRel β
(fiβ({ran π
} βͺ
(ran (π₯ β ran π
β¦ {π¦ β ran π
β£ Β¬ π¦β‘π
π₯}) βͺ ran (π₯ β ran π
β¦ {π¦ β ran π
β£ Β¬ π₯β‘π
π¦})))) = (fiβ({dom π
} βͺ (ran (π₯ β dom π
β¦ {π¦ β dom π
β£ Β¬ π¦π
π₯}) βͺ ran (π₯ β dom π
β¦ {π¦ β dom π
β£ Β¬ π₯π
π¦}))))) |
24 | 23 | fveq2d 6896 |
. 2
β’ (π
β PosetRel β
(topGenβ(fiβ({ran π
} βͺ (ran (π₯ β ran π
β¦ {π¦ β ran π
β£ Β¬ π¦β‘π
π₯}) βͺ ran (π₯ β ran π
β¦ {π¦ β ran π
β£ Β¬ π₯β‘π
π¦}))))) = (topGenβ(fiβ({dom π
} βͺ (ran (π₯ β dom π
β¦ {π¦ β dom π
β£ Β¬ π¦π
π₯}) βͺ ran (π₯ β dom π
β¦ {π¦ β dom π
β£ Β¬ π₯π
π¦})))))) |
25 | | cnvps 18531 |
. . 3
β’ (π
β PosetRel β β‘π
β PosetRel) |
26 | | df-rn 5688 |
. . . 4
β’ ran π
= dom β‘π
|
27 | | eqid 2733 |
. . . 4
β’ ran
(π₯ β ran π
β¦ {π¦ β ran π
β£ Β¬ π¦β‘π
π₯}) = ran (π₯ β ran π
β¦ {π¦ β ran π
β£ Β¬ π¦β‘π
π₯}) |
28 | | eqid 2733 |
. . . 4
β’ ran
(π₯ β ran π
β¦ {π¦ β ran π
β£ Β¬ π₯β‘π
π¦}) = ran (π₯ β ran π
β¦ {π¦ β ran π
β£ Β¬ π₯β‘π
π¦}) |
29 | 26, 27, 28 | ordtval 22693 |
. . 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 2733 |
. . 3
β’ ran
(π₯ β dom π
β¦ {π¦ β dom π
β£ Β¬ π¦π
π₯}) = ran (π₯ β dom π
β¦ {π¦ β dom π
β£ Β¬ π¦π
π₯}) |
32 | | eqid 2733 |
. . 3
β’ ran
(π₯ β dom π
β¦ {π¦ β dom π
β£ Β¬ π₯π
π¦}) = ran (π₯ β dom π
β¦ {π¦ β dom π
β£ Β¬ π₯π
π¦}) |
33 | 1, 31, 32 | ordtval 22693 |
. 2
β’ (π
β PosetRel β
(ordTopβπ
) =
(topGenβ(fiβ({dom π
} βͺ (ran (π₯ β dom π
β¦ {π¦ β dom π
β£ Β¬ π¦π
π₯}) βͺ ran (π₯ β dom π
β¦ {π¦ β dom π
β£ Β¬ π₯π
π¦})))))) |
34 | 24, 30, 33 | 3eqtr4d 2783 |
1
β’ (π
β PosetRel β
(ordTopββ‘π
) = (ordTopβπ
)) |