Step | Hyp | Ref
| Expression |
1 | | filsspw 23346 |
. . . . . . . 8
β’ (πΉ β (Filβπ) β πΉ β π« π) |
2 | 1 | adantr 481 |
. . . . . . 7
β’ ((πΉ β (Filβπ) β§ π΄ β (π½ fClus πΉ)) β πΉ β π« π) |
3 | | fclstop 23506 |
. . . . . . . . . 10
β’ (π΄ β (π½ fClus πΉ) β π½ β Top) |
4 | 3 | adantl 482 |
. . . . . . . . 9
β’ ((πΉ β (Filβπ) β§ π΄ β (π½ fClus πΉ)) β π½ β Top) |
5 | | eqid 2732 |
. . . . . . . . . 10
β’ βͺ π½ =
βͺ π½ |
6 | 5 | neisspw 22602 |
. . . . . . . . 9
β’ (π½ β Top β
((neiβπ½)β{π΄}) β π« βͺ π½) |
7 | 4, 6 | syl 17 |
. . . . . . . 8
β’ ((πΉ β (Filβπ) β§ π΄ β (π½ fClus πΉ)) β ((neiβπ½)β{π΄}) β π« βͺ π½) |
8 | | filunibas 23376 |
. . . . . . . . . 10
β’ (πΉ β (Filβπ) β βͺ πΉ =
π) |
9 | 5 | fclsfil 23505 |
. . . . . . . . . . 11
β’ (π΄ β (π½ fClus πΉ) β πΉ β (Filββͺ π½)) |
10 | | filunibas 23376 |
. . . . . . . . . . 11
β’ (πΉ β (Filββͺ π½)
β βͺ πΉ = βͺ π½) |
11 | 9, 10 | syl 17 |
. . . . . . . . . 10
β’ (π΄ β (π½ fClus πΉ) β βͺ πΉ = βͺ
π½) |
12 | 8, 11 | sylan9req 2793 |
. . . . . . . . 9
β’ ((πΉ β (Filβπ) β§ π΄ β (π½ fClus πΉ)) β π = βͺ π½) |
13 | 12 | pweqd 4618 |
. . . . . . . 8
β’ ((πΉ β (Filβπ) β§ π΄ β (π½ fClus πΉ)) β π« π = π« βͺ
π½) |
14 | 7, 13 | sseqtrrd 4022 |
. . . . . . 7
β’ ((πΉ β (Filβπ) β§ π΄ β (π½ fClus πΉ)) β ((neiβπ½)β{π΄}) β π« π) |
15 | 2, 14 | unssd 4185 |
. . . . . 6
β’ ((πΉ β (Filβπ) β§ π΄ β (π½ fClus πΉ)) β (πΉ βͺ ((neiβπ½)β{π΄})) β π« π) |
16 | | ssun1 4171 |
. . . . . . . 8
β’ πΉ β (πΉ βͺ ((neiβπ½)β{π΄})) |
17 | | filn0 23357 |
. . . . . . . 8
β’ (πΉ β (Filβπ) β πΉ β β
) |
18 | | ssn0 4399 |
. . . . . . . 8
β’ ((πΉ β (πΉ βͺ ((neiβπ½)β{π΄})) β§ πΉ β β
) β (πΉ βͺ ((neiβπ½)β{π΄})) β β
) |
19 | 16, 17, 18 | sylancr 587 |
. . . . . . 7
β’ (πΉ β (Filβπ) β (πΉ βͺ ((neiβπ½)β{π΄})) β β
) |
20 | 19 | adantr 481 |
. . . . . 6
β’ ((πΉ β (Filβπ) β§ π΄ β (π½ fClus πΉ)) β (πΉ βͺ ((neiβπ½)β{π΄})) β β
) |
21 | | incom 4200 |
. . . . . . . . . . . 12
β’ (π¦ β© π₯) = (π₯ β© π¦) |
22 | | fclsneii 23512 |
. . . . . . . . . . . 12
β’ ((π΄ β (π½ fClus πΉ) β§ π¦ β ((neiβπ½)β{π΄}) β§ π₯ β πΉ) β (π¦ β© π₯) β β
) |
23 | 21, 22 | eqnetrrid 3016 |
. . . . . . . . . . 11
β’ ((π΄ β (π½ fClus πΉ) β§ π¦ β ((neiβπ½)β{π΄}) β§ π₯ β πΉ) β (π₯ β© π¦) β β
) |
24 | 23 | 3com23 1126 |
. . . . . . . . . 10
β’ ((π΄ β (π½ fClus πΉ) β§ π₯ β πΉ β§ π¦ β ((neiβπ½)β{π΄})) β (π₯ β© π¦) β β
) |
25 | 24 | 3expb 1120 |
. . . . . . . . 9
β’ ((π΄ β (π½ fClus πΉ) β§ (π₯ β πΉ β§ π¦ β ((neiβπ½)β{π΄}))) β (π₯ β© π¦) β β
) |
26 | 25 | adantll 712 |
. . . . . . . 8
β’ (((πΉ β (Filβπ) β§ π΄ β (π½ fClus πΉ)) β§ (π₯ β πΉ β§ π¦ β ((neiβπ½)β{π΄}))) β (π₯ β© π¦) β β
) |
27 | 26 | ralrimivva 3200 |
. . . . . . 7
β’ ((πΉ β (Filβπ) β§ π΄ β (π½ fClus πΉ)) β βπ₯ β πΉ βπ¦ β ((neiβπ½)β{π΄})(π₯ β© π¦) β β
) |
28 | | filfbas 23343 |
. . . . . . . . 9
β’ (πΉ β (Filβπ) β πΉ β (fBasβπ)) |
29 | 28 | adantr 481 |
. . . . . . . 8
β’ ((πΉ β (Filβπ) β§ π΄ β (π½ fClus πΉ)) β πΉ β (fBasβπ)) |
30 | | istopon 22405 |
. . . . . . . . . . 11
β’ (π½ β (TopOnβπ) β (π½ β Top β§ π = βͺ π½)) |
31 | 4, 12, 30 | sylanbrc 583 |
. . . . . . . . . 10
β’ ((πΉ β (Filβπ) β§ π΄ β (π½ fClus πΉ)) β π½ β (TopOnβπ)) |
32 | 5 | fclselbas 23511 |
. . . . . . . . . . . . 13
β’ (π΄ β (π½ fClus πΉ) β π΄ β βͺ π½) |
33 | 32 | adantl 482 |
. . . . . . . . . . . 12
β’ ((πΉ β (Filβπ) β§ π΄ β (π½ fClus πΉ)) β π΄ β βͺ π½) |
34 | 33, 12 | eleqtrrd 2836 |
. . . . . . . . . . 11
β’ ((πΉ β (Filβπ) β§ π΄ β (π½ fClus πΉ)) β π΄ β π) |
35 | 34 | snssd 4811 |
. . . . . . . . . 10
β’ ((πΉ β (Filβπ) β§ π΄ β (π½ fClus πΉ)) β {π΄} β π) |
36 | | snnzg 4777 |
. . . . . . . . . . 11
β’ (π΄ β (π½ fClus πΉ) β {π΄} β β
) |
37 | 36 | adantl 482 |
. . . . . . . . . 10
β’ ((πΉ β (Filβπ) β§ π΄ β (π½ fClus πΉ)) β {π΄} β β
) |
38 | | neifil 23375 |
. . . . . . . . . 10
β’ ((π½ β (TopOnβπ) β§ {π΄} β π β§ {π΄} β β
) β ((neiβπ½)β{π΄}) β (Filβπ)) |
39 | 31, 35, 37, 38 | syl3anc 1371 |
. . . . . . . . 9
β’ ((πΉ β (Filβπ) β§ π΄ β (π½ fClus πΉ)) β ((neiβπ½)β{π΄}) β (Filβπ)) |
40 | | filfbas 23343 |
. . . . . . . . 9
β’
(((neiβπ½)β{π΄}) β (Filβπ) β ((neiβπ½)β{π΄}) β (fBasβπ)) |
41 | 39, 40 | syl 17 |
. . . . . . . 8
β’ ((πΉ β (Filβπ) β§ π΄ β (π½ fClus πΉ)) β ((neiβπ½)β{π΄}) β (fBasβπ)) |
42 | | fbunfip 23364 |
. . . . . . . 8
β’ ((πΉ β (fBasβπ) β§ ((neiβπ½)β{π΄}) β (fBasβπ)) β (Β¬ β
β
(fiβ(πΉ βͺ
((neiβπ½)β{π΄}))) β βπ₯ β πΉ βπ¦ β ((neiβπ½)β{π΄})(π₯ β© π¦) β β
)) |
43 | 29, 41, 42 | syl2anc 584 |
. . . . . . 7
β’ ((πΉ β (Filβπ) β§ π΄ β (π½ fClus πΉ)) β (Β¬ β
β
(fiβ(πΉ βͺ
((neiβπ½)β{π΄}))) β βπ₯ β πΉ βπ¦ β ((neiβπ½)β{π΄})(π₯ β© π¦) β β
)) |
44 | 27, 43 | mpbird 256 |
. . . . . 6
β’ ((πΉ β (Filβπ) β§ π΄ β (π½ fClus πΉ)) β Β¬ β
β
(fiβ(πΉ βͺ
((neiβπ½)β{π΄})))) |
45 | | filtop 23350 |
. . . . . . . 8
β’ (πΉ β (Filβπ) β π β πΉ) |
46 | | fsubbas 23362 |
. . . . . . . 8
β’ (π β πΉ β ((fiβ(πΉ βͺ ((neiβπ½)β{π΄}))) β (fBasβπ) β ((πΉ βͺ ((neiβπ½)β{π΄})) β π« π β§ (πΉ βͺ ((neiβπ½)β{π΄})) β β
β§ Β¬ β
β
(fiβ(πΉ βͺ
((neiβπ½)β{π΄})))))) |
47 | 45, 46 | syl 17 |
. . . . . . 7
β’ (πΉ β (Filβπ) β ((fiβ(πΉ βͺ ((neiβπ½)β{π΄}))) β (fBasβπ) β ((πΉ βͺ ((neiβπ½)β{π΄})) β π« π β§ (πΉ βͺ ((neiβπ½)β{π΄})) β β
β§ Β¬ β
β
(fiβ(πΉ βͺ
((neiβπ½)β{π΄})))))) |
48 | 47 | adantr 481 |
. . . . . 6
β’ ((πΉ β (Filβπ) β§ π΄ β (π½ fClus πΉ)) β ((fiβ(πΉ βͺ ((neiβπ½)β{π΄}))) β (fBasβπ) β ((πΉ βͺ ((neiβπ½)β{π΄})) β π« π β§ (πΉ βͺ ((neiβπ½)β{π΄})) β β
β§ Β¬ β
β
(fiβ(πΉ βͺ
((neiβπ½)β{π΄})))))) |
49 | 15, 20, 44, 48 | mpbir3and 1342 |
. . . . 5
β’ ((πΉ β (Filβπ) β§ π΄ β (π½ fClus πΉ)) β (fiβ(πΉ βͺ ((neiβπ½)β{π΄}))) β (fBasβπ)) |
50 | | fgcl 23373 |
. . . . 5
β’
((fiβ(πΉ βͺ
((neiβπ½)β{π΄}))) β (fBasβπ) β (πfilGen(fiβ(πΉ βͺ ((neiβπ½)β{π΄})))) β (Filβπ)) |
51 | 49, 50 | syl 17 |
. . . 4
β’ ((πΉ β (Filβπ) β§ π΄ β (π½ fClus πΉ)) β (πfilGen(fiβ(πΉ βͺ ((neiβπ½)β{π΄})))) β (Filβπ)) |
52 | | fvex 6901 |
. . . . . . . . 9
β’
((neiβπ½)β{π΄}) β V |
53 | | unexg 7732 |
. . . . . . . . 9
β’ ((πΉ β (Filβπ) β§ ((neiβπ½)β{π΄}) β V) β (πΉ βͺ ((neiβπ½)β{π΄})) β V) |
54 | 52, 53 | mpan2 689 |
. . . . . . . 8
β’ (πΉ β (Filβπ) β (πΉ βͺ ((neiβπ½)β{π΄})) β V) |
55 | | ssfii 9410 |
. . . . . . . 8
β’ ((πΉ βͺ ((neiβπ½)β{π΄})) β V β (πΉ βͺ ((neiβπ½)β{π΄})) β (fiβ(πΉ βͺ ((neiβπ½)β{π΄})))) |
56 | 54, 55 | syl 17 |
. . . . . . 7
β’ (πΉ β (Filβπ) β (πΉ βͺ ((neiβπ½)β{π΄})) β (fiβ(πΉ βͺ ((neiβπ½)β{π΄})))) |
57 | 56 | adantr 481 |
. . . . . 6
β’ ((πΉ β (Filβπ) β§ π΄ β (π½ fClus πΉ)) β (πΉ βͺ ((neiβπ½)β{π΄})) β (fiβ(πΉ βͺ ((neiβπ½)β{π΄})))) |
58 | 57 | unssad 4186 |
. . . . 5
β’ ((πΉ β (Filβπ) β§ π΄ β (π½ fClus πΉ)) β πΉ β (fiβ(πΉ βͺ ((neiβπ½)β{π΄})))) |
59 | | ssfg 23367 |
. . . . . 6
β’
((fiβ(πΉ βͺ
((neiβπ½)β{π΄}))) β (fBasβπ) β (fiβ(πΉ βͺ ((neiβπ½)β{π΄}))) β (πfilGen(fiβ(πΉ βͺ ((neiβπ½)β{π΄}))))) |
60 | 49, 59 | syl 17 |
. . . . 5
β’ ((πΉ β (Filβπ) β§ π΄ β (π½ fClus πΉ)) β (fiβ(πΉ βͺ ((neiβπ½)β{π΄}))) β (πfilGen(fiβ(πΉ βͺ ((neiβπ½)β{π΄}))))) |
61 | 58, 60 | sstrd 3991 |
. . . 4
β’ ((πΉ β (Filβπ) β§ π΄ β (π½ fClus πΉ)) β πΉ β (πfilGen(fiβ(πΉ βͺ ((neiβπ½)β{π΄}))))) |
62 | 57 | unssbd 4187 |
. . . . . 6
β’ ((πΉ β (Filβπ) β§ π΄ β (π½ fClus πΉ)) β ((neiβπ½)β{π΄}) β (fiβ(πΉ βͺ ((neiβπ½)β{π΄})))) |
63 | 62, 60 | sstrd 3991 |
. . . . 5
β’ ((πΉ β (Filβπ) β§ π΄ β (π½ fClus πΉ)) β ((neiβπ½)β{π΄}) β (πfilGen(fiβ(πΉ βͺ ((neiβπ½)β{π΄}))))) |
64 | | elflim 23466 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ (πfilGen(fiβ(πΉ βͺ ((neiβπ½)β{π΄})))) β (Filβπ)) β (π΄ β (π½ fLim (πfilGen(fiβ(πΉ βͺ ((neiβπ½)β{π΄}))))) β (π΄ β π β§ ((neiβπ½)β{π΄}) β (πfilGen(fiβ(πΉ βͺ ((neiβπ½)β{π΄}))))))) |
65 | 31, 51, 64 | syl2anc 584 |
. . . . 5
β’ ((πΉ β (Filβπ) β§ π΄ β (π½ fClus πΉ)) β (π΄ β (π½ fLim (πfilGen(fiβ(πΉ βͺ ((neiβπ½)β{π΄}))))) β (π΄ β π β§ ((neiβπ½)β{π΄}) β (πfilGen(fiβ(πΉ βͺ ((neiβπ½)β{π΄}))))))) |
66 | 34, 63, 65 | mpbir2and 711 |
. . . 4
β’ ((πΉ β (Filβπ) β§ π΄ β (π½ fClus πΉ)) β π΄ β (π½ fLim (πfilGen(fiβ(πΉ βͺ ((neiβπ½)β{π΄})))))) |
67 | | sseq2 4007 |
. . . . . 6
β’ (π = (πfilGen(fiβ(πΉ βͺ ((neiβπ½)β{π΄})))) β (πΉ β π β πΉ β (πfilGen(fiβ(πΉ βͺ ((neiβπ½)β{π΄})))))) |
68 | | oveq2 7413 |
. . . . . . 7
β’ (π = (πfilGen(fiβ(πΉ βͺ ((neiβπ½)β{π΄})))) β (π½ fLim π) = (π½ fLim (πfilGen(fiβ(πΉ βͺ ((neiβπ½)β{π΄})))))) |
69 | 68 | eleq2d 2819 |
. . . . . 6
β’ (π = (πfilGen(fiβ(πΉ βͺ ((neiβπ½)β{π΄})))) β (π΄ β (π½ fLim π) β π΄ β (π½ fLim (πfilGen(fiβ(πΉ βͺ ((neiβπ½)β{π΄}))))))) |
70 | 67, 69 | anbi12d 631 |
. . . . 5
β’ (π = (πfilGen(fiβ(πΉ βͺ ((neiβπ½)β{π΄})))) β ((πΉ β π β§ π΄ β (π½ fLim π)) β (πΉ β (πfilGen(fiβ(πΉ βͺ ((neiβπ½)β{π΄})))) β§ π΄ β (π½ fLim (πfilGen(fiβ(πΉ βͺ ((neiβπ½)β{π΄})))))))) |
71 | 70 | rspcev 3612 |
. . . 4
β’ (((πfilGen(fiβ(πΉ βͺ ((neiβπ½)β{π΄})))) β (Filβπ) β§ (πΉ β (πfilGen(fiβ(πΉ βͺ ((neiβπ½)β{π΄})))) β§ π΄ β (π½ fLim (πfilGen(fiβ(πΉ βͺ ((neiβπ½)β{π΄}))))))) β βπ β (Filβπ)(πΉ β π β§ π΄ β (π½ fLim π))) |
72 | 51, 61, 66, 71 | syl12anc 835 |
. . 3
β’ ((πΉ β (Filβπ) β§ π΄ β (π½ fClus πΉ)) β βπ β (Filβπ)(πΉ β π β§ π΄ β (π½ fLim π))) |
73 | 72 | ex 413 |
. 2
β’ (πΉ β (Filβπ) β (π΄ β (π½ fClus πΉ) β βπ β (Filβπ)(πΉ β π β§ π΄ β (π½ fLim π)))) |
74 | | simprl 769 |
. . . . . 6
β’ ((πΉ β (Filβπ) β§ (π β (Filβπ) β§ (πΉ β π β§ π΄ β (π½ fLim π)))) β π β (Filβπ)) |
75 | | simprrr 780 |
. . . . . . 7
β’ ((πΉ β (Filβπ) β§ (π β (Filβπ) β§ (πΉ β π β§ π΄ β (π½ fLim π)))) β π΄ β (π½ fLim π)) |
76 | | flimtopon 23465 |
. . . . . . 7
β’ (π΄ β (π½ fLim π) β (π½ β (TopOnβπ) β π β (Filβπ))) |
77 | 75, 76 | syl 17 |
. . . . . 6
β’ ((πΉ β (Filβπ) β§ (π β (Filβπ) β§ (πΉ β π β§ π΄ β (π½ fLim π)))) β (π½ β (TopOnβπ) β π β (Filβπ))) |
78 | 74, 77 | mpbird 256 |
. . . . 5
β’ ((πΉ β (Filβπ) β§ (π β (Filβπ) β§ (πΉ β π β§ π΄ β (π½ fLim π)))) β π½ β (TopOnβπ)) |
79 | | simpl 483 |
. . . . 5
β’ ((πΉ β (Filβπ) β§ (π β (Filβπ) β§ (πΉ β π β§ π΄ β (π½ fLim π)))) β πΉ β (Filβπ)) |
80 | | simprrl 779 |
. . . . 5
β’ ((πΉ β (Filβπ) β§ (π β (Filβπ) β§ (πΉ β π β§ π΄ β (π½ fLim π)))) β πΉ β π) |
81 | | fclsss2 23518 |
. . . . 5
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ πΉ β π) β (π½ fClus π) β (π½ fClus πΉ)) |
82 | 78, 79, 80, 81 | syl3anc 1371 |
. . . 4
β’ ((πΉ β (Filβπ) β§ (π β (Filβπ) β§ (πΉ β π β§ π΄ β (π½ fLim π)))) β (π½ fClus π) β (π½ fClus πΉ)) |
83 | | flimfcls 23521 |
. . . . 5
β’ (π½ fLim π) β (π½ fClus π) |
84 | 83, 75 | sselid 3979 |
. . . 4
β’ ((πΉ β (Filβπ) β§ (π β (Filβπ) β§ (πΉ β π β§ π΄ β (π½ fLim π)))) β π΄ β (π½ fClus π)) |
85 | 82, 84 | sseldd 3982 |
. . 3
β’ ((πΉ β (Filβπ) β§ (π β (Filβπ) β§ (πΉ β π β§ π΄ β (π½ fLim π)))) β π΄ β (π½ fClus πΉ)) |
86 | 85 | rexlimdvaa 3156 |
. 2
β’ (πΉ β (Filβπ) β (βπ β (Filβπ)(πΉ β π β§ π΄ β (π½ fLim π)) β π΄ β (π½ fClus πΉ))) |
87 | 73, 86 | impbid 211 |
1
β’ (πΉ β (Filβπ) β (π΄ β (π½ fClus πΉ) β βπ β (Filβπ)(πΉ β π β§ π΄ β (π½ fLim π)))) |