| Step | Hyp | Ref
| Expression |
|---|
| 1 | | ssrab2 4077 |
. . 3
β’ {π₯ β π β£ π₯π
π} β π |
| 2 | | ordttopon.3 |
. . . . . 6
β’ π = dom π
|
| 3 | 2 | ordttopon 22918 |
. . . . 5
β’ (π
β π β (ordTopβπ
) β (TopOnβπ)) |
| 4 | 3 | adantr 480 |
. . . 4
β’ ((π
β π β§ π β π) β (ordTopβπ
) β (TopOnβπ)) |
| 5 | | toponuni 22637 |
. . . 4
β’
((ordTopβπ
)
β (TopOnβπ)
β π = βͺ (ordTopβπ
)) |
| 6 | 4, 5 | syl 17 |
. . 3
β’ ((π
β π β§ π β π) β π = βͺ
(ordTopβπ
)) |
| 7 | 1, 6 | sseqtrid 4034 |
. 2
β’ ((π
β π β§ π β π) β {π₯ β π β£ π₯π
π} β βͺ
(ordTopβπ
)) |
| 8 | | notrab 4311 |
. . . 4
β’ (π β {π₯ β π β£ π₯π
π}) = {π₯ β π β£ Β¬ π₯π
π} |
| 9 | 6 | difeq1d 4121 |
. . . 4
β’ ((π
β π β§ π β π) β (π β {π₯ β π β£ π₯π
π}) = (βͺ
(ordTopβπ
) β
{π₯ β π β£ π₯π
π})) |
| 10 | 8, 9 | eqtr3id 2785 |
. . 3
β’ ((π
β π β§ π β π) β {π₯ β π β£ Β¬ π₯π
π} = (βͺ
(ordTopβπ
) β
{π₯ β π β£ π₯π
π})) |
| 11 | 2 | ordtopn1 22919 |
. . 3
β’ ((π
β π β§ π β π) β {π₯ β π β£ Β¬ π₯π
π} β (ordTopβπ
)) |
| 12 | 10, 11 | eqeltrrd 2833 |
. 2
β’ ((π
β π β§ π β π) β (βͺ
(ordTopβπ
) β
{π₯ β π β£ π₯π
π}) β (ordTopβπ
)) |
| 13 | | topontop 22636 |
. . 3
β’
((ordTopβπ
)
β (TopOnβπ)
β (ordTopβπ
)
β Top) |
| 14 | | eqid 2731 |
. . . 4
β’ βͺ (ordTopβπ
) = βͺ
(ordTopβπ
) |
| 15 | 14 | iscld 22752 |
. . 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βπ
))) |
