Step | Hyp | Ref
| Expression |
1 | | simpll 765 |
. . . . 5
β’ (((π β§ π₯ β πΆ) β§ π€ β ((neiβπΎ)β{(((π½CnExtπΎ)βπΉ)βπ₯)})) β π) |
2 | | simpll 765 |
. . . . . . . . 9
β’ (((π β§ π₯ β πΆ) β§ (π€ β ((neiβπΎ)β{(((π½CnExtπΎ)βπΉ)βπ₯)}) β§ π β ((neiβπ½)β{π₯}) β§ ((clsβπΎ)β(πΉ β (π β© π΄))) β π€)) β π) |
3 | | simpr3 1196 |
. . . . . . . . 9
β’ (((π β§ π₯ β πΆ) β§ (π€ β ((neiβπΎ)β{(((π½CnExtπΎ)βπΉ)βπ₯)}) β§ π β ((neiβπ½)β{π₯}) β§ ((clsβπΎ)β(πΉ β (π β© π΄))) β π€)) β ((clsβπΎ)β(πΉ β (π β© π΄))) β π€) |
4 | | cnextf.3 |
. . . . . . . . . . 11
β’ (π β π½ β Top) |
5 | 4 | ad2antrr 724 |
. . . . . . . . . 10
β’ (((π β§ π₯ β πΆ) β§ (π€ β ((neiβπΎ)β{(((π½CnExtπΎ)βπΉ)βπ₯)}) β§ π β ((neiβπ½)β{π₯}) β§ ((clsβπΎ)β(πΉ β (π β© π΄))) β π€)) β π½ β Top) |
6 | | simpr2 1195 |
. . . . . . . . . 10
β’ (((π β§ π₯ β πΆ) β§ (π€ β ((neiβπΎ)β{(((π½CnExtπΎ)βπΉ)βπ₯)}) β§ π β ((neiβπ½)β{π₯}) β§ ((clsβπΎ)β(πΉ β (π β© π΄))) β π€)) β π β ((neiβπ½)β{π₯})) |
7 | | neii2 22603 |
. . . . . . . . . 10
β’ ((π½ β Top β§ π β ((neiβπ½)β{π₯})) β βπ£ β π½ ({π₯} β π£ β§ π£ β π)) |
8 | 5, 6, 7 | syl2anc 584 |
. . . . . . . . 9
β’ (((π β§ π₯ β πΆ) β§ (π€ β ((neiβπΎ)β{(((π½CnExtπΎ)βπΉ)βπ₯)}) β§ π β ((neiβπ½)β{π₯}) β§ ((clsβπΎ)β(πΉ β (π β© π΄))) β π€)) β βπ£ β π½ ({π₯} β π£ β§ π£ β π)) |
9 | | vex 3478 |
. . . . . . . . . . . . . . . . . . . 20
β’ π₯ β V |
10 | 9 | snss 4788 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ β π£ β {π₯} β π£) |
11 | 10 | biimpri 227 |
. . . . . . . . . . . . . . . . . 18
β’ ({π₯} β π£ β π₯ β π£) |
12 | 11 | anim1i 615 |
. . . . . . . . . . . . . . . . 17
β’ (({π₯} β π£ β§ π£ β π) β (π₯ β π£ β§ π£ β π)) |
13 | 12 | anim2i 617 |
. . . . . . . . . . . . . . . 16
β’ ((π£ β π½ β§ ({π₯} β π£ β§ π£ β π)) β (π£ β π½ β§ (π₯ β π£ β§ π£ β π))) |
14 | 13 | anim2i 617 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π£ β π½ β§ ({π₯} β π£ β§ π£ β π))) β (π β§ (π£ β π½ β§ (π₯ β π£ β§ π£ β π)))) |
15 | 14 | ex 413 |
. . . . . . . . . . . . . 14
β’ (π β ((π£ β π½ β§ ({π₯} β π£ β§ π£ β π)) β (π β§ (π£ β π½ β§ (π₯ β π£ β§ π£ β π))))) |
16 | | 3anass 1095 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π£ β π½ β§ π₯ β π£) β (π β§ (π£ β π½ β§ π₯ β π£))) |
17 | 16 | anbi1i 624 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π£ β π½ β§ π₯ β π£) β§ π£ β π) β ((π β§ (π£ β π½ β§ π₯ β π£)) β§ π£ β π)) |
18 | | anass 469 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π£ β π½ β§ π₯ β π£)) β§ π£ β π) β (π β§ ((π£ β π½ β§ π₯ β π£) β§ π£ β π))) |
19 | | anass 469 |
. . . . . . . . . . . . . . . . 17
β’ (((π£ β π½ β§ π₯ β π£) β§ π£ β π) β (π£ β π½ β§ (π₯ β π£ β§ π£ β π))) |
20 | 19 | anbi2i 623 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ ((π£ β π½ β§ π₯ β π£) β§ π£ β π)) β (π β§ (π£ β π½ β§ (π₯ β π£ β§ π£ β π)))) |
21 | 17, 18, 20 | 3bitri 296 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π£ β π½ β§ π₯ β π£) β§ π£ β π) β (π β§ (π£ β π½ β§ (π₯ β π£ β§ π£ β π)))) |
22 | | opnneip 22614 |
. . . . . . . . . . . . . . . . . 18
β’ ((π½ β Top β§ π£ β π½ β§ π₯ β π£) β π£ β ((neiβπ½)β{π₯})) |
23 | 4, 22 | syl3an1 1163 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π£ β π½ β§ π₯ β π£) β π£ β ((neiβπ½)β{π₯})) |
24 | 23 | adantr 481 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π£ β π½ β§ π₯ β π£) β§ π£ β π) β π£ β ((neiβπ½)β{π₯})) |
25 | | simpr2 1195 |
. . . . . . . . . . . . . . . . . 18
β’ ((π£ β π β§ (π β§ π£ β π½ β§ π₯ β π£)) β π£ β π½) |
26 | 25 | ex 413 |
. . . . . . . . . . . . . . . . 17
β’ (π£ β π β ((π β§ π£ β π½ β§ π₯ β π£) β π£ β π½)) |
27 | 26 | imdistanri 570 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π£ β π½ β§ π₯ β π£) β§ π£ β π) β (π£ β π½ β§ π£ β π)) |
28 | 24, 27 | jca 512 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π£ β π½ β§ π₯ β π£) β§ π£ β π) β (π£ β ((neiβπ½)β{π₯}) β§ (π£ β π½ β§ π£ β π))) |
29 | 21, 28 | sylbir 234 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π£ β π½ β§ (π₯ β π£ β§ π£ β π))) β (π£ β ((neiβπ½)β{π₯}) β§ (π£ β π½ β§ π£ β π))) |
30 | 15, 29 | syl6 35 |
. . . . . . . . . . . . 13
β’ (π β ((π£ β π½ β§ ({π₯} β π£ β§ π£ β π)) β (π£ β ((neiβπ½)β{π₯}) β§ (π£ β π½ β§ π£ β π)))) |
31 | 30 | adantr 481 |
. . . . . . . . . . . 12
β’ ((π β§ ((clsβπΎ)β(πΉ β (π β© π΄))) β π€) β ((π£ β π½ β§ ({π₯} β π£ β§ π£ β π)) β (π£ β ((neiβπ½)β{π₯}) β§ (π£ β π½ β§ π£ β π)))) |
32 | | cnextf.4 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β πΎ β Haus) |
33 | | haustop 22826 |
. . . . . . . . . . . . . . . . . . 19
β’ (πΎ β Haus β πΎ β Top) |
34 | 32, 33 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π β πΎ β Top) |
35 | | imassrn 6068 |
. . . . . . . . . . . . . . . . . . 19
β’ (πΉ β (π β© π΄)) β ran πΉ |
36 | | cnextf.5 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β πΉ:π΄βΆπ΅) |
37 | 36 | frnd 6722 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β ran πΉ β π΅) |
38 | 35, 37 | sstrid 3992 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (πΉ β (π β© π΄)) β π΅) |
39 | | ssrin 4232 |
. . . . . . . . . . . . . . . . . . 19
β’ (π£ β π β (π£ β© π΄) β (π β© π΄)) |
40 | | imass2 6098 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π£ β© π΄) β (π β© π΄) β (πΉ β (π£ β© π΄)) β (πΉ β (π β© π΄))) |
41 | 39, 40 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π£ β π β (πΉ β (π£ β© π΄)) β (πΉ β (π β© π΄))) |
42 | | cnextf.2 |
. . . . . . . . . . . . . . . . . . 19
β’ π΅ = βͺ
πΎ |
43 | 42 | clsss 22549 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΎ β Top β§ (πΉ β (π β© π΄)) β π΅ β§ (πΉ β (π£ β© π΄)) β (πΉ β (π β© π΄))) β ((clsβπΎ)β(πΉ β (π£ β© π΄))) β ((clsβπΎ)β(πΉ β (π β© π΄)))) |
44 | 34, 38, 41, 43 | syl2an3an 1422 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π£ β π) β ((clsβπΎ)β(πΉ β (π£ β© π΄))) β ((clsβπΎ)β(πΉ β (π β© π΄)))) |
45 | | sstr 3989 |
. . . . . . . . . . . . . . . . 17
β’
((((clsβπΎ)β(πΉ β (π£ β© π΄))) β ((clsβπΎ)β(πΉ β (π β© π΄))) β§ ((clsβπΎ)β(πΉ β (π β© π΄))) β π€) β ((clsβπΎ)β(πΉ β (π£ β© π΄))) β π€) |
46 | 44, 45 | sylan 580 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π£ β π) β§ ((clsβπΎ)β(πΉ β (π β© π΄))) β π€) β ((clsβπΎ)β(πΉ β (π£ β© π΄))) β π€) |
47 | 46 | an32s 650 |
. . . . . . . . . . . . . . 15
β’ (((π β§ ((clsβπΎ)β(πΉ β (π β© π΄))) β π€) β§ π£ β π) β ((clsβπΎ)β(πΉ β (π£ β© π΄))) β π€) |
48 | 47 | ex 413 |
. . . . . . . . . . . . . 14
β’ ((π β§ ((clsβπΎ)β(πΉ β (π β© π΄))) β π€) β (π£ β π β ((clsβπΎ)β(πΉ β (π£ β© π΄))) β π€)) |
49 | 48 | anim2d 612 |
. . . . . . . . . . . . 13
β’ ((π β§ ((clsβπΎ)β(πΉ β (π β© π΄))) β π€) β ((π£ β π½ β§ π£ β π) β (π£ β π½ β§ ((clsβπΎ)β(πΉ β (π£ β© π΄))) β π€))) |
50 | 49 | anim2d 612 |
. . . . . . . . . . . 12
β’ ((π β§ ((clsβπΎ)β(πΉ β (π β© π΄))) β π€) β ((π£ β ((neiβπ½)β{π₯}) β§ (π£ β π½ β§ π£ β π)) β (π£ β ((neiβπ½)β{π₯}) β§ (π£ β π½ β§ ((clsβπΎ)β(πΉ β (π£ β© π΄))) β π€)))) |
51 | 31, 50 | syld 47 |
. . . . . . . . . . 11
β’ ((π β§ ((clsβπΎ)β(πΉ β (π β© π΄))) β π€) β ((π£ β π½ β§ ({π₯} β π£ β§ π£ β π)) β (π£ β ((neiβπ½)β{π₯}) β§ (π£ β π½ β§ ((clsβπΎ)β(πΉ β (π£ β© π΄))) β π€)))) |
52 | 51 | reximdv2 3164 |
. . . . . . . . . 10
β’ ((π β§ ((clsβπΎ)β(πΉ β (π β© π΄))) β π€) β (βπ£ β π½ ({π₯} β π£ β§ π£ β π) β βπ£ β ((neiβπ½)β{π₯})(π£ β π½ β§ ((clsβπΎ)β(πΉ β (π£ β© π΄))) β π€))) |
53 | 52 | imp 407 |
. . . . . . . . 9
β’ (((π β§ ((clsβπΎ)β(πΉ β (π β© π΄))) β π€) β§ βπ£ β π½ ({π₯} β π£ β§ π£ β π)) β βπ£ β ((neiβπ½)β{π₯})(π£ β π½ β§ ((clsβπΎ)β(πΉ β (π£ β© π΄))) β π€)) |
54 | 2, 3, 8, 53 | syl21anc 836 |
. . . . . . . 8
β’ (((π β§ π₯ β πΆ) β§ (π€ β ((neiβπΎ)β{(((π½CnExtπΎ)βπΉ)βπ₯)}) β§ π β ((neiβπ½)β{π₯}) β§ ((clsβπΎ)β(πΉ β (π β© π΄))) β π€)) β βπ£ β ((neiβπ½)β{π₯})(π£ β π½ β§ ((clsβπΎ)β(πΉ β (π£ β© π΄))) β π€)) |
55 | 54 | 3anassrs 1360 |
. . . . . . 7
β’
(((((π β§ π₯ β πΆ) β§ π€ β ((neiβπΎ)β{(((π½CnExtπΎ)βπΉ)βπ₯)})) β§ π β ((neiβπ½)β{π₯})) β§ ((clsβπΎ)β(πΉ β (π β© π΄))) β π€) β βπ£ β ((neiβπ½)β{π₯})(π£ β π½ β§ ((clsβπΎ)β(πΉ β (π£ β© π΄))) β π€)) |
56 | | simpr 485 |
. . . . . . . . 9
β’
(((((π β§ π₯ β πΆ) β§ π€ β ((neiβπΎ)β{(((π½CnExtπΎ)βπΉ)βπ₯)})) β§ π’ β (((neiβπ½)β{π₯}) βΎt π΄)) β§ ((clsβπΎ)β(πΉ β π’)) β π€) β ((clsβπΎ)β(πΉ β π’)) β π€) |
57 | | simp-4l 781 |
. . . . . . . . 9
β’
(((((π β§ π₯ β πΆ) β§ π€ β ((neiβπΎ)β{(((π½CnExtπΎ)βπΉ)βπ₯)})) β§ π’ β (((neiβπ½)β{π₯}) βΎt π΄)) β§ ((clsβπΎ)β(πΉ β π’)) β π€) β π) |
58 | | simplr 767 |
. . . . . . . . 9
β’
(((((π β§ π₯ β πΆ) β§ π€ β ((neiβπΎ)β{(((π½CnExtπΎ)βπΉ)βπ₯)})) β§ π’ β (((neiβπ½)β{π₯}) βΎt π΄)) β§ ((clsβπΎ)β(πΉ β π’)) β π€) β π’ β (((neiβπ½)β{π₯}) βΎt π΄)) |
59 | | imaeq2 6053 |
. . . . . . . . . . . . . 14
β’ (π’ = (π β© π΄) β (πΉ β π’) = (πΉ β (π β© π΄))) |
60 | 59 | fveq2d 6892 |
. . . . . . . . . . . . 13
β’ (π’ = (π β© π΄) β ((clsβπΎ)β(πΉ β π’)) = ((clsβπΎ)β(πΉ β (π β© π΄)))) |
61 | 60 | sseq1d 4012 |
. . . . . . . . . . . 12
β’ (π’ = (π β© π΄) β (((clsβπΎ)β(πΉ β π’)) β π€ β ((clsβπΎ)β(πΉ β (π β© π΄))) β π€)) |
62 | 61 | biimpcd 248 |
. . . . . . . . . . 11
β’
(((clsβπΎ)β(πΉ β π’)) β π€ β (π’ = (π β© π΄) β ((clsβπΎ)β(πΉ β (π β© π΄))) β π€)) |
63 | 62 | reximdv 3170 |
. . . . . . . . . 10
β’
(((clsβπΎ)β(πΉ β π’)) β π€ β (βπ β ((neiβπ½)β{π₯})π’ = (π β© π΄) β βπ β ((neiβπ½)β{π₯})((clsβπΎ)β(πΉ β (π β© π΄))) β π€)) |
64 | | fvexd 6903 |
. . . . . . . . . . . 12
β’ (π β ((neiβπ½)β{π₯}) β V) |
65 | | cnextf.1 |
. . . . . . . . . . . . . . . 16
β’ πΆ = βͺ
π½ |
66 | 65 | toptopon 22410 |
. . . . . . . . . . . . . . 15
β’ (π½ β Top β π½ β (TopOnβπΆ)) |
67 | 4, 66 | sylib 217 |
. . . . . . . . . . . . . 14
β’ (π β π½ β (TopOnβπΆ)) |
68 | 67 | elfvexd 6927 |
. . . . . . . . . . . . 13
β’ (π β πΆ β V) |
69 | | cnextf.a |
. . . . . . . . . . . . 13
β’ (π β π΄ β πΆ) |
70 | 68, 69 | ssexd 5323 |
. . . . . . . . . . . 12
β’ (π β π΄ β V) |
71 | | elrest 17369 |
. . . . . . . . . . . 12
β’
((((neiβπ½)β{π₯}) β V β§ π΄ β V) β (π’ β (((neiβπ½)β{π₯}) βΎt π΄) β βπ β ((neiβπ½)β{π₯})π’ = (π β© π΄))) |
72 | 64, 70, 71 | syl2anc 584 |
. . . . . . . . . . 11
β’ (π β (π’ β (((neiβπ½)β{π₯}) βΎt π΄) β βπ β ((neiβπ½)β{π₯})π’ = (π β© π΄))) |
73 | 72 | biimpa 477 |
. . . . . . . . . 10
β’ ((π β§ π’ β (((neiβπ½)β{π₯}) βΎt π΄)) β βπ β ((neiβπ½)β{π₯})π’ = (π β© π΄)) |
74 | 63, 73 | impel 506 |
. . . . . . . . 9
β’
((((clsβπΎ)β(πΉ β π’)) β π€ β§ (π β§ π’ β (((neiβπ½)β{π₯}) βΎt π΄))) β βπ β ((neiβπ½)β{π₯})((clsβπΎ)β(πΉ β (π β© π΄))) β π€) |
75 | 56, 57, 58, 74 | syl12anc 835 |
. . . . . . . 8
β’
(((((π β§ π₯ β πΆ) β§ π€ β ((neiβπΎ)β{(((π½CnExtπΎ)βπΉ)βπ₯)})) β§ π’ β (((neiβπ½)β{π₯}) βΎt π΄)) β§ ((clsβπΎ)β(πΉ β π’)) β π€) β βπ β ((neiβπ½)β{π₯})((clsβπΎ)β(πΉ β (π β© π΄))) β π€) |
76 | | cnextf.6 |
. . . . . . . . . . . . . . . 16
β’ (π β ((clsβπ½)βπ΄) = πΆ) |
77 | | eleq1w 2816 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ = π¦ β (π₯ β πΆ β π¦ β πΆ)) |
78 | 77 | anbi2d 629 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = π¦ β ((π β§ π₯ β πΆ) β (π β§ π¦ β πΆ))) |
79 | | sneq 4637 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π₯ = π¦ β {π₯} = {π¦}) |
80 | 79 | fveq2d 6892 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π₯ = π¦ β ((neiβπ½)β{π₯}) = ((neiβπ½)β{π¦})) |
81 | 80 | oveq1d 7420 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ = π¦ β (((neiβπ½)β{π₯}) βΎt π΄) = (((neiβπ½)β{π¦}) βΎt π΄)) |
82 | 81 | oveq2d 7421 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ = π¦ β (πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄)) = (πΎ fLimf (((neiβπ½)β{π¦}) βΎt π΄))) |
83 | 82 | fveq1d 6890 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ = π¦ β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ) = ((πΎ fLimf (((neiβπ½)β{π¦}) βΎt π΄))βπΉ)) |
84 | 83 | neeq1d 3000 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = π¦ β (((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ) β β
β ((πΎ fLimf (((neiβπ½)β{π¦}) βΎt π΄))βπΉ) β β
)) |
85 | 78, 84 | imbi12d 344 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = π¦ β (((π β§ π₯ β πΆ) β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ) β β
) β ((π β§ π¦ β πΆ) β ((πΎ fLimf (((neiβπ½)β{π¦}) βΎt π΄))βπΉ) β β
))) |
86 | | cnextf.7 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π₯ β πΆ) β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ) β β
) |
87 | 85, 86 | chvarvv 2002 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π¦ β πΆ) β ((πΎ fLimf (((neiβπ½)β{π¦}) βΎt π΄))βπΉ) β β
) |
88 | 65, 42, 4, 32, 36, 69, 76, 87 | cnextfvval 23560 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β πΆ) β (((π½CnExtπΎ)βπΉ)βπ₯) = βͺ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ)) |
89 | | fvex 6901 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ) β V |
90 | 89 | uniex 7727 |
. . . . . . . . . . . . . . . . 17
β’ βͺ ((πΎ
fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ) β V |
91 | 90 | snid 4663 |
. . . . . . . . . . . . . . . 16
β’ βͺ ((πΎ
fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ) β {βͺ
((πΎ fLimf
(((neiβπ½)β{π₯}) βΎt π΄))βπΉ)} |
92 | 32 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π₯ β πΆ) β πΎ β Haus) |
93 | 76 | eleq2d 2819 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (π₯ β ((clsβπ½)βπ΄) β π₯ β πΆ)) |
94 | 93 | biimpar 478 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π₯ β πΆ) β π₯ β ((clsβπ½)βπ΄)) |
95 | 67 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π₯ β πΆ) β π½ β (TopOnβπΆ)) |
96 | 69 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π₯ β πΆ) β π΄ β πΆ) |
97 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π₯ β πΆ) β π₯ β πΆ) |
98 | | trnei 23387 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π½ β (TopOnβπΆ) β§ π΄ β πΆ β§ π₯ β πΆ) β (π₯ β ((clsβπ½)βπ΄) β (((neiβπ½)β{π₯}) βΎt π΄) β (Filβπ΄))) |
99 | 95, 96, 97, 98 | syl3anc 1371 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π₯ β πΆ) β (π₯ β ((clsβπ½)βπ΄) β (((neiβπ½)β{π₯}) βΎt π΄) β (Filβπ΄))) |
100 | 94, 99 | mpbid 231 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π₯ β πΆ) β (((neiβπ½)β{π₯}) βΎt π΄) β (Filβπ΄)) |
101 | 36 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π₯ β πΆ) β πΉ:π΄βΆπ΅) |
102 | 42 | hausflf2 23493 |
. . . . . . . . . . . . . . . . . 18
β’ (((πΎ β Haus β§
(((neiβπ½)β{π₯}) βΎt π΄) β (Filβπ΄) β§ πΉ:π΄βΆπ΅) β§ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ) β β
) β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ) β 1o) |
103 | 92, 100, 101, 86, 102 | syl31anc 1373 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π₯ β πΆ) β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ) β 1o) |
104 | | en1b 9019 |
. . . . . . . . . . . . . . . . 17
β’ (((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ) β 1o β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ) = {βͺ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ)}) |
105 | 103, 104 | sylib 217 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β πΆ) β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ) = {βͺ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ)}) |
106 | 91, 105 | eleqtrrid 2840 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β πΆ) β βͺ
((πΎ fLimf
(((neiβπ½)β{π₯}) βΎt π΄))βπΉ) β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ)) |
107 | 88, 106 | eqeltrd 2833 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β πΆ) β (((π½CnExtπΎ)βπΉ)βπ₯) β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ)) |
108 | 42 | toptopon 22410 |
. . . . . . . . . . . . . . . . 17
β’ (πΎ β Top β πΎ β (TopOnβπ΅)) |
109 | 34, 108 | sylib 217 |
. . . . . . . . . . . . . . . 16
β’ (π β πΎ β (TopOnβπ΅)) |
110 | 109 | adantr 481 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β πΆ) β πΎ β (TopOnβπ΅)) |
111 | | flfnei 23486 |
. . . . . . . . . . . . . . 15
β’ ((πΎ β (TopOnβπ΅) β§ (((neiβπ½)β{π₯}) βΎt π΄) β (Filβπ΄) β§ πΉ:π΄βΆπ΅) β ((((π½CnExtπΎ)βπΉ)βπ₯) β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ) β ((((π½CnExtπΎ)βπΉ)βπ₯) β π΅ β§ βπ β ((neiβπΎ)β{(((π½CnExtπΎ)βπΉ)βπ₯)})βπ’ β (((neiβπ½)β{π₯}) βΎt π΄)(πΉ β π’) β π))) |
112 | 110, 100,
101, 111 | syl3anc 1371 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β πΆ) β ((((π½CnExtπΎ)βπΉ)βπ₯) β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ) β ((((π½CnExtπΎ)βπΉ)βπ₯) β π΅ β§ βπ β ((neiβπΎ)β{(((π½CnExtπΎ)βπΉ)βπ₯)})βπ’ β (((neiβπ½)β{π₯}) βΎt π΄)(πΉ β π’) β π))) |
113 | 107, 112 | mpbid 231 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β πΆ) β ((((π½CnExtπΎ)βπΉ)βπ₯) β π΅ β§ βπ β ((neiβπΎ)β{(((π½CnExtπΎ)βπΉ)βπ₯)})βπ’ β (((neiβπ½)β{π₯}) βΎt π΄)(πΉ β π’) β π)) |
114 | 113 | simprd 496 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β πΆ) β βπ β ((neiβπΎ)β{(((π½CnExtπΎ)βπΉ)βπ₯)})βπ’ β (((neiβπ½)β{π₯}) βΎt π΄)(πΉ β π’) β π) |
115 | 114 | r19.21bi 3248 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β πΆ) β§ π β ((neiβπΎ)β{(((π½CnExtπΎ)βπΉ)βπ₯)})) β βπ’ β (((neiβπ½)β{π₯}) βΎt π΄)(πΉ β π’) β π) |
116 | 115 | ad4ant13 749 |
. . . . . . . . . 10
β’
(((((π β§ π₯ β πΆ) β§ π€ β ((neiβπΎ)β{(((π½CnExtπΎ)βπΉ)βπ₯)})) β§ π β ((neiβπΎ)β{(((π½CnExtπΎ)βπΉ)βπ₯)})) β§ ((clsβπΎ)βπ) β π€) β βπ’ β (((neiβπ½)β{π₯}) βΎt π΄)(πΉ β π’) β π) |
117 | 34 | ad3antrrr 728 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β πΆ) β§ π β ((neiβπΎ)β{(((π½CnExtπΎ)βπΉ)βπ₯)})) β§ ((clsβπΎ)βπ) β π€) β πΎ β Top) |
118 | | simplr 767 |
. . . . . . . . . . . . 13
β’ ((((π β§ π₯ β πΆ) β§ π β ((neiβπΎ)β{(((π½CnExtπΎ)βπΉ)βπ₯)})) β§ ((clsβπΎ)βπ) β π€) β π β ((neiβπΎ)β{(((π½CnExtπΎ)βπΉ)βπ₯)})) |
119 | 42 | neii1 22601 |
. . . . . . . . . . . . 13
β’ ((πΎ β Top β§ π β ((neiβπΎ)β{(((π½CnExtπΎ)βπΉ)βπ₯)})) β π β π΅) |
120 | 117, 118,
119 | syl2anc 584 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β πΆ) β§ π β ((neiβπΎ)β{(((π½CnExtπΎ)βπΉ)βπ₯)})) β§ ((clsβπΎ)βπ) β π€) β π β π΅) |
121 | | simpr 485 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β πΆ) β§ π β ((neiβπΎ)β{(((π½CnExtπΎ)βπΉ)βπ₯)})) β§ ((clsβπΎ)βπ) β π€) β ((clsβπΎ)βπ) β π€) |
122 | 42 | clsss 22549 |
. . . . . . . . . . . . . . . 16
β’ ((πΎ β Top β§ π β π΅ β§ (πΉ β π’) β π) β ((clsβπΎ)β(πΉ β π’)) β ((clsβπΎ)βπ)) |
123 | | sstr 3989 |
. . . . . . . . . . . . . . . 16
β’
((((clsβπΎ)β(πΉ β π’)) β ((clsβπΎ)βπ) β§ ((clsβπΎ)βπ) β π€) β ((clsβπΎ)β(πΉ β π’)) β π€) |
124 | 122, 123 | sylan 580 |
. . . . . . . . . . . . . . 15
β’ (((πΎ β Top β§ π β π΅ β§ (πΉ β π’) β π) β§ ((clsβπΎ)βπ) β π€) β ((clsβπΎ)β(πΉ β π’)) β π€) |
125 | 124 | 3an1rs 1359 |
. . . . . . . . . . . . . 14
β’ (((πΎ β Top β§ π β π΅ β§ ((clsβπΎ)βπ) β π€) β§ (πΉ β π’) β π) β ((clsβπΎ)β(πΉ β π’)) β π€) |
126 | 125 | ex 413 |
. . . . . . . . . . . . 13
β’ ((πΎ β Top β§ π β π΅ β§ ((clsβπΎ)βπ) β π€) β ((πΉ β π’) β π β ((clsβπΎ)β(πΉ β π’)) β π€)) |
127 | 126 | reximdv 3170 |
. . . . . . . . . . . 12
β’ ((πΎ β Top β§ π β π΅ β§ ((clsβπΎ)βπ) β π€) β (βπ’ β (((neiβπ½)β{π₯}) βΎt π΄)(πΉ β π’) β π β βπ’ β (((neiβπ½)β{π₯}) βΎt π΄)((clsβπΎ)β(πΉ β π’)) β π€)) |
128 | 117, 120,
121, 127 | syl3anc 1371 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β πΆ) β§ π β ((neiβπΎ)β{(((π½CnExtπΎ)βπΉ)βπ₯)})) β§ ((clsβπΎ)βπ) β π€) β (βπ’ β (((neiβπ½)β{π₯}) βΎt π΄)(πΉ β π’) β π β βπ’ β (((neiβπ½)β{π₯}) βΎt π΄)((clsβπΎ)β(πΉ β π’)) β π€)) |
129 | 128 | adantllr 717 |
. . . . . . . . . 10
β’
(((((π β§ π₯ β πΆ) β§ π€ β ((neiβπΎ)β{(((π½CnExtπΎ)βπΉ)βπ₯)})) β§ π β ((neiβπΎ)β{(((π½CnExtπΎ)βπΉ)βπ₯)})) β§ ((clsβπΎ)βπ) β π€) β (βπ’ β (((neiβπ½)β{π₯}) βΎt π΄)(πΉ β π’) β π β βπ’ β (((neiβπ½)β{π₯}) βΎt π΄)((clsβπΎ)β(πΉ β π’)) β π€)) |
130 | 116, 129 | mpd 15 |
. . . . . . . . 9
β’
(((((π β§ π₯ β πΆ) β§ π€ β ((neiβπΎ)β{(((π½CnExtπΎ)βπΉ)βπ₯)})) β§ π β ((neiβπΎ)β{(((π½CnExtπΎ)βπΉ)βπ₯)})) β§ ((clsβπΎ)βπ) β π€) β βπ’ β (((neiβπ½)β{π₯}) βΎt π΄)((clsβπΎ)β(πΉ β π’)) β π€) |
131 | 34 | ad2antrr 724 |
. . . . . . . . . 10
β’ (((π β§ π₯ β πΆ) β§ π€ β ((neiβπΎ)β{(((π½CnExtπΎ)βπΉ)βπ₯)})) β πΎ β Top) |
132 | | cnextcn.8 |
. . . . . . . . . . . . . . 15
β’ (π β πΎ β Reg) |
133 | 132 | ad2antrr 724 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β πΆ) β§ π€ β ((neiβπΎ)β{(((π½CnExtπΎ)βπΉ)βπ₯)})) β πΎ β Reg) |
134 | 133 | ad2antrr 724 |
. . . . . . . . . . . . 13
β’
(((((π β§ π₯ β πΆ) β§ π€ β ((neiβπΎ)β{(((π½CnExtπΎ)βπΉ)βπ₯)})) β§ π β πΎ) β§ ((((π½CnExtπΎ)βπΉ)βπ₯) β π β§ π β π€)) β πΎ β Reg) |
135 | | simplr 767 |
. . . . . . . . . . . . 13
β’
(((((π β§ π₯ β πΆ) β§ π€ β ((neiβπΎ)β{(((π½CnExtπΎ)βπΉ)βπ₯)})) β§ π β πΎ) β§ ((((π½CnExtπΎ)βπΉ)βπ₯) β π β§ π β π€)) β π β πΎ) |
136 | | simprl 769 |
. . . . . . . . . . . . 13
β’
(((((π β§ π₯ β πΆ) β§ π€ β ((neiβπΎ)β{(((π½CnExtπΎ)βπΉ)βπ₯)})) β§ π β πΎ) β§ ((((π½CnExtπΎ)βπΉ)βπ₯) β π β§ π β π€)) β (((π½CnExtπΎ)βπΉ)βπ₯) β π) |
137 | | regsep 22829 |
. . . . . . . . . . . . 13
β’ ((πΎ β Reg β§ π β πΎ β§ (((π½CnExtπΎ)βπΉ)βπ₯) β π) β βπ β πΎ ((((π½CnExtπΎ)βπΉ)βπ₯) β π β§ ((clsβπΎ)βπ) β π)) |
138 | 134, 135,
136, 137 | syl3anc 1371 |
. . . . . . . . . . . 12
β’
(((((π β§ π₯ β πΆ) β§ π€ β ((neiβπΎ)β{(((π½CnExtπΎ)βπΉ)βπ₯)})) β§ π β πΎ) β§ ((((π½CnExtπΎ)βπΉ)βπ₯) β π β§ π β π€)) β βπ β πΎ ((((π½CnExtπΎ)βπΉ)βπ₯) β π β§ ((clsβπΎ)βπ) β π)) |
139 | | sstr 3989 |
. . . . . . . . . . . . . . . 16
β’
((((clsβπΎ)βπ) β π β§ π β π€) β ((clsβπΎ)βπ) β π€) |
140 | 139 | expcom 414 |
. . . . . . . . . . . . . . 15
β’ (π β π€ β (((clsβπΎ)βπ) β π β ((clsβπΎ)βπ) β π€)) |
141 | 140 | anim2d 612 |
. . . . . . . . . . . . . 14
β’ (π β π€ β (((((π½CnExtπΎ)βπΉ)βπ₯) β π β§ ((clsβπΎ)βπ) β π) β ((((π½CnExtπΎ)βπΉ)βπ₯) β π β§ ((clsβπΎ)βπ) β π€))) |
142 | 141 | reximdv 3170 |
. . . . . . . . . . . . 13
β’ (π β π€ β (βπ β πΎ ((((π½CnExtπΎ)βπΉ)βπ₯) β π β§ ((clsβπΎ)βπ) β π) β βπ β πΎ ((((π½CnExtπΎ)βπΉ)βπ₯) β π β§ ((clsβπΎ)βπ) β π€))) |
143 | 142 | ad2antll 727 |
. . . . . . . . . . . 12
β’
(((((π β§ π₯ β πΆ) β§ π€ β ((neiβπΎ)β{(((π½CnExtπΎ)βπΉ)βπ₯)})) β§ π β πΎ) β§ ((((π½CnExtπΎ)βπΉ)βπ₯) β π β§ π β π€)) β (βπ β πΎ ((((π½CnExtπΎ)βπΉ)βπ₯) β π β§ ((clsβπΎ)βπ) β π) β βπ β πΎ ((((π½CnExtπΎ)βπΉ)βπ₯) β π β§ ((clsβπΎ)βπ) β π€))) |
144 | 138, 143 | mpd 15 |
. . . . . . . . . . 11
β’
(((((π β§ π₯ β πΆ) β§ π€ β ((neiβπΎ)β{(((π½CnExtπΎ)βπΉ)βπ₯)})) β§ π β πΎ) β§ ((((π½CnExtπΎ)βπΉ)βπ₯) β π β§ π β π€)) β βπ β πΎ ((((π½CnExtπΎ)βπΉ)βπ₯) β π β§ ((clsβπΎ)βπ) β π€)) |
145 | | simpr 485 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β πΆ) β§ π€ β ((neiβπΎ)β{(((π½CnExtπΎ)βπΉ)βπ₯)})) β π€ β ((neiβπΎ)β{(((π½CnExtπΎ)βπΉ)βπ₯)})) |
146 | | neii2 22603 |
. . . . . . . . . . . . 13
β’ ((πΎ β Top β§ π€ β ((neiβπΎ)β{(((π½CnExtπΎ)βπΉ)βπ₯)})) β βπ β πΎ ({(((π½CnExtπΎ)βπΉ)βπ₯)} β π β§ π β π€)) |
147 | | fvex 6901 |
. . . . . . . . . . . . . . . . 17
β’ (((π½CnExtπΎ)βπΉ)βπ₯) β V |
148 | 147 | snss 4788 |
. . . . . . . . . . . . . . . 16
β’ ((((π½CnExtπΎ)βπΉ)βπ₯) β π β {(((π½CnExtπΎ)βπΉ)βπ₯)} β π) |
149 | 148 | anbi1i 624 |
. . . . . . . . . . . . . . 15
β’
(((((π½CnExtπΎ)βπΉ)βπ₯) β π β§ π β π€) β ({(((π½CnExtπΎ)βπΉ)βπ₯)} β π β§ π β π€)) |
150 | 149 | biimpri 227 |
. . . . . . . . . . . . . 14
β’
(({(((π½CnExtπΎ)βπΉ)βπ₯)} β π β§ π β π€) β ((((π½CnExtπΎ)βπΉ)βπ₯) β π β§ π β π€)) |
151 | 150 | reximi 3084 |
. . . . . . . . . . . . 13
β’
(βπ β
πΎ ({(((π½CnExtπΎ)βπΉ)βπ₯)} β π β§ π β π€) β βπ β πΎ ((((π½CnExtπΎ)βπΉ)βπ₯) β π β§ π β π€)) |
152 | 146, 151 | syl 17 |
. . . . . . . . . . . 12
β’ ((πΎ β Top β§ π€ β ((neiβπΎ)β{(((π½CnExtπΎ)βπΉ)βπ₯)})) β βπ β πΎ ((((π½CnExtπΎ)βπΉ)βπ₯) β π β§ π β π€)) |
153 | 131, 145,
152 | syl2anc 584 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β πΆ) β§ π€ β ((neiβπΎ)β{(((π½CnExtπΎ)βπΉ)βπ₯)})) β βπ β πΎ ((((π½CnExtπΎ)βπΉ)βπ₯) β π β§ π β π€)) |
154 | 144, 153 | r19.29a 3162 |
. . . . . . . . . 10
β’ (((π β§ π₯ β πΆ) β§ π€ β ((neiβπΎ)β{(((π½CnExtπΎ)βπΉ)βπ₯)})) β βπ β πΎ ((((π½CnExtπΎ)βπΉ)βπ₯) β π β§ ((clsβπΎ)βπ) β π€)) |
155 | | anass 469 |
. . . . . . . . . . . 12
β’ (((π β πΎ β§ (((π½CnExtπΎ)βπΉ)βπ₯) β π) β§ ((clsβπΎ)βπ) β π€) β (π β πΎ β§ ((((π½CnExtπΎ)βπΉ)βπ₯) β π β§ ((clsβπΎ)βπ) β π€))) |
156 | | opnneip 22614 |
. . . . . . . . . . . . . 14
β’ ((πΎ β Top β§ π β πΎ β§ (((π½CnExtπΎ)βπΉ)βπ₯) β π) β π β ((neiβπΎ)β{(((π½CnExtπΎ)βπΉ)βπ₯)})) |
157 | 156 | 3expib 1122 |
. . . . . . . . . . . . 13
β’ (πΎ β Top β ((π β πΎ β§ (((π½CnExtπΎ)βπΉ)βπ₯) β π) β π β ((neiβπΎ)β{(((π½CnExtπΎ)βπΉ)βπ₯)}))) |
158 | 157 | anim1d 611 |
. . . . . . . . . . . 12
β’ (πΎ β Top β (((π β πΎ β§ (((π½CnExtπΎ)βπΉ)βπ₯) β π) β§ ((clsβπΎ)βπ) β π€) β (π β ((neiβπΎ)β{(((π½CnExtπΎ)βπΉ)βπ₯)}) β§ ((clsβπΎ)βπ) β π€))) |
159 | 155, 158 | biimtrrid 242 |
. . . . . . . . . . 11
β’ (πΎ β Top β ((π β πΎ β§ ((((π½CnExtπΎ)βπΉ)βπ₯) β π β§ ((clsβπΎ)βπ) β π€)) β (π β ((neiβπΎ)β{(((π½CnExtπΎ)βπΉ)βπ₯)}) β§ ((clsβπΎ)βπ) β π€))) |
160 | 159 | reximdv2 3164 |
. . . . . . . . . 10
β’ (πΎ β Top β (βπ β πΎ ((((π½CnExtπΎ)βπΉ)βπ₯) β π β§ ((clsβπΎ)βπ) β π€) β βπ β ((neiβπΎ)β{(((π½CnExtπΎ)βπΉ)βπ₯)})((clsβπΎ)βπ) β π€)) |
161 | 131, 154,
160 | sylc 65 |
. . . . . . . . 9
β’ (((π β§ π₯ β πΆ) β§ π€ β ((neiβπΎ)β{(((π½CnExtπΎ)βπΉ)βπ₯)})) β βπ β ((neiβπΎ)β{(((π½CnExtπΎ)βπΉ)βπ₯)})((clsβπΎ)βπ) β π€) |
162 | 130, 161 | r19.29a 3162 |
. . . . . . . 8
β’ (((π β§ π₯ β πΆ) β§ π€ β ((neiβπΎ)β{(((π½CnExtπΎ)βπΉ)βπ₯)})) β βπ’ β (((neiβπ½)β{π₯}) βΎt π΄)((clsβπΎ)β(πΉ β π’)) β π€) |
163 | 75, 162 | r19.29a 3162 |
. . . . . . 7
β’ (((π β§ π₯ β πΆ) β§ π€ β ((neiβπΎ)β{(((π½CnExtπΎ)βπΉ)βπ₯)})) β βπ β ((neiβπ½)β{π₯})((clsβπΎ)β(πΉ β (π β© π΄))) β π€) |
164 | 55, 163 | r19.29a 3162 |
. . . . . 6
β’ (((π β§ π₯ β πΆ) β§ π€ β ((neiβπΎ)β{(((π½CnExtπΎ)βπΉ)βπ₯)})) β βπ£ β ((neiβπ½)β{π₯})(π£ β π½ β§ ((clsβπΎ)β(πΉ β (π£ β© π΄))) β π€)) |
165 | | simplr 767 |
. . . . . . . . . . 11
β’ ((((π β§ π£ β π½) β§ ((clsβπΎ)β(πΉ β (π£ β© π΄))) β π€) β§ π§ β π£) β ((clsβπΎ)β(πΉ β (π£ β© π΄))) β π€) |
166 | | simpll 765 |
. . . . . . . . . . . . 13
β’ (((π β§ π£ β π½) β§ π§ β π£) β π) |
167 | 4 | ad2antrr 724 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π£ β π½) β§ π§ β π£) β π½ β Top) |
168 | | simplr 767 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π£ β π½) β§ π§ β π£) β π£ β π½) |
169 | 65 | eltopss 22400 |
. . . . . . . . . . . . . . 15
β’ ((π½ β Top β§ π£ β π½) β π£ β πΆ) |
170 | 167, 168,
169 | syl2anc 584 |
. . . . . . . . . . . . . 14
β’ (((π β§ π£ β π½) β§ π§ β π£) β π£ β πΆ) |
171 | | simpr 485 |
. . . . . . . . . . . . . 14
β’ (((π β§ π£ β π½) β§ π§ β π£) β π§ β π£) |
172 | 170, 171 | sseldd 3982 |
. . . . . . . . . . . . 13
β’ (((π β§ π£ β π½) β§ π§ β π£) β π§ β πΆ) |
173 | | fvexd 6903 |
. . . . . . . . . . . . . 14
β’ (((π β§ π£ β π½) β§ π§ β π£) β ((neiβπ½)β{π§}) β V) |
174 | 70 | ad2antrr 724 |
. . . . . . . . . . . . . 14
β’ (((π β§ π£ β π½) β§ π§ β π£) β π΄ β V) |
175 | | opnneip 22614 |
. . . . . . . . . . . . . . . 16
β’ ((π½ β Top β§ π£ β π½ β§ π§ β π£) β π£ β ((neiβπ½)β{π§})) |
176 | 4, 175 | syl3an1 1163 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π£ β π½ β§ π§ β π£) β π£ β ((neiβπ½)β{π§})) |
177 | 176 | 3expa 1118 |
. . . . . . . . . . . . . 14
β’ (((π β§ π£ β π½) β§ π§ β π£) β π£ β ((neiβπ½)β{π§})) |
178 | | elrestr 17370 |
. . . . . . . . . . . . . 14
β’
((((neiβπ½)β{π§}) β V β§ π΄ β V β§ π£ β ((neiβπ½)β{π§})) β (π£ β© π΄) β (((neiβπ½)β{π§}) βΎt π΄)) |
179 | 173, 174,
177, 178 | syl3anc 1371 |
. . . . . . . . . . . . 13
β’ (((π β§ π£ β π½) β§ π§ β π£) β (π£ β© π΄) β (((neiβπ½)β{π§}) βΎt π΄)) |
180 | 65, 42, 4, 32, 36, 69, 76, 86 | cnextfvval 23560 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π§ β πΆ) β (((π½CnExtπΎ)βπΉ)βπ§) = βͺ ((πΎ fLimf (((neiβπ½)β{π§}) βΎt π΄))βπΉ)) |
181 | 180 | adantr 481 |
. . . . . . . . . . . . . 14
β’ (((π β§ π§ β πΆ) β§ (π£ β© π΄) β (((neiβπ½)β{π§}) βΎt π΄)) β (((π½CnExtπΎ)βπΉ)βπ§) = βͺ ((πΎ fLimf (((neiβπ½)β{π§}) βΎt π΄))βπΉ)) |
182 | 32 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π§ β πΆ) β πΎ β Haus) |
183 | 76 | eleq2d 2819 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (π§ β ((clsβπ½)βπ΄) β π§ β πΆ)) |
184 | 183 | biimpar 478 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π§ β πΆ) β π§ β ((clsβπ½)βπ΄)) |
185 | 67 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π§ β πΆ) β π½ β (TopOnβπΆ)) |
186 | 69 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π§ β πΆ) β π΄ β πΆ) |
187 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π§ β πΆ) β π§ β πΆ) |
188 | | trnei 23387 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π½ β (TopOnβπΆ) β§ π΄ β πΆ β§ π§ β πΆ) β (π§ β ((clsβπ½)βπ΄) β (((neiβπ½)β{π§}) βΎt π΄) β (Filβπ΄))) |
189 | 185, 186,
187, 188 | syl3anc 1371 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π§ β πΆ) β (π§ β ((clsβπ½)βπ΄) β (((neiβπ½)β{π§}) βΎt π΄) β (Filβπ΄))) |
190 | 184, 189 | mpbid 231 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π§ β πΆ) β (((neiβπ½)β{π§}) βΎt π΄) β (Filβπ΄)) |
191 | 36 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π§ β πΆ) β πΉ:π΄βΆπ΅) |
192 | | eleq1w 2816 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π₯ = π§ β (π₯ β πΆ β π§ β πΆ)) |
193 | 192 | anbi2d 629 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ = π§ β ((π β§ π₯ β πΆ) β (π β§ π§ β πΆ))) |
194 | | sneq 4637 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π₯ = π§ β {π₯} = {π§}) |
195 | 194 | fveq2d 6892 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π₯ = π§ β ((neiβπ½)β{π₯}) = ((neiβπ½)β{π§})) |
196 | 195 | oveq1d 7420 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π₯ = π§ β (((neiβπ½)β{π₯}) βΎt π΄) = (((neiβπ½)β{π§}) βΎt π΄)) |
197 | 196 | oveq2d 7421 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π₯ = π§ β (πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄)) = (πΎ fLimf (((neiβπ½)β{π§}) βΎt π΄))) |
198 | 197 | fveq1d 6890 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π₯ = π§ β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ) = ((πΎ fLimf (((neiβπ½)β{π§}) βΎt π΄))βπΉ)) |
199 | 198 | neeq1d 3000 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ = π§ β (((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ) β β
β ((πΎ fLimf (((neiβπ½)β{π§}) βΎt π΄))βπΉ) β β
)) |
200 | 193, 199 | imbi12d 344 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ = π§ β (((π β§ π₯ β πΆ) β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ) β β
) β ((π β§ π§ β πΆ) β ((πΎ fLimf (((neiβπ½)β{π§}) βΎt π΄))βπΉ) β β
))) |
201 | 200, 86 | chvarvv 2002 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π§ β πΆ) β ((πΎ fLimf (((neiβπ½)β{π§}) βΎt π΄))βπΉ) β β
) |
202 | 42 | hausflf2 23493 |
. . . . . . . . . . . . . . . . . . 19
β’ (((πΎ β Haus β§
(((neiβπ½)β{π§}) βΎt π΄) β (Filβπ΄) β§ πΉ:π΄βΆπ΅) β§ ((πΎ fLimf (((neiβπ½)β{π§}) βΎt π΄))βπΉ) β β
) β ((πΎ fLimf (((neiβπ½)β{π§}) βΎt π΄))βπΉ) β 1o) |
203 | 182, 190,
191, 201, 202 | syl31anc 1373 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π§ β πΆ) β ((πΎ fLimf (((neiβπ½)β{π§}) βΎt π΄))βπΉ) β 1o) |
204 | | en1b 9019 |
. . . . . . . . . . . . . . . . . 18
β’ (((πΎ fLimf (((neiβπ½)β{π§}) βΎt π΄))βπΉ) β 1o β ((πΎ fLimf (((neiβπ½)β{π§}) βΎt π΄))βπΉ) = {βͺ ((πΎ fLimf (((neiβπ½)β{π§}) βΎt π΄))βπΉ)}) |
205 | 203, 204 | sylib 217 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π§ β πΆ) β ((πΎ fLimf (((neiβπ½)β{π§}) βΎt π΄))βπΉ) = {βͺ ((πΎ fLimf (((neiβπ½)β{π§}) βΎt π΄))βπΉ)}) |
206 | 205 | adantr 481 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π§ β πΆ) β§ (π£ β© π΄) β (((neiβπ½)β{π§}) βΎt π΄)) β ((πΎ fLimf (((neiβπ½)β{π§}) βΎt π΄))βπΉ) = {βͺ ((πΎ fLimf (((neiβπ½)β{π§}) βΎt π΄))βπΉ)}) |
207 | 109 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π§ β πΆ) β πΎ β (TopOnβπ΅)) |
208 | | flfval 23485 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΎ β (TopOnβπ΅) β§ (((neiβπ½)β{π§}) βΎt π΄) β (Filβπ΄) β§ πΉ:π΄βΆπ΅) β ((πΎ fLimf (((neiβπ½)β{π§}) βΎt π΄))βπΉ) = (πΎ fLim ((π΅ FilMap πΉ)β(((neiβπ½)β{π§}) βΎt π΄)))) |
209 | 207, 190,
191, 208 | syl3anc 1371 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π§ β πΆ) β ((πΎ fLimf (((neiβπ½)β{π§}) βΎt π΄))βπΉ) = (πΎ fLim ((π΅ FilMap πΉ)β(((neiβπ½)β{π§}) βΎt π΄)))) |
210 | 209 | adantr 481 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π§ β πΆ) β§ (π£ β© π΄) β (((neiβπ½)β{π§}) βΎt π΄)) β ((πΎ fLimf (((neiβπ½)β{π§}) βΎt π΄))βπΉ) = (πΎ fLim ((π΅ FilMap πΉ)β(((neiβπ½)β{π§}) βΎt π΄)))) |
211 | 32 | uniexd 7728 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β βͺ πΎ
β V) |
212 | 211 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π§ β πΆ) β§ (π£ β© π΄) β (((neiβπ½)β{π§}) βΎt π΄)) β βͺ πΎ β V) |
213 | 42, 212 | eqeltrid 2837 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π§ β πΆ) β§ (π£ β© π΄) β (((neiβπ½)β{π§}) βΎt π΄)) β π΅ β V) |
214 | 190 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π§ β πΆ) β§ (π£ β© π΄) β (((neiβπ½)β{π§}) βΎt π΄)) β (((neiβπ½)β{π§}) βΎt π΄) β (Filβπ΄)) |
215 | | filfbas 23343 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((neiβπ½)β{π§}) βΎt π΄) β (Filβπ΄) β (((neiβπ½)β{π§}) βΎt π΄) β (fBasβπ΄)) |
216 | 214, 215 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π§ β πΆ) β§ (π£ β© π΄) β (((neiβπ½)β{π§}) βΎt π΄)) β (((neiβπ½)β{π§}) βΎt π΄) β (fBasβπ΄)) |
217 | 36 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π§ β πΆ) β§ (π£ β© π΄) β (((neiβπ½)β{π§}) βΎt π΄)) β πΉ:π΄βΆπ΅) |
218 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π§ β πΆ) β§ (π£ β© π΄) β (((neiβπ½)β{π§}) βΎt π΄)) β (π£ β© π΄) β (((neiβπ½)β{π§}) βΎt π΄)) |
219 | | fgfil 23370 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((((neiβπ½)β{π§}) βΎt π΄) β (Filβπ΄) β (π΄filGen(((neiβπ½)β{π§}) βΎt π΄)) = (((neiβπ½)β{π§}) βΎt π΄)) |
220 | 190, 219 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π§ β πΆ) β (π΄filGen(((neiβπ½)β{π§}) βΎt π΄)) = (((neiβπ½)β{π§}) βΎt π΄)) |
221 | 220 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π§ β πΆ) β§ (π£ β© π΄) β (((neiβπ½)β{π§}) βΎt π΄)) β (π΄filGen(((neiβπ½)β{π§}) βΎt π΄)) = (((neiβπ½)β{π§}) βΎt π΄)) |
222 | 218, 221 | eleqtrrd 2836 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π§ β πΆ) β§ (π£ β© π΄) β (((neiβπ½)β{π§}) βΎt π΄)) β (π£ β© π΄) β (π΄filGen(((neiβπ½)β{π§}) βΎt π΄))) |
223 | | eqid 2732 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π΄filGen(((neiβπ½)β{π§}) βΎt π΄)) = (π΄filGen(((neiβπ½)β{π§}) βΎt π΄)) |
224 | 223 | imaelfm 23446 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π΅ β V β§
(((neiβπ½)β{π§}) βΎt π΄) β (fBasβπ΄) β§ πΉ:π΄βΆπ΅) β§ (π£ β© π΄) β (π΄filGen(((neiβπ½)β{π§}) βΎt π΄))) β (πΉ β (π£ β© π΄)) β ((π΅ FilMap πΉ)β(((neiβπ½)β{π§}) βΎt π΄))) |
225 | 213, 216,
217, 222, 224 | syl31anc 1373 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π§ β πΆ) β§ (π£ β© π΄) β (((neiβπ½)β{π§}) βΎt π΄)) β (πΉ β (π£ β© π΄)) β ((π΅ FilMap πΉ)β(((neiβπ½)β{π§}) βΎt π΄))) |
226 | | flimclsi 23473 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΉ β (π£ β© π΄)) β ((π΅ FilMap πΉ)β(((neiβπ½)β{π§}) βΎt π΄)) β (πΎ fLim ((π΅ FilMap πΉ)β(((neiβπ½)β{π§}) βΎt π΄))) β ((clsβπΎ)β(πΉ β (π£ β© π΄)))) |
227 | 225, 226 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π§ β πΆ) β§ (π£ β© π΄) β (((neiβπ½)β{π§}) βΎt π΄)) β (πΎ fLim ((π΅ FilMap πΉ)β(((neiβπ½)β{π§}) βΎt π΄))) β ((clsβπΎ)β(πΉ β (π£ β© π΄)))) |
228 | 210, 227 | eqsstrd 4019 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π§ β πΆ) β§ (π£ β© π΄) β (((neiβπ½)β{π§}) βΎt π΄)) β ((πΎ fLimf (((neiβπ½)β{π§}) βΎt π΄))βπΉ) β ((clsβπΎ)β(πΉ β (π£ β© π΄)))) |
229 | 206, 228 | eqsstrrd 4020 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π§ β πΆ) β§ (π£ β© π΄) β (((neiβπ½)β{π§}) βΎt π΄)) β {βͺ
((πΎ fLimf
(((neiβπ½)β{π§}) βΎt π΄))βπΉ)} β ((clsβπΎ)β(πΉ β (π£ β© π΄)))) |
230 | | fvex 6901 |
. . . . . . . . . . . . . . . . 17
β’ ((πΎ fLimf (((neiβπ½)β{π§}) βΎt π΄))βπΉ) β V |
231 | 230 | uniex 7727 |
. . . . . . . . . . . . . . . 16
β’ βͺ ((πΎ
fLimf (((neiβπ½)β{π§}) βΎt π΄))βπΉ) β V |
232 | 231 | snss 4788 |
. . . . . . . . . . . . . . 15
β’ (βͺ ((πΎ
fLimf (((neiβπ½)β{π§}) βΎt π΄))βπΉ) β ((clsβπΎ)β(πΉ β (π£ β© π΄))) β {βͺ
((πΎ fLimf
(((neiβπ½)β{π§}) βΎt π΄))βπΉ)} β ((clsβπΎ)β(πΉ β (π£ β© π΄)))) |
233 | 229, 232 | sylibr 233 |
. . . . . . . . . . . . . 14
β’ (((π β§ π§ β πΆ) β§ (π£ β© π΄) β (((neiβπ½)β{π§}) βΎt π΄)) β βͺ
((πΎ fLimf
(((neiβπ½)β{π§}) βΎt π΄))βπΉ) β ((clsβπΎ)β(πΉ β (π£ β© π΄)))) |
234 | 181, 233 | eqeltrd 2833 |
. . . . . . . . . . . . 13
β’ (((π β§ π§ β πΆ) β§ (π£ β© π΄) β (((neiβπ½)β{π§}) βΎt π΄)) β (((π½CnExtπΎ)βπΉ)βπ§) β ((clsβπΎ)β(πΉ β (π£ β© π΄)))) |
235 | 166, 172,
179, 234 | syl21anc 836 |
. . . . . . . . . . . 12
β’ (((π β§ π£ β π½) β§ π§ β π£) β (((π½CnExtπΎ)βπΉ)βπ§) β ((clsβπΎ)β(πΉ β (π£ β© π΄)))) |
236 | 235 | adantlr 713 |
. . . . . . . . . . 11
β’ ((((π β§ π£ β π½) β§ ((clsβπΎ)β(πΉ β (π£ β© π΄))) β π€) β§ π§ β π£) β (((π½CnExtπΎ)βπΉ)βπ§) β ((clsβπΎ)β(πΉ β (π£ β© π΄)))) |
237 | 165, 236 | sseldd 3982 |
. . . . . . . . . 10
β’ ((((π β§ π£ β π½) β§ ((clsβπΎ)β(πΉ β (π£ β© π΄))) β π€) β§ π§ β π£) β (((π½CnExtπΎ)βπΉ)βπ§) β π€) |
238 | 237 | ralrimiva 3146 |
. . . . . . . . 9
β’ (((π β§ π£ β π½) β§ ((clsβπΎ)β(πΉ β (π£ β© π΄))) β π€) β βπ§ β π£ (((π½CnExtπΎ)βπΉ)βπ§) β π€) |
239 | 238 | expl 458 |
. . . . . . . 8
β’ (π β ((π£ β π½ β§ ((clsβπΎ)β(πΉ β (π£ β© π΄))) β π€) β βπ§ β π£ (((π½CnExtπΎ)βπΉ)βπ§) β π€)) |
240 | 239 | reximdv 3170 |
. . . . . . 7
β’ (π β (βπ£ β ((neiβπ½)β{π₯})(π£ β π½ β§ ((clsβπΎ)β(πΉ β (π£ β© π΄))) β π€) β βπ£ β ((neiβπ½)β{π₯})βπ§ β π£ (((π½CnExtπΎ)βπΉ)βπ§) β π€)) |
241 | 240 | ad2antrr 724 |
. . . . . 6
β’ (((π β§ π₯ β πΆ) β§ π€ β ((neiβπΎ)β{(((π½CnExtπΎ)βπΉ)βπ₯)})) β (βπ£ β ((neiβπ½)β{π₯})(π£ β π½ β§ ((clsβπΎ)β(πΉ β (π£ β© π΄))) β π€) β βπ£ β ((neiβπ½)β{π₯})βπ§ β π£ (((π½CnExtπΎ)βπΉ)βπ§) β π€)) |
242 | 164, 241 | mpd 15 |
. . . . 5
β’ (((π β§ π₯ β πΆ) β§ π€ β ((neiβπΎ)β{(((π½CnExtπΎ)βπΉ)βπ₯)})) β βπ£ β ((neiβπ½)β{π₯})βπ§ β π£ (((π½CnExtπΎ)βπΉ)βπ§) β π€) |
243 | 65, 42, 4, 32, 36, 69, 76, 86 | cnextf 23561 |
. . . . . . . . . 10
β’ (π β ((π½CnExtπΎ)βπΉ):πΆβΆπ΅) |
244 | 243 | ffund 6718 |
. . . . . . . . 9
β’ (π β Fun ((π½CnExtπΎ)βπΉ)) |
245 | 244 | adantr 481 |
. . . . . . . 8
β’ ((π β§ π£ β ((neiβπ½)β{π₯})) β Fun ((π½CnExtπΎ)βπΉ)) |
246 | 65 | neii1 22601 |
. . . . . . . . . 10
β’ ((π½ β Top β§ π£ β ((neiβπ½)β{π₯})) β π£ β πΆ) |
247 | 4, 246 | sylan 580 |
. . . . . . . . 9
β’ ((π β§ π£ β ((neiβπ½)β{π₯})) β π£ β πΆ) |
248 | 243 | fdmd 6725 |
. . . . . . . . . 10
β’ (π β dom ((π½CnExtπΎ)βπΉ) = πΆ) |
249 | 248 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ π£ β ((neiβπ½)β{π₯})) β dom ((π½CnExtπΎ)βπΉ) = πΆ) |
250 | 247, 249 | sseqtrrd 4022 |
. . . . . . . 8
β’ ((π β§ π£ β ((neiβπ½)β{π₯})) β π£ β dom ((π½CnExtπΎ)βπΉ)) |
251 | | funimass4 6953 |
. . . . . . . 8
β’ ((Fun
((π½CnExtπΎ)βπΉ) β§ π£ β dom ((π½CnExtπΎ)βπΉ)) β ((((π½CnExtπΎ)βπΉ) β π£) β π€ β βπ§ β π£ (((π½CnExtπΎ)βπΉ)βπ§) β π€)) |
252 | 245, 250,
251 | syl2anc 584 |
. . . . . . 7
β’ ((π β§ π£ β ((neiβπ½)β{π₯})) β ((((π½CnExtπΎ)βπΉ) β π£) β π€ β βπ§ β π£ (((π½CnExtπΎ)βπΉ)βπ§) β π€)) |
253 | 252 | biimprd 247 |
. . . . . 6
β’ ((π β§ π£ β ((neiβπ½)β{π₯})) β (βπ§ β π£ (((π½CnExtπΎ)βπΉ)βπ§) β π€ β (((π½CnExtπΎ)βπΉ) β π£) β π€)) |
254 | 253 | reximdva 3168 |
. . . . 5
β’ (π β (βπ£ β ((neiβπ½)β{π₯})βπ§ β π£ (((π½CnExtπΎ)βπΉ)βπ§) β π€ β βπ£ β ((neiβπ½)β{π₯})(((π½CnExtπΎ)βπΉ) β π£) β π€)) |
255 | 1, 242, 254 | sylc 65 |
. . . 4
β’ (((π β§ π₯ β πΆ) β§ π€ β ((neiβπΎ)β{(((π½CnExtπΎ)βπΉ)βπ₯)})) β βπ£ β ((neiβπ½)β{π₯})(((π½CnExtπΎ)βπΉ) β π£) β π€) |
256 | 255 | ralrimiva 3146 |
. . 3
β’ ((π β§ π₯ β πΆ) β βπ€ β ((neiβπΎ)β{(((π½CnExtπΎ)βπΉ)βπ₯)})βπ£ β ((neiβπ½)β{π₯})(((π½CnExtπΎ)βπΉ) β π£) β π€) |
257 | 256 | ralrimiva 3146 |
. 2
β’ (π β βπ₯ β πΆ βπ€ β ((neiβπΎ)β{(((π½CnExtπΎ)βπΉ)βπ₯)})βπ£ β ((neiβπ½)β{π₯})(((π½CnExtπΎ)βπΉ) β π£) β π€) |
258 | 65, 42 | cnnei 22777 |
. . 3
β’ ((π½ β Top β§ πΎ β Top β§ ((π½CnExtπΎ)βπΉ):πΆβΆπ΅) β (((π½CnExtπΎ)βπΉ) β (π½ Cn πΎ) β βπ₯ β πΆ βπ€ β ((neiβπΎ)β{(((π½CnExtπΎ)βπΉ)βπ₯)})βπ£ β ((neiβπ½)β{π₯})(((π½CnExtπΎ)βπΉ) β π£) β π€)) |
259 | 4, 34, 243, 258 | syl3anc 1371 |
. 2
β’ (π β (((π½CnExtπΎ)βπΉ) β (π½ Cn πΎ) β βπ₯ β πΆ βπ€ β ((neiβπΎ)β{(((π½CnExtπΎ)βπΉ)βπ₯)})βπ£ β ((neiβπ½)β{π₯})(((π½CnExtπΎ)βπΉ) β π£) β π€)) |
260 | 257, 259 | mpbird 256 |
1
β’ (π β ((π½CnExtπΎ)βπΉ) β (π½ Cn πΎ)) |