| Step | Hyp | Ref
| Expression |
|---|
| 1 | | simpr 484 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ π΄ β π) β π΄ β π) |
| 2 | 1 | snssd 4812 |
. . . . 5
β’ ((π½ β (TopOnβπ) β§ π΄ β π) β {π΄} β π) |
| 3 | | snex 5431 |
. . . . . 6
β’ {π΄} β V |
| 4 | 3 | elpw 4606 |
. . . . 5
β’ ({π΄} β π« π β {π΄} β π) |
| 5 | 2, 4 | sylibr 233 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ π΄ β π) β {π΄} β π« π) |
| 6 | | snidg 4662 |
. . . . 5
β’ (π΄ β π β π΄ β {π΄}) |
| 7 | 6 | adantl 481 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ π΄ β π) β π΄ β {π΄}) |
| 8 | | restsn2 22896 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ π΄ β π) β (π½ βΎt {π΄}) = π« {π΄}) |
| 9 | | pwsn 4900 |
. . . . . . 7
β’ π«
{π΄} = {β
, {π΄}} |
| 10 | | indisconn 23143 |
. . . . . . 7
β’ {β
,
{π΄}} β
Conn |
| 11 | 9, 10 | eqeltri 2828 |
. . . . . 6
β’ π«
{π΄} β
Conn |
| 12 | 8, 11 | eqeltrdi 2840 |
. . . . 5
β’ ((π½ β (TopOnβπ) β§ π΄ β π) β (π½ βΎt {π΄}) β Conn) |
| 13 | 7, 12 | jca 511 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ π΄ β π) β (π΄ β {π΄} β§ (π½ βΎt {π΄}) β Conn)) |
| 14 | | eleq2 2821 |
. . . . . 6
β’ (π₯ = {π΄} β (π΄ β π₯ β π΄ β {π΄})) |
| 15 | | oveq2 7420 |
. . . . . . . 8
β’ (π₯ = {π΄} β (π½ βΎt π₯) = (π½ βΎt {π΄})) |
| 16 | 15 | eleq1d 2817 |
. . . . . . 7
β’ (π₯ = {π΄} β ((π½ βΎt π₯) β Conn β (π½ βΎt {π΄}) β Conn)) |
| 17 | 14, 16 | anbi12d 630 |
. . . . . 6
β’ (π₯ = {π΄} β ((π΄ β π₯ β§ (π½ βΎt π₯) β Conn) β (π΄ β {π΄} β§ (π½ βΎt {π΄}) β Conn))) |
| 18 | 14, 17 | anbi12d 630 |
. . . . 5
β’ (π₯ = {π΄} β ((π΄ β π₯ β§ (π΄ β π₯ β§ (π½ βΎt π₯) β Conn)) β (π΄ β {π΄} β§ (π΄ β {π΄} β§ (π½ βΎt {π΄}) β Conn)))) |
| 19 | 18 | rspcev 3612 |
. . . 4
β’ (({π΄} β π« π β§ (π΄ β {π΄} β§ (π΄ β {π΄} β§ (π½ βΎt {π΄}) β Conn))) β βπ₯ β π« π(π΄ β π₯ β§ (π΄ β π₯ β§ (π½ βΎt π₯) β Conn))) |
| 20 | 5, 7, 13, 19 | syl12anc 834 |
. . 3
β’ ((π½ β (TopOnβπ) β§ π΄ β π) β βπ₯ β π« π(π΄ β π₯ β§ (π΄ β π₯ β§ (π½ βΎt π₯) β Conn))) |
| 21 | | elunirab 4924 |
. . 3
β’ (π΄ β βͺ {π₯
β π« π β£
(π΄ β π₯ β§ (π½ βΎt π₯) β Conn)} β βπ₯ β π« π(π΄ β π₯ β§ (π΄ β π₯ β§ (π½ βΎt π₯) β Conn))) |
| 22 | 20, 21 | sylibr 233 |
. 2
β’ ((π½ β (TopOnβπ) β§ π΄ β π) β π΄ β βͺ {π₯ β π« π β£ (π΄ β π₯ β§ (π½ βΎt π₯) β Conn)}) |
| 23 | | conncomp.2 |
. 2
β’ π = βͺ
{π₯ β π« π β£ (π΄ β π₯ β§ (π½ βΎt π₯) β Conn)} |
| 24 | 22, 23 | eleqtrrdi 2843 |
1
β’ ((π½ β (TopOnβπ) β§ π΄ β π) β π΄ β π) |
