Step | Hyp | Ref
| Expression |
1 | | ordttop 22704 |
. 2
β’ (π
β PosetRel β
(ordTopβπ
) β
Top) |
2 | | snssi 4812 |
. . . . . . . 8
β’ (π₯ β dom π
β {π₯} β dom π
) |
3 | 2 | adantl 483 |
. . . . . . 7
β’ ((π
β PosetRel β§ π₯ β dom π
) β {π₯} β dom π
) |
4 | | sseqin2 4216 |
. . . . . . 7
β’ ({π₯} β dom π
β (dom π
β© {π₯}) = {π₯}) |
5 | 3, 4 | sylib 217 |
. . . . . 6
β’ ((π
β PosetRel β§ π₯ β dom π
) β (dom π
β© {π₯}) = {π₯}) |
6 | | velsn 4645 |
. . . . . . . 8
β’ (π¦ β {π₯} β π¦ = π₯) |
7 | | eqid 2733 |
. . . . . . . . . . . . 13
β’ dom π
= dom π
|
8 | 7 | psref 18527 |
. . . . . . . . . . . 12
β’ ((π
β PosetRel β§ π₯ β dom π
) β π₯π
π₯) |
9 | 8 | adantr 482 |
. . . . . . . . . . 11
β’ (((π
β PosetRel β§ π₯ β dom π
) β§ π¦ β dom π
) β π₯π
π₯) |
10 | 9, 9 | jca 513 |
. . . . . . . . . 10
β’ (((π
β PosetRel β§ π₯ β dom π
) β§ π¦ β dom π
) β (π₯π
π₯ β§ π₯π
π₯)) |
11 | | breq2 5153 |
. . . . . . . . . . 11
β’ (π¦ = π₯ β (π₯π
π¦ β π₯π
π₯)) |
12 | | breq1 5152 |
. . . . . . . . . . 11
β’ (π¦ = π₯ β (π¦π
π₯ β π₯π
π₯)) |
13 | 11, 12 | anbi12d 632 |
. . . . . . . . . 10
β’ (π¦ = π₯ β ((π₯π
π¦ β§ π¦π
π₯) β (π₯π
π₯ β§ π₯π
π₯))) |
14 | 10, 13 | syl5ibrcom 246 |
. . . . . . . . 9
β’ (((π
β PosetRel β§ π₯ β dom π
) β§ π¦ β dom π
) β (π¦ = π₯ β (π₯π
π¦ β§ π¦π
π₯))) |
15 | | psasym 18529 |
. . . . . . . . . . . 12
β’ ((π
β PosetRel β§ π₯π
π¦ β§ π¦π
π₯) β π₯ = π¦) |
16 | 15 | equcomd 2023 |
. . . . . . . . . . 11
β’ ((π
β PosetRel β§ π₯π
π¦ β§ π¦π
π₯) β π¦ = π₯) |
17 | 16 | 3expib 1123 |
. . . . . . . . . 10
β’ (π
β PosetRel β ((π₯π
π¦ β§ π¦π
π₯) β π¦ = π₯)) |
18 | 17 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π
β PosetRel β§ π₯ β dom π
) β§ π¦ β dom π
) β ((π₯π
π¦ β§ π¦π
π₯) β π¦ = π₯)) |
19 | 14, 18 | impbid 211 |
. . . . . . . 8
β’ (((π
β PosetRel β§ π₯ β dom π
) β§ π¦ β dom π
) β (π¦ = π₯ β (π₯π
π¦ β§ π¦π
π₯))) |
20 | 6, 19 | bitrid 283 |
. . . . . . 7
β’ (((π
β PosetRel β§ π₯ β dom π
) β§ π¦ β dom π
) β (π¦ β {π₯} β (π₯π
π¦ β§ π¦π
π₯))) |
21 | 20 | rabbi2dva 4218 |
. . . . . 6
β’ ((π
β PosetRel β§ π₯ β dom π
) β (dom π
β© {π₯}) = {π¦ β dom π
β£ (π₯π
π¦ β§ π¦π
π₯)}) |
22 | 5, 21 | eqtr3d 2775 |
. . . . 5
β’ ((π
β PosetRel β§ π₯ β dom π
) β {π₯} = {π¦ β dom π
β£ (π₯π
π¦ β§ π¦π
π₯)}) |
23 | 7 | ordtcld3 22703 |
. . . . . 6
β’ ((π
β PosetRel β§ π₯ β dom π
β§ π₯ β dom π
) β {π¦ β dom π
β£ (π₯π
π¦ β§ π¦π
π₯)} β (Clsdβ(ordTopβπ
))) |
24 | 23 | 3anidm23 1422 |
. . . . 5
β’ ((π
β PosetRel β§ π₯ β dom π
) β {π¦ β dom π
β£ (π₯π
π¦ β§ π¦π
π₯)} β (Clsdβ(ordTopβπ
))) |
25 | 22, 24 | eqeltrd 2834 |
. . . 4
β’ ((π
β PosetRel β§ π₯ β dom π
) β {π₯} β (Clsdβ(ordTopβπ
))) |
26 | 25 | ralrimiva 3147 |
. . 3
β’ (π
β PosetRel β
βπ₯ β dom π
{π₯} β (Clsdβ(ordTopβπ
))) |
27 | 7 | ordttopon 22697 |
. . . . 5
β’ (π
β PosetRel β
(ordTopβπ
) β
(TopOnβdom π
)) |
28 | | toponuni 22416 |
. . . . 5
β’
((ordTopβπ
)
β (TopOnβdom π
)
β dom π
= βͺ (ordTopβπ
)) |
29 | 27, 28 | syl 17 |
. . . 4
β’ (π
β PosetRel β dom
π
= βͺ (ordTopβπ
)) |
30 | 29 | raleqdv 3326 |
. . 3
β’ (π
β PosetRel β
(βπ₯ β dom π
{π₯} β (Clsdβ(ordTopβπ
)) β βπ₯ β βͺ (ordTopβπ
){π₯} β (Clsdβ(ordTopβπ
)))) |
31 | 26, 30 | mpbid 231 |
. 2
β’ (π
β PosetRel β
βπ₯ β βͺ (ordTopβπ
){π₯} β (Clsdβ(ordTopβπ
))) |
32 | | eqid 2733 |
. . 3
β’ βͺ (ordTopβπ
) = βͺ
(ordTopβπ
) |
33 | 32 | ist1 22825 |
. 2
β’
((ordTopβπ
)
β Fre β ((ordTopβπ
) β Top β§ βπ₯ β βͺ (ordTopβπ
){π₯} β (Clsdβ(ordTopβπ
)))) |
34 | 1, 31, 33 | sylanbrc 584 |
1
β’ (π
β PosetRel β
(ordTopβπ
) β
Fre) |