Step | Hyp | Ref
| Expression |
1 | | alexsub.1 |
. . . . . . . . 9
β’ (π β π β UFL) |
2 | 1 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π β (UFilβπ) β§ (π½ fLim π) = β
)) β π β UFL) |
3 | | alexsub.2 |
. . . . . . . . 9
β’ (π β π = βͺ π΅) |
4 | 3 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π β (UFilβπ) β§ (π½ fLim π) = β
)) β π = βͺ π΅) |
5 | | alexsub.3 |
. . . . . . . . 9
β’ (π β π½ = (topGenβ(fiβπ΅))) |
6 | 5 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π β (UFilβπ) β§ (π½ fLim π) = β
)) β π½ = (topGenβ(fiβπ΅))) |
7 | | alexsub.4 |
. . . . . . . . 9
β’ ((π β§ (π₯ β π΅ β§ π = βͺ π₯)) β βπ¦ β (π« π₯ β© Fin)π = βͺ π¦) |
8 | 7 | adantlr 714 |
. . . . . . . 8
β’ (((π β§ (π β (UFilβπ) β§ (π½ fLim π) = β
)) β§ (π₯ β π΅ β§ π = βͺ π₯)) β βπ¦ β (π« π₯ β© Fin)π = βͺ π¦) |
9 | | simprl 770 |
. . . . . . . 8
β’ ((π β§ (π β (UFilβπ) β§ (π½ fLim π) = β
)) β π β (UFilβπ)) |
10 | | simprr 772 |
. . . . . . . 8
β’ ((π β§ (π β (UFilβπ) β§ (π½ fLim π) = β
)) β (π½ fLim π) = β
) |
11 | 2, 4, 6, 8, 9, 10 | alexsublem 23418 |
. . . . . . 7
β’ Β¬
(π β§ (π β (UFilβπ) β§ (π½ fLim π) = β
)) |
12 | 11 | pm2.21i 119 |
. . . . . 6
β’ ((π β§ (π β (UFilβπ) β§ (π½ fLim π) = β
)) β Β¬ (π½ fLim π) = β
) |
13 | 12 | expr 458 |
. . . . 5
β’ ((π β§ π β (UFilβπ)) β ((π½ fLim π) = β
β Β¬ (π½ fLim π) = β
)) |
14 | 13 | pm2.01d 189 |
. . . 4
β’ ((π β§ π β (UFilβπ)) β Β¬ (π½ fLim π) = β
) |
15 | 14 | neqned 2947 |
. . 3
β’ ((π β§ π β (UFilβπ)) β (π½ fLim π) β β
) |
16 | 15 | ralrimiva 3140 |
. 2
β’ (π β βπ β (UFilβπ)(π½ fLim π) β β
) |
17 | | fibas 22350 |
. . . . . 6
β’
(fiβπ΅) β
TopBases |
18 | | tgtopon 22344 |
. . . . . 6
β’
((fiβπ΅) β
TopBases β (topGenβ(fiβπ΅)) β (TopOnββͺ (fiβπ΅))) |
19 | 17, 18 | ax-mp 5 |
. . . . 5
β’
(topGenβ(fiβπ΅)) β (TopOnββͺ (fiβπ΅)) |
20 | 5, 19 | eqeltrdi 2842 |
. . . 4
β’ (π β π½ β (TopOnββͺ (fiβπ΅))) |
21 | 1 | elexd 3467 |
. . . . . . . . 9
β’ (π β π β V) |
22 | 3, 21 | eqeltrrd 2835 |
. . . . . . . 8
β’ (π β βͺ π΅
β V) |
23 | | uniexb 7702 |
. . . . . . . 8
β’ (π΅ β V β βͺ π΅
β V) |
24 | 22, 23 | sylibr 233 |
. . . . . . 7
β’ (π β π΅ β V) |
25 | | fiuni 9372 |
. . . . . . 7
β’ (π΅ β V β βͺ π΅ =
βͺ (fiβπ΅)) |
26 | 24, 25 | syl 17 |
. . . . . 6
β’ (π β βͺ π΅ =
βͺ (fiβπ΅)) |
27 | 3, 26 | eqtrd 2773 |
. . . . 5
β’ (π β π = βͺ
(fiβπ΅)) |
28 | 27 | fveq2d 6850 |
. . . 4
β’ (π β (TopOnβπ) = (TopOnββͺ (fiβπ΅))) |
29 | 20, 28 | eleqtrrd 2837 |
. . 3
β’ (π β π½ β (TopOnβπ)) |
30 | | ufilcmp 23406 |
. . 3
β’ ((π β UFL β§ π½ β (TopOnβπ)) β (π½ β Comp β βπ β (UFilβπ)(π½ fLim π) β β
)) |
31 | 1, 29, 30 | syl2anc 585 |
. 2
β’ (π β (π½ β Comp β βπ β (UFilβπ)(π½ fLim π) β β
)) |
32 | 16, 31 | mpbird 257 |
1
β’ (π β π½ β Comp) |