Step | Hyp | Ref
| Expression |
1 | | isfcls2 23517 |
. 2
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β (π΄ β (π½ fClus πΉ) β βπ β πΉ π΄ β ((clsβπ½)βπ ))) |
2 | | filn0 23366 |
. . . . . 6
β’ (πΉ β (Filβπ) β πΉ β β
) |
3 | 2 | adantl 483 |
. . . . 5
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β πΉ β β
) |
4 | | r19.2z 4495 |
. . . . . 6
β’ ((πΉ β β
β§
βπ β πΉ π΄ β ((clsβπ½)βπ )) β βπ β πΉ π΄ β ((clsβπ½)βπ )) |
5 | 4 | ex 414 |
. . . . 5
β’ (πΉ β β
β
(βπ β πΉ π΄ β ((clsβπ½)βπ ) β βπ β πΉ π΄ β ((clsβπ½)βπ ))) |
6 | 3, 5 | syl 17 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β (βπ β πΉ π΄ β ((clsβπ½)βπ ) β βπ β πΉ π΄ β ((clsβπ½)βπ ))) |
7 | | topontop 22415 |
. . . . . . . . 9
β’ (π½ β (TopOnβπ) β π½ β Top) |
8 | 7 | ad2antrr 725 |
. . . . . . . 8
β’ (((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β§ π β πΉ) β π½ β Top) |
9 | | filelss 23356 |
. . . . . . . . . 10
β’ ((πΉ β (Filβπ) β§ π β πΉ) β π β π) |
10 | 9 | adantll 713 |
. . . . . . . . 9
β’ (((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β§ π β πΉ) β π β π) |
11 | | toponuni 22416 |
. . . . . . . . . 10
β’ (π½ β (TopOnβπ) β π = βͺ π½) |
12 | 11 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β§ π β πΉ) β π = βͺ π½) |
13 | 10, 12 | sseqtrd 4023 |
. . . . . . . 8
β’ (((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β§ π β πΉ) β π β βͺ π½) |
14 | | eqid 2733 |
. . . . . . . . 9
β’ βͺ π½ =
βͺ π½ |
15 | 14 | clsss3 22563 |
. . . . . . . 8
β’ ((π½ β Top β§ π β βͺ π½)
β ((clsβπ½)βπ ) β βͺ π½) |
16 | 8, 13, 15 | syl2anc 585 |
. . . . . . 7
β’ (((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β§ π β πΉ) β ((clsβπ½)βπ ) β βͺ π½) |
17 | 16, 12 | sseqtrrd 4024 |
. . . . . 6
β’ (((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β§ π β πΉ) β ((clsβπ½)βπ ) β π) |
18 | 17 | sseld 3982 |
. . . . 5
β’ (((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β§ π β πΉ) β (π΄ β ((clsβπ½)βπ ) β π΄ β π)) |
19 | 18 | rexlimdva 3156 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β (βπ β πΉ π΄ β ((clsβπ½)βπ ) β π΄ β π)) |
20 | 6, 19 | syld 47 |
. . 3
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β (βπ β πΉ π΄ β ((clsβπ½)βπ ) β π΄ β π)) |
21 | 20 | pm4.71rd 564 |
. 2
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β (βπ β πΉ π΄ β ((clsβπ½)βπ ) β (π΄ β π β§ βπ β πΉ π΄ β ((clsβπ½)βπ )))) |
22 | 7 | ad3antrrr 729 |
. . . . . 6
β’ ((((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β§ π΄ β π) β§ π β πΉ) β π½ β Top) |
23 | 13 | adantlr 714 |
. . . . . 6
β’ ((((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β§ π΄ β π) β§ π β πΉ) β π β βͺ π½) |
24 | | simplr 768 |
. . . . . . 7
β’ ((((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β§ π΄ β π) β§ π β πΉ) β π΄ β π) |
25 | 11 | ad3antrrr 729 |
. . . . . . 7
β’ ((((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β§ π΄ β π) β§ π β πΉ) β π = βͺ π½) |
26 | 24, 25 | eleqtrd 2836 |
. . . . . 6
β’ ((((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β§ π΄ β π) β§ π β πΉ) β π΄ β βͺ π½) |
27 | 14 | elcls 22577 |
. . . . . 6
β’ ((π½ β Top β§ π β βͺ π½
β§ π΄ β βͺ π½)
β (π΄ β
((clsβπ½)βπ ) β βπ β π½ (π΄ β π β (π β© π ) β β
))) |
28 | 22, 23, 26, 27 | syl3anc 1372 |
. . . . 5
β’ ((((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β§ π΄ β π) β§ π β πΉ) β (π΄ β ((clsβπ½)βπ ) β βπ β π½ (π΄ β π β (π β© π ) β β
))) |
29 | 28 | ralbidva 3176 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β§ π΄ β π) β (βπ β πΉ π΄ β ((clsβπ½)βπ ) β βπ β πΉ βπ β π½ (π΄ β π β (π β© π ) β β
))) |
30 | | ralcom 3287 |
. . . . 5
β’
(βπ β
πΉ βπ β π½ (π΄ β π β (π β© π ) β β
) β βπ β π½ βπ β πΉ (π΄ β π β (π β© π ) β β
)) |
31 | | r19.21v 3180 |
. . . . . 6
β’
(βπ β
πΉ (π΄ β π β (π β© π ) β β
) β (π΄ β π β βπ β πΉ (π β© π ) β β
)) |
32 | 31 | ralbii 3094 |
. . . . 5
β’
(βπ β
π½ βπ β πΉ (π΄ β π β (π β© π ) β β
) β βπ β π½ (π΄ β π β βπ β πΉ (π β© π ) β β
)) |
33 | 30, 32 | bitri 275 |
. . . 4
β’
(βπ β
πΉ βπ β π½ (π΄ β π β (π β© π ) β β
) β βπ β π½ (π΄ β π β βπ β πΉ (π β© π ) β β
)) |
34 | 29, 33 | bitrdi 287 |
. . 3
β’ (((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β§ π΄ β π) β (βπ β πΉ π΄ β ((clsβπ½)βπ ) β βπ β π½ (π΄ β π β βπ β πΉ (π β© π ) β β
))) |
35 | 34 | pm5.32da 580 |
. 2
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β ((π΄ β π β§ βπ β πΉ π΄ β ((clsβπ½)βπ )) β (π΄ β π β§ βπ β π½ (π΄ β π β βπ β πΉ (π β© π ) β β
)))) |
36 | 1, 21, 35 | 3bitrd 305 |
1
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β (π΄ β (π½ fClus πΉ) β (π΄ β π β§ βπ β π½ (π΄ β π β βπ β πΉ (π β© π ) β β
)))) |