Step | Hyp | Ref
| Expression |
1 | | filsspw 23218 |
. . . . . . . 8
β’ (πΉ β (Filβπ) β πΉ β π« π) |
2 | 1 | adantr 482 |
. . . . . . 7
β’ ((πΉ β (Filβπ) β§ π΄ β (π½ fClus πΉ)) β πΉ β π« π) |
3 | | fclstop 23378 |
. . . . . . . . . 10
β’ (π΄ β (π½ fClus πΉ) β π½ β Top) |
4 | 3 | adantl 483 |
. . . . . . . . 9
β’ ((πΉ β (Filβπ) β§ π΄ β (π½ fClus πΉ)) β π½ β Top) |
5 | | eqid 2733 |
. . . . . . . . . 10
β’ βͺ π½ =
βͺ π½ |
6 | 5 | neisspw 22474 |
. . . . . . . . 9
β’ (π½ β Top β
((neiβπ½)β{π΄}) β π« βͺ π½) |
7 | 4, 6 | syl 17 |
. . . . . . . 8
β’ ((πΉ β (Filβπ) β§ π΄ β (π½ fClus πΉ)) β ((neiβπ½)β{π΄}) β π« βͺ π½) |
8 | | filunibas 23248 |
. . . . . . . . . 10
β’ (πΉ β (Filβπ) β βͺ πΉ =
π) |
9 | 5 | fclsfil 23377 |
. . . . . . . . . . 11
β’ (π΄ β (π½ fClus πΉ) β πΉ β (Filββͺ π½)) |
10 | | filunibas 23248 |
. . . . . . . . . . 11
β’ (πΉ β (Filββͺ π½)
β βͺ πΉ = βͺ π½) |
11 | 9, 10 | syl 17 |
. . . . . . . . . 10
β’ (π΄ β (π½ fClus πΉ) β βͺ πΉ = βͺ
π½) |
12 | 8, 11 | sylan9req 2794 |
. . . . . . . . 9
β’ ((πΉ β (Filβπ) β§ π΄ β (π½ fClus πΉ)) β π = βͺ π½) |
13 | 12 | pweqd 4578 |
. . . . . . . 8
β’ ((πΉ β (Filβπ) β§ π΄ β (π½ fClus πΉ)) β π« π = π« βͺ
π½) |
14 | 7, 13 | sseqtrrd 3986 |
. . . . . . 7
β’ ((πΉ β (Filβπ) β§ π΄ β (π½ fClus πΉ)) β ((neiβπ½)β{π΄}) β π« π) |
15 | 2, 14 | unssd 4147 |
. . . . . 6
β’ ((πΉ β (Filβπ) β§ π΄ β (π½ fClus πΉ)) β (πΉ βͺ ((neiβπ½)β{π΄})) β π« π) |
16 | | ssun1 4133 |
. . . . . . . 8
β’ πΉ β (πΉ βͺ ((neiβπ½)β{π΄})) |
17 | | filn0 23229 |
. . . . . . . 8
β’ (πΉ β (Filβπ) β πΉ β β
) |
18 | | ssn0 4361 |
. . . . . . . 8
β’ ((πΉ β (πΉ βͺ ((neiβπ½)β{π΄})) β§ πΉ β β
) β (πΉ βͺ ((neiβπ½)β{π΄})) β β
) |
19 | 16, 17, 18 | sylancr 588 |
. . . . . . 7
β’ (πΉ β (Filβπ) β (πΉ βͺ ((neiβπ½)β{π΄})) β β
) |
20 | 19 | adantr 482 |
. . . . . 6
β’ ((πΉ β (Filβπ) β§ π΄ β (π½ fClus πΉ)) β (πΉ βͺ ((neiβπ½)β{π΄})) β β
) |
21 | | incom 4162 |
. . . . . . . . . . . 12
β’ (π¦ β© π₯) = (π₯ β© π¦) |
22 | | fclsneii 23384 |
. . . . . . . . . . . 12
β’ ((π΄ β (π½ fClus πΉ) β§ π¦ β ((neiβπ½)β{π΄}) β§ π₯ β πΉ) β (π¦ β© π₯) β β
) |
23 | 21, 22 | eqnetrrid 3016 |
. . . . . . . . . . 11
β’ ((π΄ β (π½ fClus πΉ) β§ π¦ β ((neiβπ½)β{π΄}) β§ π₯ β πΉ) β (π₯ β© π¦) β β
) |
24 | 23 | 3com23 1127 |
. . . . . . . . . 10
β’ ((π΄ β (π½ fClus πΉ) β§ π₯ β πΉ β§ π¦ β ((neiβπ½)β{π΄})) β (π₯ β© π¦) β β
) |
25 | 24 | 3expb 1121 |
. . . . . . . . 9
β’ ((π΄ β (π½ fClus πΉ) β§ (π₯ β πΉ β§ π¦ β ((neiβπ½)β{π΄}))) β (π₯ β© π¦) β β
) |
26 | 25 | adantll 713 |
. . . . . . . 8
β’ (((πΉ β (Filβπ) β§ π΄ β (π½ fClus πΉ)) β§ (π₯ β πΉ β§ π¦ β ((neiβπ½)β{π΄}))) β (π₯ β© π¦) β β
) |
27 | 26 | ralrimivva 3194 |
. . . . . . 7
β’ ((πΉ β (Filβπ) β§ π΄ β (π½ fClus πΉ)) β βπ₯ β πΉ βπ¦ β ((neiβπ½)β{π΄})(π₯ β© π¦) β β
) |
28 | | filfbas 23215 |
. . . . . . . . 9
β’ (πΉ β (Filβπ) β πΉ β (fBasβπ)) |
29 | 28 | adantr 482 |
. . . . . . . 8
β’ ((πΉ β (Filβπ) β§ π΄ β (π½ fClus πΉ)) β πΉ β (fBasβπ)) |
30 | | istopon 22277 |
. . . . . . . . . . 11
β’ (π½ β (TopOnβπ) β (π½ β Top β§ π = βͺ π½)) |
31 | 4, 12, 30 | sylanbrc 584 |
. . . . . . . . . 10
β’ ((πΉ β (Filβπ) β§ π΄ β (π½ fClus πΉ)) β π½ β (TopOnβπ)) |
32 | 5 | fclselbas 23383 |
. . . . . . . . . . . . 13
β’ (π΄ β (π½ fClus πΉ) β π΄ β βͺ π½) |
33 | 32 | adantl 483 |
. . . . . . . . . . . 12
β’ ((πΉ β (Filβπ) β§ π΄ β (π½ fClus πΉ)) β π΄ β βͺ π½) |
34 | 33, 12 | eleqtrrd 2837 |
. . . . . . . . . . 11
β’ ((πΉ β (Filβπ) β§ π΄ β (π½ fClus πΉ)) β π΄ β π) |
35 | 34 | snssd 4770 |
. . . . . . . . . 10
β’ ((πΉ β (Filβπ) β§ π΄ β (π½ fClus πΉ)) β {π΄} β π) |
36 | | snnzg 4736 |
. . . . . . . . . . 11
β’ (π΄ β (π½ fClus πΉ) β {π΄} β β
) |
37 | 36 | adantl 483 |
. . . . . . . . . 10
β’ ((πΉ β (Filβπ) β§ π΄ β (π½ fClus πΉ)) β {π΄} β β
) |
38 | | neifil 23247 |
. . . . . . . . . 10
β’ ((π½ β (TopOnβπ) β§ {π΄} β π β§ {π΄} β β
) β ((neiβπ½)β{π΄}) β (Filβπ)) |
39 | 31, 35, 37, 38 | syl3anc 1372 |
. . . . . . . . 9
β’ ((πΉ β (Filβπ) β§ π΄ β (π½ fClus πΉ)) β ((neiβπ½)β{π΄}) β (Filβπ)) |
40 | | filfbas 23215 |
. . . . . . . . 9
β’
(((neiβπ½)β{π΄}) β (Filβπ) β ((neiβπ½)β{π΄}) β (fBasβπ)) |
41 | 39, 40 | syl 17 |
. . . . . . . 8
β’ ((πΉ β (Filβπ) β§ π΄ β (π½ fClus πΉ)) β ((neiβπ½)β{π΄}) β (fBasβπ)) |
42 | | fbunfip 23236 |
. . . . . . . 8
β’ ((πΉ β (fBasβπ) β§ ((neiβπ½)β{π΄}) β (fBasβπ)) β (Β¬ β
β
(fiβ(πΉ βͺ
((neiβπ½)β{π΄}))) β βπ₯ β πΉ βπ¦ β ((neiβπ½)β{π΄})(π₯ β© π¦) β β
)) |
43 | 29, 41, 42 | syl2anc 585 |
. . . . . . 7
β’ ((πΉ β (Filβπ) β§ π΄ β (π½ fClus πΉ)) β (Β¬ β
β
(fiβ(πΉ βͺ
((neiβπ½)β{π΄}))) β βπ₯ β πΉ βπ¦ β ((neiβπ½)β{π΄})(π₯ β© π¦) β β
)) |
44 | 27, 43 | mpbird 257 |
. . . . . 6
β’ ((πΉ β (Filβπ) β§ π΄ β (π½ fClus πΉ)) β Β¬ β
β
(fiβ(πΉ βͺ
((neiβπ½)β{π΄})))) |
45 | | filtop 23222 |
. . . . . . . 8
β’ (πΉ β (Filβπ) β π β πΉ) |
46 | | fsubbas 23234 |
. . . . . . . 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 482 |
. . . . . 6
β’ ((πΉ β (Filβπ) β§ π΄ β (π½ fClus πΉ)) β ((fiβ(πΉ βͺ ((neiβπ½)β{π΄}))) β (fBasβπ) β ((πΉ βͺ ((neiβπ½)β{π΄})) β π« π β§ (πΉ βͺ ((neiβπ½)β{π΄})) β β
β§ Β¬ β
β
(fiβ(πΉ βͺ
((neiβπ½)β{π΄})))))) |
49 | 15, 20, 44, 48 | mpbir3and 1343 |
. . . . 5
β’ ((πΉ β (Filβπ) β§ π΄ β (π½ fClus πΉ)) β (fiβ(πΉ βͺ ((neiβπ½)β{π΄}))) β (fBasβπ)) |
50 | | fgcl 23245 |
. . . . 5
β’
((fiβ(πΉ βͺ
((neiβπ½)β{π΄}))) β (fBasβπ) β (πfilGen(fiβ(πΉ βͺ ((neiβπ½)β{π΄})))) β (Filβπ)) |
51 | 49, 50 | syl 17 |
. . . 4
β’ ((πΉ β (Filβπ) β§ π΄ β (π½ fClus πΉ)) β (πfilGen(fiβ(πΉ βͺ ((neiβπ½)β{π΄})))) β (Filβπ)) |
52 | | fvex 6856 |
. . . . . . . . 9
β’
((neiβπ½)β{π΄}) β V |
53 | | unexg 7684 |
. . . . . . . . 9
β’ ((πΉ β (Filβπ) β§ ((neiβπ½)β{π΄}) β V) β (πΉ βͺ ((neiβπ½)β{π΄})) β V) |
54 | 52, 53 | mpan2 690 |
. . . . . . . 8
β’ (πΉ β (Filβπ) β (πΉ βͺ ((neiβπ½)β{π΄})) β V) |
55 | | ssfii 9360 |
. . . . . . . 8
β’ ((πΉ βͺ ((neiβπ½)β{π΄})) β V β (πΉ βͺ ((neiβπ½)β{π΄})) β (fiβ(πΉ βͺ ((neiβπ½)β{π΄})))) |
56 | 54, 55 | syl 17 |
. . . . . . 7
β’ (πΉ β (Filβπ) β (πΉ βͺ ((neiβπ½)β{π΄})) β (fiβ(πΉ βͺ ((neiβπ½)β{π΄})))) |
57 | 56 | adantr 482 |
. . . . . 6
β’ ((πΉ β (Filβπ) β§ π΄ β (π½ fClus πΉ)) β (πΉ βͺ ((neiβπ½)β{π΄})) β (fiβ(πΉ βͺ ((neiβπ½)β{π΄})))) |
58 | 57 | unssad 4148 |
. . . . 5
β’ ((πΉ β (Filβπ) β§ π΄ β (π½ fClus πΉ)) β πΉ β (fiβ(πΉ βͺ ((neiβπ½)β{π΄})))) |
59 | | ssfg 23239 |
. . . . . 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 3955 |
. . . 4
β’ ((πΉ β (Filβπ) β§ π΄ β (π½ fClus πΉ)) β πΉ β (πfilGen(fiβ(πΉ βͺ ((neiβπ½)β{π΄}))))) |
62 | 57 | unssbd 4149 |
. . . . . 6
β’ ((πΉ β (Filβπ) β§ π΄ β (π½ fClus πΉ)) β ((neiβπ½)β{π΄}) β (fiβ(πΉ βͺ ((neiβπ½)β{π΄})))) |
63 | 62, 60 | sstrd 3955 |
. . . . 5
β’ ((πΉ β (Filβπ) β§ π΄ β (π½ fClus πΉ)) β ((neiβπ½)β{π΄}) β (πfilGen(fiβ(πΉ βͺ ((neiβπ½)β{π΄}))))) |
64 | | elflim 23338 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ (πfilGen(fiβ(πΉ βͺ ((neiβπ½)β{π΄})))) β (Filβπ)) β (π΄ β (π½ fLim (πfilGen(fiβ(πΉ βͺ ((neiβπ½)β{π΄}))))) β (π΄ β π β§ ((neiβπ½)β{π΄}) β (πfilGen(fiβ(πΉ βͺ ((neiβπ½)β{π΄}))))))) |
65 | 31, 51, 64 | syl2anc 585 |
. . . . 5
β’ ((πΉ β (Filβπ) β§ π΄ β (π½ fClus πΉ)) β (π΄ β (π½ fLim (πfilGen(fiβ(πΉ βͺ ((neiβπ½)β{π΄}))))) β (π΄ β π β§ ((neiβπ½)β{π΄}) β (πfilGen(fiβ(πΉ βͺ ((neiβπ½)β{π΄}))))))) |
66 | 34, 63, 65 | mpbir2and 712 |
. . . 4
β’ ((πΉ β (Filβπ) β§ π΄ β (π½ fClus πΉ)) β π΄ β (π½ fLim (πfilGen(fiβ(πΉ βͺ ((neiβπ½)β{π΄})))))) |
67 | | sseq2 3971 |
. . . . . 6
β’ (π = (πfilGen(fiβ(πΉ βͺ ((neiβπ½)β{π΄})))) β (πΉ β π β πΉ β (πfilGen(fiβ(πΉ βͺ ((neiβπ½)β{π΄})))))) |
68 | | oveq2 7366 |
. . . . . . 7
β’ (π = (πfilGen(fiβ(πΉ βͺ ((neiβπ½)β{π΄})))) β (π½ fLim π) = (π½ fLim (πfilGen(fiβ(πΉ βͺ ((neiβπ½)β{π΄})))))) |
69 | 68 | eleq2d 2820 |
. . . . . 6
β’ (π = (πfilGen(fiβ(πΉ βͺ ((neiβπ½)β{π΄})))) β (π΄ β (π½ fLim π) β π΄ β (π½ fLim (πfilGen(fiβ(πΉ βͺ ((neiβπ½)β{π΄}))))))) |
70 | 67, 69 | anbi12d 632 |
. . . . 5
β’ (π = (πfilGen(fiβ(πΉ βͺ ((neiβπ½)β{π΄})))) β ((πΉ β π β§ π΄ β (π½ fLim π)) β (πΉ β (πfilGen(fiβ(πΉ βͺ ((neiβπ½)β{π΄})))) β§ π΄ β (π½ fLim (πfilGen(fiβ(πΉ βͺ ((neiβπ½)β{π΄})))))))) |
71 | 70 | rspcev 3580 |
. . . 4
β’ (((πfilGen(fiβ(πΉ βͺ ((neiβπ½)β{π΄})))) β (Filβπ) β§ (πΉ β (πfilGen(fiβ(πΉ βͺ ((neiβπ½)β{π΄})))) β§ π΄ β (π½ fLim (πfilGen(fiβ(πΉ βͺ ((neiβπ½)β{π΄}))))))) β βπ β (Filβπ)(πΉ β π β§ π΄ β (π½ fLim π))) |
72 | 51, 61, 66, 71 | syl12anc 836 |
. . 3
β’ ((πΉ β (Filβπ) β§ π΄ β (π½ fClus πΉ)) β βπ β (Filβπ)(πΉ β π β§ π΄ β (π½ fLim π))) |
73 | 72 | ex 414 |
. 2
β’ (πΉ β (Filβπ) β (π΄ β (π½ fClus πΉ) β βπ β (Filβπ)(πΉ β π β§ π΄ β (π½ fLim π)))) |
74 | | simprl 770 |
. . . . . 6
β’ ((πΉ β (Filβπ) β§ (π β (Filβπ) β§ (πΉ β π β§ π΄ β (π½ fLim π)))) β π β (Filβπ)) |
75 | | simprrr 781 |
. . . . . . 7
β’ ((πΉ β (Filβπ) β§ (π β (Filβπ) β§ (πΉ β π β§ π΄ β (π½ fLim π)))) β π΄ β (π½ fLim π)) |
76 | | flimtopon 23337 |
. . . . . . 7
β’ (π΄ β (π½ fLim π) β (π½ β (TopOnβπ) β π β (Filβπ))) |
77 | 75, 76 | syl 17 |
. . . . . 6
β’ ((πΉ β (Filβπ) β§ (π β (Filβπ) β§ (πΉ β π β§ π΄ β (π½ fLim π)))) β (π½ β (TopOnβπ) β π β (Filβπ))) |
78 | 74, 77 | mpbird 257 |
. . . . 5
β’ ((πΉ β (Filβπ) β§ (π β (Filβπ) β§ (πΉ β π β§ π΄ β (π½ fLim π)))) β π½ β (TopOnβπ)) |
79 | | simpl 484 |
. . . . 5
β’ ((πΉ β (Filβπ) β§ (π β (Filβπ) β§ (πΉ β π β§ π΄ β (π½ fLim π)))) β πΉ β (Filβπ)) |
80 | | simprrl 780 |
. . . . 5
β’ ((πΉ β (Filβπ) β§ (π β (Filβπ) β§ (πΉ β π β§ π΄ β (π½ fLim π)))) β πΉ β π) |
81 | | fclsss2 23390 |
. . . . 5
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ πΉ β π) β (π½ fClus π) β (π½ fClus πΉ)) |
82 | 78, 79, 80, 81 | syl3anc 1372 |
. . . 4
β’ ((πΉ β (Filβπ) β§ (π β (Filβπ) β§ (πΉ β π β§ π΄ β (π½ fLim π)))) β (π½ fClus π) β (π½ fClus πΉ)) |
83 | | flimfcls 23393 |
. . . . 5
β’ (π½ fLim π) β (π½ fClus π) |
84 | 83, 75 | sselid 3943 |
. . . 4
β’ ((πΉ β (Filβπ) β§ (π β (Filβπ) β§ (πΉ β π β§ π΄ β (π½ fLim π)))) β π΄ β (π½ fClus π)) |
85 | 82, 84 | sseldd 3946 |
. . 3
β’ ((πΉ β (Filβπ) β§ (π β (Filβπ) β§ (πΉ β π β§ π΄ β (π½ fLim π)))) β π΄ β (π½ fClus πΉ)) |
86 | 85 | rexlimdvaa 3150 |
. 2
β’ (πΉ β (Filβπ) β (βπ β (Filβπ)(πΉ β π β§ π΄ β (π½ fLim π)) β π΄ β (π½ fClus πΉ))) |
87 | 73, 86 | impbid 211 |
1
β’ (πΉ β (Filβπ) β (π΄ β (π½ fClus πΉ) β βπ β (Filβπ)(πΉ β π β§ π΄ β (π½ fLim π)))) |