Step | Hyp | Ref
| Expression |
1 | | ufilfil 23278 |
. . . . . 6
β’ (π β (UFilββͺ π½)
β π β
(Filββͺ π½)) |
2 | | eqid 2733 |
. . . . . . 7
β’ βͺ π½ =
βͺ π½ |
3 | 2 | fclscmpi 23403 |
. . . . . 6
β’ ((π½ β Comp β§ π β (Filββͺ π½))
β (π½ fClus π) β β
) |
4 | 1, 3 | sylan2 594 |
. . . . 5
β’ ((π½ β Comp β§ π β (UFilββͺ π½))
β (π½ fClus π) β β
) |
5 | 4 | ralrimiva 3140 |
. . . 4
β’ (π½ β Comp β
βπ β
(UFilββͺ π½)(π½ fClus π) β β
) |
6 | | toponuni 22286 |
. . . . . . 7
β’ (π½ β (TopOnβπ) β π = βͺ π½) |
7 | 6 | fveq2d 6850 |
. . . . . 6
β’ (π½ β (TopOnβπ) β (UFilβπ) = (UFilββͺ π½)) |
8 | 7 | raleqdv 3312 |
. . . . 5
β’ (π½ β (TopOnβπ) β (βπ β (UFilβπ)(π½ fClus π) β β
β βπ β (UFilββͺ π½)(π½ fClus π) β β
)) |
9 | 8 | adantl 483 |
. . . 4
β’ ((π β UFL β§ π½ β (TopOnβπ)) β (βπ β (UFilβπ)(π½ fClus π) β β
β βπ β (UFilββͺ π½)(π½ fClus π) β β
)) |
10 | 5, 9 | syl5ibr 246 |
. . 3
β’ ((π β UFL β§ π½ β (TopOnβπ)) β (π½ β Comp β βπ β (UFilβπ)(π½ fClus π) β β
)) |
11 | | ufli 23288 |
. . . . . . 7
β’ ((π β UFL β§ π β (Filβπ)) β βπ β (UFilβπ)π β π) |
12 | 11 | adantlr 714 |
. . . . . 6
β’ (((π β UFL β§ π½ β (TopOnβπ)) β§ π β (Filβπ)) β βπ β (UFilβπ)π β π) |
13 | | r19.29 3114 |
. . . . . . 7
β’
((βπ β
(UFilβπ)(π½ fClus π) β β
β§ βπ β (UFilβπ)π β π) β βπ β (UFilβπ)((π½ fClus π) β β
β§ π β π)) |
14 | | simpllr 775 |
. . . . . . . . . . . 12
β’ ((((π β UFL β§ π½ β (TopOnβπ)) β§ π β (Filβπ)) β§ (π β (UFilβπ) β§ π β π)) β π½ β (TopOnβπ)) |
15 | | simplr 768 |
. . . . . . . . . . . 12
β’ ((((π β UFL β§ π½ β (TopOnβπ)) β§ π β (Filβπ)) β§ (π β (UFilβπ) β§ π β π)) β π β (Filβπ)) |
16 | | simprr 772 |
. . . . . . . . . . . 12
β’ ((((π β UFL β§ π½ β (TopOnβπ)) β§ π β (Filβπ)) β§ (π β (UFilβπ) β§ π β π)) β π β π) |
17 | | fclsss2 23397 |
. . . . . . . . . . . 12
β’ ((π½ β (TopOnβπ) β§ π β (Filβπ) β§ π β π) β (π½ fClus π) β (π½ fClus π)) |
18 | 14, 15, 16, 17 | syl3anc 1372 |
. . . . . . . . . . 11
β’ ((((π β UFL β§ π½ β (TopOnβπ)) β§ π β (Filβπ)) β§ (π β (UFilβπ) β§ π β π)) β (π½ fClus π) β (π½ fClus π)) |
19 | | ssn0 4364 |
. . . . . . . . . . . 12
β’ (((π½ fClus π) β (π½ fClus π) β§ (π½ fClus π) β β
) β (π½ fClus π) β β
) |
20 | 19 | ex 414 |
. . . . . . . . . . 11
β’ ((π½ fClus π) β (π½ fClus π) β ((π½ fClus π) β β
β (π½ fClus π) β β
)) |
21 | 18, 20 | syl 17 |
. . . . . . . . . 10
β’ ((((π β UFL β§ π½ β (TopOnβπ)) β§ π β (Filβπ)) β§ (π β (UFilβπ) β§ π β π)) β ((π½ fClus π) β β
β (π½ fClus π) β β
)) |
22 | 21 | expr 458 |
. . . . . . . . 9
β’ ((((π β UFL β§ π½ β (TopOnβπ)) β§ π β (Filβπ)) β§ π β (UFilβπ)) β (π β π β ((π½ fClus π) β β
β (π½ fClus π) β β
))) |
23 | 22 | impcomd 413 |
. . . . . . . 8
β’ ((((π β UFL β§ π½ β (TopOnβπ)) β§ π β (Filβπ)) β§ π β (UFilβπ)) β (((π½ fClus π) β β
β§ π β π) β (π½ fClus π) β β
)) |
24 | 23 | rexlimdva 3149 |
. . . . . . 7
β’ (((π β UFL β§ π½ β (TopOnβπ)) β§ π β (Filβπ)) β (βπ β (UFilβπ)((π½ fClus π) β β
β§ π β π) β (π½ fClus π) β β
)) |
25 | 13, 24 | syl5 34 |
. . . . . 6
β’ (((π β UFL β§ π½ β (TopOnβπ)) β§ π β (Filβπ)) β ((βπ β (UFilβπ)(π½ fClus π) β β
β§ βπ β (UFilβπ)π β π) β (π½ fClus π) β β
)) |
26 | 12, 25 | mpan2d 693 |
. . . . 5
β’ (((π β UFL β§ π½ β (TopOnβπ)) β§ π β (Filβπ)) β (βπ β (UFilβπ)(π½ fClus π) β β
β (π½ fClus π) β β
)) |
27 | 26 | ralrimdva 3148 |
. . . 4
β’ ((π β UFL β§ π½ β (TopOnβπ)) β (βπ β (UFilβπ)(π½ fClus π) β β
β βπ β (Filβπ)(π½ fClus π) β β
)) |
28 | | fclscmp 23404 |
. . . . 5
β’ (π½ β (TopOnβπ) β (π½ β Comp β βπ β (Filβπ)(π½ fClus π) β β
)) |
29 | 28 | adantl 483 |
. . . 4
β’ ((π β UFL β§ π½ β (TopOnβπ)) β (π½ β Comp β βπ β (Filβπ)(π½ fClus π) β β
)) |
30 | 27, 29 | sylibrd 259 |
. . 3
β’ ((π β UFL β§ π½ β (TopOnβπ)) β (βπ β (UFilβπ)(π½ fClus π) β β
β π½ β Comp)) |
31 | 10, 30 | impbid 211 |
. 2
β’ ((π β UFL β§ π½ β (TopOnβπ)) β (π½ β Comp β βπ β (UFilβπ)(π½ fClus π) β β
)) |
32 | | uffclsflim 23405 |
. . . 4
β’ (π β (UFilβπ) β (π½ fClus π) = (π½ fLim π)) |
33 | 32 | neeq1d 3000 |
. . 3
β’ (π β (UFilβπ) β ((π½ fClus π) β β
β (π½ fLim π) β β
)) |
34 | 33 | ralbiia 3091 |
. 2
β’
(βπ β
(UFilβπ)(π½ fClus π) β β
β βπ β (UFilβπ)(π½ fLim π) β β
) |
35 | 31, 34 | bitrdi 287 |
1
β’ ((π β UFL β§ π½ β (TopOnβπ)) β (π½ β Comp β βπ β (UFilβπ)(π½ fLim π) β β
)) |