Step | Hyp | Ref
| Expression |
1 | | flimcls.2 |
. . 3
β’ πΉ = (πfilGen(fiβ(((neiβπ½)β{π΄}) βͺ {π}))) |
2 | | topontop 22415 |
. . . . . . . . 9
β’ (π½ β (TopOnβπ) β π½ β Top) |
3 | 2 | 3ad2ant1 1134 |
. . . . . . . 8
β’ ((π½ β (TopOnβπ) β§ π β π β§ π΄ β ((clsβπ½)βπ)) β π½ β Top) |
4 | | eqid 2733 |
. . . . . . . . 9
β’ βͺ π½ =
βͺ π½ |
5 | 4 | neisspw 22611 |
. . . . . . . 8
β’ (π½ β Top β
((neiβπ½)β{π΄}) β π« βͺ π½) |
6 | 3, 5 | syl 17 |
. . . . . . 7
β’ ((π½ β (TopOnβπ) β§ π β π β§ π΄ β ((clsβπ½)βπ)) β ((neiβπ½)β{π΄}) β π« βͺ π½) |
7 | | toponuni 22416 |
. . . . . . . . 9
β’ (π½ β (TopOnβπ) β π = βͺ π½) |
8 | 7 | 3ad2ant1 1134 |
. . . . . . . 8
β’ ((π½ β (TopOnβπ) β§ π β π β§ π΄ β ((clsβπ½)βπ)) β π = βͺ π½) |
9 | 8 | pweqd 4620 |
. . . . . . 7
β’ ((π½ β (TopOnβπ) β§ π β π β§ π΄ β ((clsβπ½)βπ)) β π« π = π« βͺ
π½) |
10 | 6, 9 | sseqtrrd 4024 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ π β π β§ π΄ β ((clsβπ½)βπ)) β ((neiβπ½)β{π΄}) β π« π) |
11 | | toponmax 22428 |
. . . . . . . . . 10
β’ (π½ β (TopOnβπ) β π β π½) |
12 | | elpw2g 5345 |
. . . . . . . . . 10
β’ (π β π½ β (π β π« π β π β π)) |
13 | 11, 12 | syl 17 |
. . . . . . . . 9
β’ (π½ β (TopOnβπ) β (π β π« π β π β π)) |
14 | 13 | biimpar 479 |
. . . . . . . 8
β’ ((π½ β (TopOnβπ) β§ π β π) β π β π« π) |
15 | 14 | 3adant3 1133 |
. . . . . . 7
β’ ((π½ β (TopOnβπ) β§ π β π β§ π΄ β ((clsβπ½)βπ)) β π β π« π) |
16 | 15 | snssd 4813 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ π β π β§ π΄ β ((clsβπ½)βπ)) β {π} β π« π) |
17 | 10, 16 | unssd 4187 |
. . . . 5
β’ ((π½ β (TopOnβπ) β§ π β π β§ π΄ β ((clsβπ½)βπ)) β (((neiβπ½)β{π΄}) βͺ {π}) β π« π) |
18 | | ssun2 4174 |
. . . . . 6
β’ {π} β (((neiβπ½)β{π΄}) βͺ {π}) |
19 | 11 | 3ad2ant1 1134 |
. . . . . . . 8
β’ ((π½ β (TopOnβπ) β§ π β π β§ π΄ β ((clsβπ½)βπ)) β π β π½) |
20 | | simp2 1138 |
. . . . . . . 8
β’ ((π½ β (TopOnβπ) β§ π β π β§ π΄ β ((clsβπ½)βπ)) β π β π) |
21 | 19, 20 | ssexd 5325 |
. . . . . . 7
β’ ((π½ β (TopOnβπ) β§ π β π β§ π΄ β ((clsβπ½)βπ)) β π β V) |
22 | 21 | snn0d 4780 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ π β π β§ π΄ β ((clsβπ½)βπ)) β {π} β β
) |
23 | | ssn0 4401 |
. . . . . 6
β’ (({π} β (((neiβπ½)β{π΄}) βͺ {π}) β§ {π} β β
) β (((neiβπ½)β{π΄}) βͺ {π}) β β
) |
24 | 18, 22, 23 | sylancr 588 |
. . . . 5
β’ ((π½ β (TopOnβπ) β§ π β π β§ π΄ β ((clsβπ½)βπ)) β (((neiβπ½)β{π΄}) βͺ {π}) β β
) |
25 | 20, 8 | sseqtrd 4023 |
. . . . . . . . . . 11
β’ ((π½ β (TopOnβπ) β§ π β π β§ π΄ β ((clsβπ½)βπ)) β π β βͺ π½) |
26 | | simp3 1139 |
. . . . . . . . . . 11
β’ ((π½ β (TopOnβπ) β§ π β π β§ π΄ β ((clsβπ½)βπ)) β π΄ β ((clsβπ½)βπ)) |
27 | 4 | neindisj 22621 |
. . . . . . . . . . . 12
β’ (((π½ β Top β§ π β βͺ π½)
β§ (π΄ β
((clsβπ½)βπ) β§ π₯ β ((neiβπ½)β{π΄}))) β (π₯ β© π) β β
) |
28 | 27 | expr 458 |
. . . . . . . . . . 11
β’ (((π½ β Top β§ π β βͺ π½)
β§ π΄ β
((clsβπ½)βπ)) β (π₯ β ((neiβπ½)β{π΄}) β (π₯ β© π) β β
)) |
29 | 3, 25, 26, 28 | syl21anc 837 |
. . . . . . . . . 10
β’ ((π½ β (TopOnβπ) β§ π β π β§ π΄ β ((clsβπ½)βπ)) β (π₯ β ((neiβπ½)β{π΄}) β (π₯ β© π) β β
)) |
30 | 29 | imp 408 |
. . . . . . . . 9
β’ (((π½ β (TopOnβπ) β§ π β π β§ π΄ β ((clsβπ½)βπ)) β§ π₯ β ((neiβπ½)β{π΄})) β (π₯ β© π) β β
) |
31 | | elsni 4646 |
. . . . . . . . . . 11
β’ (π¦ β {π} β π¦ = π) |
32 | 31 | ineq2d 4213 |
. . . . . . . . . 10
β’ (π¦ β {π} β (π₯ β© π¦) = (π₯ β© π)) |
33 | 32 | neeq1d 3001 |
. . . . . . . . 9
β’ (π¦ β {π} β ((π₯ β© π¦) β β
β (π₯ β© π) β β
)) |
34 | 30, 33 | syl5ibrcom 246 |
. . . . . . . 8
β’ (((π½ β (TopOnβπ) β§ π β π β§ π΄ β ((clsβπ½)βπ)) β§ π₯ β ((neiβπ½)β{π΄})) β (π¦ β {π} β (π₯ β© π¦) β β
)) |
35 | 34 | ralrimiv 3146 |
. . . . . . 7
β’ (((π½ β (TopOnβπ) β§ π β π β§ π΄ β ((clsβπ½)βπ)) β§ π₯ β ((neiβπ½)β{π΄})) β βπ¦ β {π} (π₯ β© π¦) β β
) |
36 | 35 | ralrimiva 3147 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ π β π β§ π΄ β ((clsβπ½)βπ)) β βπ₯ β ((neiβπ½)β{π΄})βπ¦ β {π} (π₯ β© π¦) β β
) |
37 | | simp1 1137 |
. . . . . . . . 9
β’ ((π½ β (TopOnβπ) β§ π β π β§ π΄ β ((clsβπ½)βπ)) β π½ β (TopOnβπ)) |
38 | 4 | clsss3 22563 |
. . . . . . . . . . . . 13
β’ ((π½ β Top β§ π β βͺ π½)
β ((clsβπ½)βπ) β βͺ π½) |
39 | 3, 25, 38 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((π½ β (TopOnβπ) β§ π β π β§ π΄ β ((clsβπ½)βπ)) β ((clsβπ½)βπ) β βͺ π½) |
40 | 39, 26 | sseldd 3984 |
. . . . . . . . . . 11
β’ ((π½ β (TopOnβπ) β§ π β π β§ π΄ β ((clsβπ½)βπ)) β π΄ β βͺ π½) |
41 | 40, 8 | eleqtrrd 2837 |
. . . . . . . . . 10
β’ ((π½ β (TopOnβπ) β§ π β π β§ π΄ β ((clsβπ½)βπ)) β π΄ β π) |
42 | 41 | snssd 4813 |
. . . . . . . . 9
β’ ((π½ β (TopOnβπ) β§ π β π β§ π΄ β ((clsβπ½)βπ)) β {π΄} β π) |
43 | | snnzg 4779 |
. . . . . . . . . 10
β’ (π΄ β ((clsβπ½)βπ) β {π΄} β β
) |
44 | 43 | 3ad2ant3 1136 |
. . . . . . . . 9
β’ ((π½ β (TopOnβπ) β§ π β π β§ π΄ β ((clsβπ½)βπ)) β {π΄} β β
) |
45 | | neifil 23384 |
. . . . . . . . 9
β’ ((π½ β (TopOnβπ) β§ {π΄} β π β§ {π΄} β β
) β ((neiβπ½)β{π΄}) β (Filβπ)) |
46 | 37, 42, 44, 45 | syl3anc 1372 |
. . . . . . . 8
β’ ((π½ β (TopOnβπ) β§ π β π β§ π΄ β ((clsβπ½)βπ)) β ((neiβπ½)β{π΄}) β (Filβπ)) |
47 | | filfbas 23352 |
. . . . . . . 8
β’
(((neiβπ½)β{π΄}) β (Filβπ) β ((neiβπ½)β{π΄}) β (fBasβπ)) |
48 | 46, 47 | syl 17 |
. . . . . . 7
β’ ((π½ β (TopOnβπ) β§ π β π β§ π΄ β ((clsβπ½)βπ)) β ((neiβπ½)β{π΄}) β (fBasβπ)) |
49 | | ne0i 4335 |
. . . . . . . . . . 11
β’ (π΄ β ((clsβπ½)βπ) β ((clsβπ½)βπ) β β
) |
50 | 49 | 3ad2ant3 1136 |
. . . . . . . . . 10
β’ ((π½ β (TopOnβπ) β§ π β π β§ π΄ β ((clsβπ½)βπ)) β ((clsβπ½)βπ) β β
) |
51 | | cls0 22584 |
. . . . . . . . . . 11
β’ (π½ β Top β
((clsβπ½)ββ
) = β
) |
52 | 3, 51 | syl 17 |
. . . . . . . . . 10
β’ ((π½ β (TopOnβπ) β§ π β π β§ π΄ β ((clsβπ½)βπ)) β ((clsβπ½)ββ
) = β
) |
53 | 50, 52 | neeqtrrd 3016 |
. . . . . . . . 9
β’ ((π½ β (TopOnβπ) β§ π β π β§ π΄ β ((clsβπ½)βπ)) β ((clsβπ½)βπ) β ((clsβπ½)ββ
)) |
54 | | fveq2 6892 |
. . . . . . . . . 10
β’ (π = β
β
((clsβπ½)βπ) = ((clsβπ½)ββ
)) |
55 | 54 | necon3i 2974 |
. . . . . . . . 9
β’
(((clsβπ½)βπ) β ((clsβπ½)ββ
) β π β β
) |
56 | 53, 55 | syl 17 |
. . . . . . . 8
β’ ((π½ β (TopOnβπ) β§ π β π β§ π΄ β ((clsβπ½)βπ)) β π β β
) |
57 | | snfbas 23370 |
. . . . . . . 8
β’ ((π β π β§ π β β
β§ π β π½) β {π} β (fBasβπ)) |
58 | 20, 56, 19, 57 | syl3anc 1372 |
. . . . . . 7
β’ ((π½ β (TopOnβπ) β§ π β π β§ π΄ β ((clsβπ½)βπ)) β {π} β (fBasβπ)) |
59 | | fbunfip 23373 |
. . . . . . 7
β’
((((neiβπ½)β{π΄}) β (fBasβπ) β§ {π} β (fBasβπ)) β (Β¬ β
β
(fiβ(((neiβπ½)β{π΄}) βͺ {π})) β βπ₯ β ((neiβπ½)β{π΄})βπ¦ β {π} (π₯ β© π¦) β β
)) |
60 | 48, 58, 59 | syl2anc 585 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ π β π β§ π΄ β ((clsβπ½)βπ)) β (Β¬ β
β
(fiβ(((neiβπ½)β{π΄}) βͺ {π})) β βπ₯ β ((neiβπ½)β{π΄})βπ¦ β {π} (π₯ β© π¦) β β
)) |
61 | 36, 60 | mpbird 257 |
. . . . 5
β’ ((π½ β (TopOnβπ) β§ π β π β§ π΄ β ((clsβπ½)βπ)) β Β¬ β
β
(fiβ(((neiβπ½)β{π΄}) βͺ {π}))) |
62 | | fsubbas 23371 |
. . . . . 6
β’ (π β π½ β ((fiβ(((neiβπ½)β{π΄}) βͺ {π})) β (fBasβπ) β ((((neiβπ½)β{π΄}) βͺ {π}) β π« π β§ (((neiβπ½)β{π΄}) βͺ {π}) β β
β§ Β¬ β
β
(fiβ(((neiβπ½)β{π΄}) βͺ {π}))))) |
63 | 19, 62 | syl 17 |
. . . . 5
β’ ((π½ β (TopOnβπ) β§ π β π β§ π΄ β ((clsβπ½)βπ)) β ((fiβ(((neiβπ½)β{π΄}) βͺ {π})) β (fBasβπ) β ((((neiβπ½)β{π΄}) βͺ {π}) β π« π β§ (((neiβπ½)β{π΄}) βͺ {π}) β β
β§ Β¬ β
β
(fiβ(((neiβπ½)β{π΄}) βͺ {π}))))) |
64 | 17, 24, 61, 63 | mpbir3and 1343 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ π β π β§ π΄ β ((clsβπ½)βπ)) β (fiβ(((neiβπ½)β{π΄}) βͺ {π})) β (fBasβπ)) |
65 | | fgcl 23382 |
. . . 4
β’
((fiβ(((neiβπ½)β{π΄}) βͺ {π})) β (fBasβπ) β (πfilGen(fiβ(((neiβπ½)β{π΄}) βͺ {π}))) β (Filβπ)) |
66 | 64, 65 | syl 17 |
. . 3
β’ ((π½ β (TopOnβπ) β§ π β π β§ π΄ β ((clsβπ½)βπ)) β (πfilGen(fiβ(((neiβπ½)β{π΄}) βͺ {π}))) β (Filβπ)) |
67 | 1, 66 | eqeltrid 2838 |
. 2
β’ ((π½ β (TopOnβπ) β§ π β π β§ π΄ β ((clsβπ½)βπ)) β πΉ β (Filβπ)) |
68 | | fvex 6905 |
. . . . . 6
β’
((neiβπ½)β{π΄}) β V |
69 | | snex 5432 |
. . . . . 6
β’ {π} β V |
70 | 68, 69 | unex 7733 |
. . . . 5
β’
(((neiβπ½)β{π΄}) βͺ {π}) β V |
71 | | ssfii 9414 |
. . . . 5
β’
((((neiβπ½)β{π΄}) βͺ {π}) β V β (((neiβπ½)β{π΄}) βͺ {π}) β (fiβ(((neiβπ½)β{π΄}) βͺ {π}))) |
72 | 70, 71 | ax-mp 5 |
. . . 4
β’
(((neiβπ½)β{π΄}) βͺ {π}) β (fiβ(((neiβπ½)β{π΄}) βͺ {π})) |
73 | | ssfg 23376 |
. . . . . 6
β’
((fiβ(((neiβπ½)β{π΄}) βͺ {π})) β (fBasβπ) β (fiβ(((neiβπ½)β{π΄}) βͺ {π})) β (πfilGen(fiβ(((neiβπ½)β{π΄}) βͺ {π})))) |
74 | 64, 73 | syl 17 |
. . . . 5
β’ ((π½ β (TopOnβπ) β§ π β π β§ π΄ β ((clsβπ½)βπ)) β (fiβ(((neiβπ½)β{π΄}) βͺ {π})) β (πfilGen(fiβ(((neiβπ½)β{π΄}) βͺ {π})))) |
75 | 74, 1 | sseqtrrdi 4034 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ π β π β§ π΄ β ((clsβπ½)βπ)) β (fiβ(((neiβπ½)β{π΄}) βͺ {π})) β πΉ) |
76 | 72, 75 | sstrid 3994 |
. . 3
β’ ((π½ β (TopOnβπ) β§ π β π β§ π΄ β ((clsβπ½)βπ)) β (((neiβπ½)β{π΄}) βͺ {π}) β πΉ) |
77 | | snssg 4788 |
. . . . 5
β’ (π β V β (π β (((neiβπ½)β{π΄}) βͺ {π}) β {π} β (((neiβπ½)β{π΄}) βͺ {π}))) |
78 | 21, 77 | syl 17 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ π β π β§ π΄ β ((clsβπ½)βπ)) β (π β (((neiβπ½)β{π΄}) βͺ {π}) β {π} β (((neiβπ½)β{π΄}) βͺ {π}))) |
79 | 18, 78 | mpbiri 258 |
. . 3
β’ ((π½ β (TopOnβπ) β§ π β π β§ π΄ β ((clsβπ½)βπ)) β π β (((neiβπ½)β{π΄}) βͺ {π})) |
80 | 76, 79 | sseldd 3984 |
. 2
β’ ((π½ β (TopOnβπ) β§ π β π β§ π΄ β ((clsβπ½)βπ)) β π β πΉ) |
81 | 76 | unssad 4188 |
. . 3
β’ ((π½ β (TopOnβπ) β§ π β π β§ π΄ β ((clsβπ½)βπ)) β ((neiβπ½)β{π΄}) β πΉ) |
82 | | elflim 23475 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β (π΄ β (π½ fLim πΉ) β (π΄ β π β§ ((neiβπ½)β{π΄}) β πΉ))) |
83 | 37, 67, 82 | syl2anc 585 |
. . 3
β’ ((π½ β (TopOnβπ) β§ π β π β§ π΄ β ((clsβπ½)βπ)) β (π΄ β (π½ fLim πΉ) β (π΄ β π β§ ((neiβπ½)β{π΄}) β πΉ))) |
84 | 41, 81, 83 | mpbir2and 712 |
. 2
β’ ((π½ β (TopOnβπ) β§ π β π β§ π΄ β ((clsβπ½)βπ)) β π΄ β (π½ fLim πΉ)) |
85 | 67, 80, 84 | 3jca 1129 |
1
β’ ((π½ β (TopOnβπ) β§ π β π β§ π΄ β ((clsβπ½)βπ)) β (πΉ β (Filβπ) β§ π β πΉ β§ π΄ β (π½ fLim πΉ))) |