Step | Hyp | Ref
| Expression |
1 | | conncomp.2 |
. . . 4
β’ π = βͺ
{π₯ β π« π β£ (π΄ β π₯ β§ (π½ βΎt π₯) β Conn)} |
2 | | uniiun 5022 |
. . . 4
β’ βͺ {π₯
β π« π β£
(π΄ β π₯ β§ (π½ βΎt π₯) β Conn)} = βͺ π¦ β {π₯ β π« π β£ (π΄ β π₯ β§ (π½ βΎt π₯) β Conn)}π¦ |
3 | 1, 2 | eqtri 2761 |
. . 3
β’ π = βͺ π¦ β {π₯ β π« π β£ (π΄ β π₯ β§ (π½ βΎt π₯) β Conn)}π¦ |
4 | 3 | oveq2i 7372 |
. 2
β’ (π½ βΎt π) = (π½ βΎt βͺ π¦ β {π₯ β π« π β£ (π΄ β π₯ β§ (π½ βΎt π₯) β Conn)}π¦) |
5 | | simpl 484 |
. . 3
β’ ((π½ β (TopOnβπ) β§ π΄ β π) β π½ β (TopOnβπ)) |
6 | | simpr 486 |
. . . . . 6
β’ (((π½ β (TopOnβπ) β§ π΄ β π) β§ π¦ β {π₯ β π« π β£ (π΄ β π₯ β§ (π½ βΎt π₯) β Conn)}) β π¦ β {π₯ β π« π β£ (π΄ β π₯ β§ (π½ βΎt π₯) β Conn)}) |
7 | | eleq2w 2818 |
. . . . . . . 8
β’ (π₯ = π¦ β (π΄ β π₯ β π΄ β π¦)) |
8 | | oveq2 7369 |
. . . . . . . . 9
β’ (π₯ = π¦ β (π½ βΎt π₯) = (π½ βΎt π¦)) |
9 | 8 | eleq1d 2819 |
. . . . . . . 8
β’ (π₯ = π¦ β ((π½ βΎt π₯) β Conn β (π½ βΎt π¦) β Conn)) |
10 | 7, 9 | anbi12d 632 |
. . . . . . 7
β’ (π₯ = π¦ β ((π΄ β π₯ β§ (π½ βΎt π₯) β Conn) β (π΄ β π¦ β§ (π½ βΎt π¦) β Conn))) |
11 | 10 | elrab 3649 |
. . . . . 6
β’ (π¦ β {π₯ β π« π β£ (π΄ β π₯ β§ (π½ βΎt π₯) β Conn)} β (π¦ β π« π β§ (π΄ β π¦ β§ (π½ βΎt π¦) β Conn))) |
12 | 6, 11 | sylib 217 |
. . . . 5
β’ (((π½ β (TopOnβπ) β§ π΄ β π) β§ π¦ β {π₯ β π« π β£ (π΄ β π₯ β§ (π½ βΎt π₯) β Conn)}) β (π¦ β π« π β§ (π΄ β π¦ β§ (π½ βΎt π¦) β Conn))) |
13 | 12 | simpld 496 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ π΄ β π) β§ π¦ β {π₯ β π« π β£ (π΄ β π₯ β§ (π½ βΎt π₯) β Conn)}) β π¦ β π« π) |
14 | 13 | elpwid 4573 |
. . 3
β’ (((π½ β (TopOnβπ) β§ π΄ β π) β§ π¦ β {π₯ β π« π β£ (π΄ β π₯ β§ (π½ βΎt π₯) β Conn)}) β π¦ β π) |
15 | 12 | simprd 497 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ π΄ β π) β§ π¦ β {π₯ β π« π β£ (π΄ β π₯ β§ (π½ βΎt π₯) β Conn)}) β (π΄ β π¦ β§ (π½ βΎt π¦) β Conn)) |
16 | 15 | simpld 496 |
. . 3
β’ (((π½ β (TopOnβπ) β§ π΄ β π) β§ π¦ β {π₯ β π« π β£ (π΄ β π₯ β§ (π½ βΎt π₯) β Conn)}) β π΄ β π¦) |
17 | 15 | simprd 497 |
. . 3
β’ (((π½ β (TopOnβπ) β§ π΄ β π) β§ π¦ β {π₯ β π« π β£ (π΄ β π₯ β§ (π½ βΎt π₯) β Conn)}) β (π½ βΎt π¦) β Conn) |
18 | 5, 14, 16, 17 | iunconn 22802 |
. 2
β’ ((π½ β (TopOnβπ) β§ π΄ β π) β (π½ βΎt βͺ π¦ β {π₯ β π« π β£ (π΄ β π₯ β§ (π½ βΎt π₯) β Conn)}π¦) β Conn) |
19 | 4, 18 | eqeltrid 2838 |
1
β’ ((π½ β (TopOnβπ) β§ π΄ β π) β (π½ βΎt π) β Conn) |