Step | Hyp | Ref
| Expression |
1 | | topontop 22285 |
. . . . 5
β’ (π½ β (TopOnβπ) β π½ β Top) |
2 | | conncomp.2 |
. . . . . . 7
β’ π = βͺ
{π₯ β π« π β£ (π΄ β π₯ β§ (π½ βΎt π₯) β Conn)} |
3 | | ssrab2 4041 |
. . . . . . . 8
β’ {π₯ β π« π β£ (π΄ β π₯ β§ (π½ βΎt π₯) β Conn)} β π« π |
4 | | sspwuni 5064 |
. . . . . . . 8
β’ ({π₯ β π« π β£ (π΄ β π₯ β§ (π½ βΎt π₯) β Conn)} β π« π β βͺ {π₯
β π« π β£
(π΄ β π₯ β§ (π½ βΎt π₯) β Conn)} β π) |
5 | 3, 4 | mpbi 229 |
. . . . . . 7
β’ βͺ {π₯
β π« π β£
(π΄ β π₯ β§ (π½ βΎt π₯) β Conn)} β π |
6 | 2, 5 | eqsstri 3982 |
. . . . . 6
β’ π β π |
7 | | toponuni 22286 |
. . . . . . 7
β’ (π½ β (TopOnβπ) β π = βͺ π½) |
8 | 7 | adantr 482 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ π΄ β π) β π = βͺ π½) |
9 | 6, 8 | sseqtrid 4000 |
. . . . 5
β’ ((π½ β (TopOnβπ) β§ π΄ β π) β π β βͺ π½) |
10 | | eqid 2733 |
. . . . . 6
β’ βͺ π½ =
βͺ π½ |
11 | 10 | clsss3 22433 |
. . . . 5
β’ ((π½ β Top β§ π β βͺ π½)
β ((clsβπ½)βπ) β βͺ π½) |
12 | 1, 9, 11 | syl2an2r 684 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ π΄ β π) β ((clsβπ½)βπ) β βͺ π½) |
13 | 12, 8 | sseqtrrd 3989 |
. . 3
β’ ((π½ β (TopOnβπ) β§ π΄ β π) β ((clsβπ½)βπ) β π) |
14 | 10 | sscls 22430 |
. . . . 5
β’ ((π½ β Top β§ π β βͺ π½)
β π β
((clsβπ½)βπ)) |
15 | 1, 9, 14 | syl2an2r 684 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ π΄ β π) β π β ((clsβπ½)βπ)) |
16 | 2 | conncompid 22805 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ π΄ β π) β π΄ β π) |
17 | 15, 16 | sseldd 3949 |
. . 3
β’ ((π½ β (TopOnβπ) β§ π΄ β π) β π΄ β ((clsβπ½)βπ)) |
18 | | simpl 484 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ π΄ β π) β π½ β (TopOnβπ)) |
19 | 6 | a1i 11 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ π΄ β π) β π β π) |
20 | 2 | conncompconn 22806 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ π΄ β π) β (π½ βΎt π) β Conn) |
21 | | clsconn 22804 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ π β π β§ (π½ βΎt π) β Conn) β (π½ βΎt ((clsβπ½)βπ)) β Conn) |
22 | 18, 19, 20, 21 | syl3anc 1372 |
. . 3
β’ ((π½ β (TopOnβπ) β§ π΄ β π) β (π½ βΎt ((clsβπ½)βπ)) β Conn) |
23 | 2 | conncompss 22807 |
. . 3
β’
((((clsβπ½)βπ) β π β§ π΄ β ((clsβπ½)βπ) β§ (π½ βΎt ((clsβπ½)βπ)) β Conn) β ((clsβπ½)βπ) β π) |
24 | 13, 17, 22, 23 | syl3anc 1372 |
. 2
β’ ((π½ β (TopOnβπ) β§ π΄ β π) β ((clsβπ½)βπ) β π) |
25 | 10 | iscld4 22439 |
. . 3
β’ ((π½ β Top β§ π β βͺ π½)
β (π β
(Clsdβπ½) β
((clsβπ½)βπ) β π)) |
26 | 1, 9, 25 | syl2an2r 684 |
. 2
β’ ((π½ β (TopOnβπ) β§ π΄ β π) β (π β (Clsdβπ½) β ((clsβπ½)βπ) β π)) |
27 | 24, 26 | mpbird 257 |
1
β’ ((π½ β (TopOnβπ) β§ π΄ β π) β π β (Clsdβπ½)) |