Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . . 5
β’ βͺ π½ =
βͺ π½ |
2 | 1 | fclscmpi 23403 |
. . . 4
β’ ((π½ β Comp β§ π β (Filββͺ π½))
β (π½ fClus π) β β
) |
3 | 2 | ralrimiva 3140 |
. . 3
β’ (π½ β Comp β
βπ β
(Filββͺ π½)(π½ fClus π) β β
) |
4 | | toponuni 22286 |
. . . . 5
β’ (π½ β (TopOnβπ) β π = βͺ π½) |
5 | 4 | fveq2d 6850 |
. . . 4
β’ (π½ β (TopOnβπ) β (Filβπ) = (Filββͺ π½)) |
6 | 5 | raleqdv 3312 |
. . 3
β’ (π½ β (TopOnβπ) β (βπ β (Filβπ)(π½ fClus π) β β
β βπ β (Filββͺ π½)(π½ fClus π) β β
)) |
7 | 3, 6 | syl5ibr 246 |
. 2
β’ (π½ β (TopOnβπ) β (π½ β Comp β βπ β (Filβπ)(π½ fClus π) β β
)) |
8 | | elpwi 4571 |
. . . . . 6
β’ (π₯ β π«
(Clsdβπ½) β π₯ β (Clsdβπ½)) |
9 | | vn0 4302 |
. . . . . . . . . 10
β’ V β
β
|
10 | | simpr 486 |
. . . . . . . . . . . . 13
β’ (((π½ β (TopOnβπ) β§ (π₯ β (Clsdβπ½) β§ Β¬ β
β (fiβπ₯))) β§ π₯ = β
) β π₯ = β
) |
11 | 10 | inteqd 4916 |
. . . . . . . . . . . 12
β’ (((π½ β (TopOnβπ) β§ (π₯ β (Clsdβπ½) β§ Β¬ β
β (fiβπ₯))) β§ π₯ = β
) β β© π₯ =
β© β
) |
12 | | int0 4927 |
. . . . . . . . . . . 12
β’ β© β
= V |
13 | 11, 12 | eqtrdi 2789 |
. . . . . . . . . . 11
β’ (((π½ β (TopOnβπ) β§ (π₯ β (Clsdβπ½) β§ Β¬ β
β (fiβπ₯))) β§ π₯ = β
) β β© π₯ =
V) |
14 | 13 | neeq1d 3000 |
. . . . . . . . . 10
β’ (((π½ β (TopOnβπ) β§ (π₯ β (Clsdβπ½) β§ Β¬ β
β (fiβπ₯))) β§ π₯ = β
) β (β© π₯
β β
β V β β
)) |
15 | 9, 14 | mpbiri 258 |
. . . . . . . . 9
β’ (((π½ β (TopOnβπ) β§ (π₯ β (Clsdβπ½) β§ Β¬ β
β (fiβπ₯))) β§ π₯ = β
) β β© π₯
β β
) |
16 | 15 | a1d 25 |
. . . . . . . 8
β’ (((π½ β (TopOnβπ) β§ (π₯ β (Clsdβπ½) β§ Β¬ β
β (fiβπ₯))) β§ π₯ = β
) β (βπ β (Filβπ)(π½ fClus π) β β
β β© π₯
β β
)) |
17 | | ssfii 9363 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β V β π₯ β (fiβπ₯)) |
18 | 17 | elv 3453 |
. . . . . . . . . . . . . . 15
β’ π₯ β (fiβπ₯) |
19 | | simplrl 776 |
. . . . . . . . . . . . . . . . . 18
β’ (((π½ β (TopOnβπ) β§ (π₯ β (Clsdβπ½) β§ Β¬ β
β (fiβπ₯))) β§ π₯ β β
) β π₯ β (Clsdβπ½)) |
20 | 1 | cldss2 22404 |
. . . . . . . . . . . . . . . . . . 19
β’
(Clsdβπ½)
β π« βͺ π½ |
21 | 4 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π½ β (TopOnβπ) β§ (π₯ β (Clsdβπ½) β§ Β¬ β
β (fiβπ₯))) β§ π₯ β β
) β π = βͺ π½) |
22 | 21 | pweqd 4581 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π½ β (TopOnβπ) β§ (π₯ β (Clsdβπ½) β§ Β¬ β
β (fiβπ₯))) β§ π₯ β β
) β π« π = π« βͺ π½) |
23 | 20, 22 | sseqtrrid 4001 |
. . . . . . . . . . . . . . . . . 18
β’ (((π½ β (TopOnβπ) β§ (π₯ β (Clsdβπ½) β§ Β¬ β
β (fiβπ₯))) β§ π₯ β β
) β (Clsdβπ½) β π« π) |
24 | 19, 23 | sstrd 3958 |
. . . . . . . . . . . . . . . . 17
β’ (((π½ β (TopOnβπ) β§ (π₯ β (Clsdβπ½) β§ Β¬ β
β (fiβπ₯))) β§ π₯ β β
) β π₯ β π« π) |
25 | | simpr 486 |
. . . . . . . . . . . . . . . . 17
β’ (((π½ β (TopOnβπ) β§ (π₯ β (Clsdβπ½) β§ Β¬ β
β (fiβπ₯))) β§ π₯ β β
) β π₯ β β
) |
26 | | simplrr 777 |
. . . . . . . . . . . . . . . . 17
β’ (((π½ β (TopOnβπ) β§ (π₯ β (Clsdβπ½) β§ Β¬ β
β (fiβπ₯))) β§ π₯ β β
) β Β¬ β
β
(fiβπ₯)) |
27 | | toponmax 22298 |
. . . . . . . . . . . . . . . . . . 19
β’ (π½ β (TopOnβπ) β π β π½) |
28 | 27 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’ (((π½ β (TopOnβπ) β§ (π₯ β (Clsdβπ½) β§ Β¬ β
β (fiβπ₯))) β§ π₯ β β
) β π β π½) |
29 | | fsubbas 23241 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π½ β ((fiβπ₯) β (fBasβπ) β (π₯ β π« π β§ π₯ β β
β§ Β¬ β
β
(fiβπ₯)))) |
30 | 28, 29 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (((π½ β (TopOnβπ) β§ (π₯ β (Clsdβπ½) β§ Β¬ β
β (fiβπ₯))) β§ π₯ β β
) β ((fiβπ₯) β (fBasβπ) β (π₯ β π« π β§ π₯ β β
β§ Β¬ β
β
(fiβπ₯)))) |
31 | 24, 25, 26, 30 | mpbir3and 1343 |
. . . . . . . . . . . . . . . 16
β’ (((π½ β (TopOnβπ) β§ (π₯ β (Clsdβπ½) β§ Β¬ β
β (fiβπ₯))) β§ π₯ β β
) β (fiβπ₯) β (fBasβπ)) |
32 | | ssfg 23246 |
. . . . . . . . . . . . . . . 16
β’
((fiβπ₯) β
(fBasβπ) β
(fiβπ₯) β (πfilGen(fiβπ₯))) |
33 | 31, 32 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (((π½ β (TopOnβπ) β§ (π₯ β (Clsdβπ½) β§ Β¬ β
β (fiβπ₯))) β§ π₯ β β
) β (fiβπ₯) β (πfilGen(fiβπ₯))) |
34 | 18, 33 | sstrid 3959 |
. . . . . . . . . . . . . 14
β’ (((π½ β (TopOnβπ) β§ (π₯ β (Clsdβπ½) β§ Β¬ β
β (fiβπ₯))) β§ π₯ β β
) β π₯ β (πfilGen(fiβπ₯))) |
35 | 34 | sselda 3948 |
. . . . . . . . . . . . 13
β’ ((((π½ β (TopOnβπ) β§ (π₯ β (Clsdβπ½) β§ Β¬ β
β (fiβπ₯))) β§ π₯ β β
) β§ π¦ β π₯) β π¦ β (πfilGen(fiβπ₯))) |
36 | | fclssscls 23392 |
. . . . . . . . . . . . 13
β’ (π¦ β (πfilGen(fiβπ₯)) β (π½ fClus (πfilGen(fiβπ₯))) β ((clsβπ½)βπ¦)) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . . 12
β’ ((((π½ β (TopOnβπ) β§ (π₯ β (Clsdβπ½) β§ Β¬ β
β (fiβπ₯))) β§ π₯ β β
) β§ π¦ β π₯) β (π½ fClus (πfilGen(fiβπ₯))) β ((clsβπ½)βπ¦)) |
38 | 19 | sselda 3948 |
. . . . . . . . . . . . 13
β’ ((((π½ β (TopOnβπ) β§ (π₯ β (Clsdβπ½) β§ Β¬ β
β (fiβπ₯))) β§ π₯ β β
) β§ π¦ β π₯) β π¦ β (Clsdβπ½)) |
39 | | cldcls 22416 |
. . . . . . . . . . . . 13
β’ (π¦ β (Clsdβπ½) β ((clsβπ½)βπ¦) = π¦) |
40 | 38, 39 | syl 17 |
. . . . . . . . . . . 12
β’ ((((π½ β (TopOnβπ) β§ (π₯ β (Clsdβπ½) β§ Β¬ β
β (fiβπ₯))) β§ π₯ β β
) β§ π¦ β π₯) β ((clsβπ½)βπ¦) = π¦) |
41 | 37, 40 | sseqtrd 3988 |
. . . . . . . . . . 11
β’ ((((π½ β (TopOnβπ) β§ (π₯ β (Clsdβπ½) β§ Β¬ β
β (fiβπ₯))) β§ π₯ β β
) β§ π¦ β π₯) β (π½ fClus (πfilGen(fiβπ₯))) β π¦) |
42 | 41 | ralrimiva 3140 |
. . . . . . . . . 10
β’ (((π½ β (TopOnβπ) β§ (π₯ β (Clsdβπ½) β§ Β¬ β
β (fiβπ₯))) β§ π₯ β β
) β βπ¦ β π₯ (π½ fClus (πfilGen(fiβπ₯))) β π¦) |
43 | | ssint 4929 |
. . . . . . . . . 10
β’ ((π½ fClus (πfilGen(fiβπ₯))) β β©
π₯ β βπ¦ β π₯ (π½ fClus (πfilGen(fiβπ₯))) β π¦) |
44 | 42, 43 | sylibr 233 |
. . . . . . . . 9
β’ (((π½ β (TopOnβπ) β§ (π₯ β (Clsdβπ½) β§ Β¬ β
β (fiβπ₯))) β§ π₯ β β
) β (π½ fClus (πfilGen(fiβπ₯))) β β©
π₯) |
45 | | fgcl 23252 |
. . . . . . . . . 10
β’
((fiβπ₯) β
(fBasβπ) β
(πfilGen(fiβπ₯)) β (Filβπ)) |
46 | | oveq2 7369 |
. . . . . . . . . . . 12
β’ (π = (πfilGen(fiβπ₯)) β (π½ fClus π) = (π½ fClus (πfilGen(fiβπ₯)))) |
47 | 46 | neeq1d 3000 |
. . . . . . . . . . 11
β’ (π = (πfilGen(fiβπ₯)) β ((π½ fClus π) β β
β (π½ fClus (πfilGen(fiβπ₯))) β β
)) |
48 | 47 | rspcv 3579 |
. . . . . . . . . 10
β’ ((πfilGen(fiβπ₯)) β (Filβπ) β (βπ β (Filβπ)(π½ fClus π) β β
β (π½ fClus (πfilGen(fiβπ₯))) β β
)) |
49 | 31, 45, 48 | 3syl 18 |
. . . . . . . . 9
β’ (((π½ β (TopOnβπ) β§ (π₯ β (Clsdβπ½) β§ Β¬ β
β (fiβπ₯))) β§ π₯ β β
) β (βπ β (Filβπ)(π½ fClus π) β β
β (π½ fClus (πfilGen(fiβπ₯))) β β
)) |
50 | | ssn0 4364 |
. . . . . . . . 9
β’ (((π½ fClus (πfilGen(fiβπ₯))) β β©
π₯ β§ (π½ fClus (πfilGen(fiβπ₯))) β β
) β β© π₯
β β
) |
51 | 44, 49, 50 | syl6an 683 |
. . . . . . . 8
β’ (((π½ β (TopOnβπ) β§ (π₯ β (Clsdβπ½) β§ Β¬ β
β (fiβπ₯))) β§ π₯ β β
) β (βπ β (Filβπ)(π½ fClus π) β β
β β© π₯
β β
)) |
52 | 16, 51 | pm2.61dane 3029 |
. . . . . . 7
β’ ((π½ β (TopOnβπ) β§ (π₯ β (Clsdβπ½) β§ Β¬ β
β (fiβπ₯))) β (βπ β (Filβπ)(π½ fClus π) β β
β β© π₯
β β
)) |
53 | 52 | expr 458 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ π₯ β (Clsdβπ½)) β (Β¬ β
β
(fiβπ₯) β
(βπ β
(Filβπ)(π½ fClus π) β β
β β© π₯
β β
))) |
54 | 8, 53 | sylan2 594 |
. . . . 5
β’ ((π½ β (TopOnβπ) β§ π₯ β π« (Clsdβπ½)) β (Β¬ β
β
(fiβπ₯) β
(βπ β
(Filβπ)(π½ fClus π) β β
β β© π₯
β β
))) |
55 | 54 | com23 86 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ π₯ β π« (Clsdβπ½)) β (βπ β (Filβπ)(π½ fClus π) β β
β (Β¬ β
β
(fiβπ₯) β β© π₯
β β
))) |
56 | 55 | ralrimdva 3148 |
. . 3
β’ (π½ β (TopOnβπ) β (βπ β (Filβπ)(π½ fClus π) β β
β βπ₯ β π«
(Clsdβπ½)(Β¬
β
β (fiβπ₯)
β β© π₯ β β
))) |
57 | | topontop 22285 |
. . . 4
β’ (π½ β (TopOnβπ) β π½ β Top) |
58 | | cmpfi 22782 |
. . . 4
β’ (π½ β Top β (π½ β Comp β
βπ₯ β π«
(Clsdβπ½)(Β¬
β
β (fiβπ₯)
β β© π₯ β β
))) |
59 | 57, 58 | syl 17 |
. . 3
β’ (π½ β (TopOnβπ) β (π½ β Comp β βπ₯ β π«
(Clsdβπ½)(Β¬
β
β (fiβπ₯)
β β© π₯ β β
))) |
60 | 56, 59 | sylibrd 259 |
. 2
β’ (π½ β (TopOnβπ) β (βπ β (Filβπ)(π½ fClus π) β β
β π½ β Comp)) |
61 | 7, 60 | impbid 211 |
1
β’ (π½ β (TopOnβπ) β (π½ β Comp β βπ β (Filβπ)(π½ fClus π) β β
)) |