Step | Hyp | Ref
| Expression |
1 | | topontop 22759 |
. . . 4
β’ (π½ β (TopOnβπ) β π½ β Top) |
2 | 1 | 3ad2ant1 1130 |
. . 3
β’ ((π½ β (TopOnβπ) β§ π΄ β π β§ π β π) β π½ β Top) |
3 | | simp2 1134 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ π΄ β π β§ π β π) β π΄ β π) |
4 | | toponuni 22760 |
. . . . 5
β’ (π½ β (TopOnβπ) β π = βͺ π½) |
5 | 4 | 3ad2ant1 1130 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ π΄ β π β§ π β π) β π = βͺ π½) |
6 | 3, 5 | sseqtrd 4015 |
. . 3
β’ ((π½ β (TopOnβπ) β§ π΄ β π β§ π β π) β π΄ β βͺ π½) |
7 | | simp3 1135 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ π΄ β π β§ π β π) β π β π) |
8 | 7, 5 | eleqtrd 2827 |
. . 3
β’ ((π½ β (TopOnβπ) β§ π΄ β π β§ π β π) β π β βͺ π½) |
9 | | eqid 2724 |
. . . 4
β’ βͺ π½ =
βͺ π½ |
10 | 9 | neindisj2 22971 |
. . 3
β’ ((π½ β Top β§ π΄ β βͺ π½
β§ π β βͺ π½)
β (π β
((clsβπ½)βπ΄) β βπ£ β ((neiβπ½)β{π})(π£ β© π΄) β β
)) |
11 | 2, 6, 8, 10 | syl3anc 1368 |
. 2
β’ ((π½ β (TopOnβπ) β§ π΄ β π β§ π β π) β (π β ((clsβπ½)βπ΄) β βπ£ β ((neiβπ½)β{π})(π£ β© π΄) β β
)) |
12 | | simp1 1133 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ π΄ β π β§ π β π) β π½ β (TopOnβπ)) |
13 | 7 | snssd 4805 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ π΄ β π β§ π β π) β {π} β π) |
14 | | snnzg 4771 |
. . . . 5
β’ (π β π β {π} β β
) |
15 | 14 | 3ad2ant3 1132 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ π΄ β π β§ π β π) β {π} β β
) |
16 | | neifil 23728 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ {π} β π β§ {π} β β
) β ((neiβπ½)β{π}) β (Filβπ)) |
17 | 12, 13, 15, 16 | syl3anc 1368 |
. . 3
β’ ((π½ β (TopOnβπ) β§ π΄ β π β§ π β π) β ((neiβπ½)β{π}) β (Filβπ)) |
18 | | trfil2 23735 |
. . 3
β’
((((neiβπ½)β{π}) β (Filβπ) β§ π΄ β π) β ((((neiβπ½)β{π}) βΎt π΄) β (Filβπ΄) β βπ£ β ((neiβπ½)β{π})(π£ β© π΄) β β
)) |
19 | 17, 3, 18 | syl2anc 583 |
. 2
β’ ((π½ β (TopOnβπ) β§ π΄ β π β§ π β π) β ((((neiβπ½)β{π}) βΎt π΄) β (Filβπ΄) β βπ£ β ((neiβπ½)β{π})(π£ β© π΄) β β
)) |
20 | 11, 19 | bitr4d 282 |
1
β’ ((π½ β (TopOnβπ) β§ π΄ β π β§ π β π) β (π β ((clsβπ½)βπ΄) β (((neiβπ½)β{π}) βΎt π΄) β (Filβπ΄))) |