| Step | Hyp | Ref
| Expression |
|---|
| 1 | | ssrab2 4072 |
. . 3
β’ {π₯ β π β£ ππ
π₯} β π |
| 2 | | ordttopon.3 |
. . . . . 6
β’ π = dom π
|
| 3 | 2 | ordttopon 23052 |
. . . . 5
β’ (π
β π β (ordTopβπ
) β (TopOnβπ)) |
| 4 | 3 | adantr 480 |
. . . 4
β’ ((π
β π β§ π β π) β (ordTopβπ
) β (TopOnβπ)) |
| 5 | | toponuni 22771 |
. . . 4
β’
((ordTopβπ
)
β (TopOnβπ)
β π = βͺ (ordTopβπ
)) |
| 6 | 4, 5 | syl 17 |
. . 3
β’ ((π
β π β§ π β π) β π = βͺ
(ordTopβπ
)) |
| 7 | 1, 6 | sseqtrid 4029 |
. 2
β’ ((π
β π β§ π β π) β {π₯ β π β£ ππ
π₯} β βͺ
(ordTopβπ
)) |
| 8 | | notrab 4306 |
. . . 4
β’ (π β {π₯ β π β£ ππ
π₯}) = {π₯ β π β£ Β¬ ππ
π₯} |
| 9 | 6 | difeq1d 4116 |
. . . 4
β’ ((π
β π β§ π β π) β (π β {π₯ β π β£ ππ
π₯}) = (βͺ
(ordTopβπ
) β
{π₯ β π β£ ππ
π₯})) |
| 10 | 8, 9 | eqtr3id 2780 |
. . 3
β’ ((π
β π β§ π β π) β {π₯ β π β£ Β¬ ππ
π₯} = (βͺ
(ordTopβπ
) β
{π₯ β π β£ ππ
π₯})) |
| 11 | 2 | ordtopn2 23054 |
. . 3
β’ ((π
β π β§ π β π) β {π₯ β π β£ Β¬ ππ
π₯} β (ordTopβπ
)) |
| 12 | 10, 11 | eqeltrrd 2828 |
. 2
β’ ((π
β π β§ π β π) β (βͺ
(ordTopβπ
) β
{π₯ β π β£ ππ
π₯}) β (ordTopβπ
)) |
| 13 | | topontop 22770 |
. . 3
β’
((ordTopβπ
)
β (TopOnβπ)
β (ordTopβπ
)
β Top) |
| 14 | | eqid 2726 |
. . . 4
β’ βͺ (ordTopβπ
) = βͺ
(ordTopβπ
) |
| 15 | 14 | iscld 22886 |
. . 3
β’
((ordTopβπ
)
β Top β ({π₯
β π β£ ππ
π₯} β (Clsdβ(ordTopβπ
)) β ({π₯ β π β£ ππ
π₯} β βͺ
(ordTopβπ
) β§
(βͺ (ordTopβπ
) β {π₯ β π β£ ππ
π₯}) β (ordTopβπ
)))) |
| 16 | 4, 13, 15 | 3syl 18 |
. 2
β’ ((π
β π β§ π β π) β ({π₯ β π β£ ππ
π₯} β (Clsdβ(ordTopβπ
)) β ({π₯ β π β£ ππ
π₯} β βͺ
(ordTopβπ
) β§
(βͺ (ordTopβπ
) β {π₯ β π β£ ππ
π₯}) β (ordTopβπ
)))) |
| 17 | 7, 12, 16 | mpbir2and 710 |
1
β’ ((π
β π β§ π β π) β {π₯ β π β£ ππ
π₯} β (Clsdβ(ordTopβπ
))) |
