Step | Hyp | Ref
| Expression |
1 | | topontop 22285 |
. . 3
β’ (π½ β (TopOnβπ) β π½ β Top) |
2 | | eqid 2733 |
. . . . 5
β’ βͺ π½ =
βͺ π½ |
3 | 2 | ishaus 22696 |
. . . 4
β’ (π½ β Haus β (π½ β Top β§ βπ₯ β βͺ π½βπ¦ β βͺ π½(π₯ β π¦ β βπ β π½ βπ β π½ (π₯ β π β§ π¦ β π β§ (π β© π) = β
)))) |
4 | 3 | baib 537 |
. . 3
β’ (π½ β Top β (π½ β Haus β
βπ₯ β βͺ π½βπ¦ β βͺ π½(π₯ β π¦ β βπ β π½ βπ β π½ (π₯ β π β§ π¦ β π β§ (π β© π) = β
)))) |
5 | 1, 4 | syl 17 |
. 2
β’ (π½ β (TopOnβπ) β (π½ β Haus β βπ₯ β βͺ π½βπ¦ β βͺ π½(π₯ β π¦ β βπ β π½ βπ β π½ (π₯ β π β§ π¦ β π β§ (π β© π) = β
)))) |
6 | | toponuni 22286 |
. . 3
β’ (π½ β (TopOnβπ) β π = βͺ π½) |
7 | 6 | raleqdv 3312 |
. . 3
β’ (π½ β (TopOnβπ) β (βπ¦ β π (π₯ β π¦ β βπ β π½ βπ β π½ (π₯ β π β§ π¦ β π β§ (π β© π) = β
)) β βπ¦ β βͺ π½(π₯ β π¦ β βπ β π½ βπ β π½ (π₯ β π β§ π¦ β π β§ (π β© π) = β
)))) |
8 | 6, 7 | raleqbidv 3318 |
. 2
β’ (π½ β (TopOnβπ) β (βπ₯ β π βπ¦ β π (π₯ β π¦ β βπ β π½ βπ β π½ (π₯ β π β§ π¦ β π β§ (π β© π) = β
)) β βπ₯ β βͺ π½βπ¦ β βͺ π½(π₯ β π¦ β βπ β π½ βπ β π½ (π₯ β π β§ π¦ β π β§ (π β© π) = β
)))) |
9 | 5, 8 | bitr4d 282 |
1
β’ (π½ β (TopOnβπ) β (π½ β Haus β βπ₯ β π βπ¦ β π (π₯ β π¦ β βπ β π½ βπ β π½ (π₯ β π β§ π¦ β π β§ (π β© π) = β
)))) |