Step | Hyp | Ref
| Expression |
1 | | cnextf.1 |
. . . . 5
β’ πΆ = βͺ
π½ |
2 | | cnextf.2 |
. . . . 5
β’ π΅ = βͺ
πΎ |
3 | | cnextf.3 |
. . . . 5
β’ (π β π½ β Top) |
4 | | cnextf.4 |
. . . . 5
β’ (π β πΎ β Haus) |
5 | | cnextf.5 |
. . . . 5
β’ (π β πΉ:π΄βΆπ΅) |
6 | | cnextf.a |
. . . . 5
β’ (π β π΄ β πΆ) |
7 | | cnextf.6 |
. . . . 5
β’ (π β ((clsβπ½)βπ΄) = πΆ) |
8 | | cnextf.7 |
. . . . 5
β’ ((π β§ π₯ β πΆ) β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ) β β
) |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | cnextf 23440 |
. . . 4
β’ (π β ((π½CnExtπΎ)βπΉ):πΆβΆπ΅) |
10 | 9 | ffnd 6673 |
. . 3
β’ (π β ((π½CnExtπΎ)βπΉ) Fn πΆ) |
11 | | fnssres 6628 |
. . 3
β’ ((((π½CnExtπΎ)βπΉ) Fn πΆ β§ π΄ β πΆ) β (((π½CnExtπΎ)βπΉ) βΎ π΄) Fn π΄) |
12 | 10, 6, 11 | syl2anc 585 |
. 2
β’ (π β (((π½CnExtπΎ)βπΉ) βΎ π΄) Fn π΄) |
13 | 5 | ffnd 6673 |
. 2
β’ (π β πΉ Fn π΄) |
14 | | fvres 6865 |
. . . 4
β’ (π¦ β π΄ β ((((π½CnExtπΎ)βπΉ) βΎ π΄)βπ¦) = (((π½CnExtπΎ)βπΉ)βπ¦)) |
15 | 14 | adantl 483 |
. . 3
β’ ((π β§ π¦ β π΄) β ((((π½CnExtπΎ)βπΉ) βΎ π΄)βπ¦) = (((π½CnExtπΎ)βπΉ)βπ¦)) |
16 | 6 | sselda 3948 |
. . . 4
β’ ((π β§ π¦ β π΄) β π¦ β πΆ) |
17 | 1, 2, 3, 4, 5, 6, 7, 8 | cnextfvval 23439 |
. . . 4
β’ ((π β§ π¦ β πΆ) β (((π½CnExtπΎ)βπΉ)βπ¦) = βͺ ((πΎ fLimf (((neiβπ½)β{π¦}) βΎt π΄))βπΉ)) |
18 | 16, 17 | syldan 592 |
. . 3
β’ ((π β§ π¦ β π΄) β (((π½CnExtπΎ)βπΉ)βπ¦) = βͺ ((πΎ fLimf (((neiβπ½)β{π¦}) βΎt π΄))βπΉ)) |
19 | 5 | ffvelcdmda 7039 |
. . . . . . 7
β’ ((π β§ π¦ β π΄) β (πΉβπ¦) β π΅) |
20 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β π΄) β π¦ β π΄) |
21 | 1 | restuni 22536 |
. . . . . . . . . . . . . 14
β’ ((π½ β Top β§ π΄ β πΆ) β π΄ = βͺ (π½ βΎt π΄)) |
22 | 3, 6, 21 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (π β π΄ = βͺ (π½ βΎt π΄)) |
23 | 22 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β π΄) β π΄ = βͺ (π½ βΎt π΄)) |
24 | 20, 23 | eleqtrd 2836 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β π΄) β π¦ β βͺ (π½ βΎt π΄)) |
25 | | cnextfres1.1 |
. . . . . . . . . . . . 13
β’ (π β πΉ β ((π½ βΎt π΄) Cn πΎ)) |
26 | | fvex 6859 |
. . . . . . . . . . . . . . . . 17
β’
((clsβπ½)βπ΄) β V |
27 | 7, 26 | eqeltrrdi 2843 |
. . . . . . . . . . . . . . . 16
β’ (π β πΆ β V) |
28 | 27, 6 | ssexd 5285 |
. . . . . . . . . . . . . . 15
β’ (π β π΄ β V) |
29 | | resttop 22534 |
. . . . . . . . . . . . . . 15
β’ ((π½ β Top β§ π΄ β V) β (π½ βΎt π΄) β Top) |
30 | 3, 28, 29 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (π β (π½ βΎt π΄) β Top) |
31 | | haustop 22705 |
. . . . . . . . . . . . . . 15
β’ (πΎ β Haus β πΎ β Top) |
32 | 4, 31 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β πΎ β Top) |
33 | 22 | feq2d 6658 |
. . . . . . . . . . . . . . 15
β’ (π β (πΉ:π΄βΆπ΅ β πΉ:βͺ (π½ βΎt π΄)βΆπ΅)) |
34 | 5, 33 | mpbid 231 |
. . . . . . . . . . . . . 14
β’ (π β πΉ:βͺ (π½ βΎt π΄)βΆπ΅) |
35 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’ βͺ (π½
βΎt π΄) =
βͺ (π½ βΎt π΄) |
36 | 35, 2 | cnnei 22656 |
. . . . . . . . . . . . . 14
β’ (((π½ βΎt π΄) β Top β§ πΎ β Top β§ πΉ:βͺ
(π½ βΎt
π΄)βΆπ΅) β (πΉ β ((π½ βΎt π΄) Cn πΎ) β βπ¦ β βͺ (π½ βΎt π΄)βπ€ β ((neiβπΎ)β{(πΉβπ¦)})βπ£ β ((neiβ(π½ βΎt π΄))β{π¦})(πΉ β π£) β π€)) |
37 | 30, 32, 34, 36 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ (π β (πΉ β ((π½ βΎt π΄) Cn πΎ) β βπ¦ β βͺ (π½ βΎt π΄)βπ€ β ((neiβπΎ)β{(πΉβπ¦)})βπ£ β ((neiβ(π½ βΎt π΄))β{π¦})(πΉ β π£) β π€)) |
38 | 25, 37 | mpbid 231 |
. . . . . . . . . . . 12
β’ (π β βπ¦ β βͺ (π½ βΎt π΄)βπ€ β ((neiβπΎ)β{(πΉβπ¦)})βπ£ β ((neiβ(π½ βΎt π΄))β{π¦})(πΉ β π£) β π€) |
39 | 38 | r19.21bi 3233 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β βͺ (π½ βΎt π΄)) β βπ€ β ((neiβπΎ)β{(πΉβπ¦)})βπ£ β ((neiβ(π½ βΎt π΄))β{π¦})(πΉ β π£) β π€) |
40 | 24, 39 | syldan 592 |
. . . . . . . . . 10
β’ ((π β§ π¦ β π΄) β βπ€ β ((neiβπΎ)β{(πΉβπ¦)})βπ£ β ((neiβ(π½ βΎt π΄))β{π¦})(πΉ β π£) β π€) |
41 | 40 | r19.21bi 3233 |
. . . . . . . . 9
β’ (((π β§ π¦ β π΄) β§ π€ β ((neiβπΎ)β{(πΉβπ¦)})) β βπ£ β ((neiβ(π½ βΎt π΄))β{π¦})(πΉ β π£) β π€) |
42 | | snssi 4772 |
. . . . . . . . . . . 12
β’ (π¦ β π΄ β {π¦} β π΄) |
43 | 1 | neitr 22554 |
. . . . . . . . . . . 12
β’ ((π½ β Top β§ π΄ β πΆ β§ {π¦} β π΄) β ((neiβ(π½ βΎt π΄))β{π¦}) = (((neiβπ½)β{π¦}) βΎt π΄)) |
44 | 3, 6, 42, 43 | syl2an3an 1423 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β π΄) β ((neiβ(π½ βΎt π΄))β{π¦}) = (((neiβπ½)β{π¦}) βΎt π΄)) |
45 | 44 | rexeqdv 3313 |
. . . . . . . . . 10
β’ ((π β§ π¦ β π΄) β (βπ£ β ((neiβ(π½ βΎt π΄))β{π¦})(πΉ β π£) β π€ β βπ£ β (((neiβπ½)β{π¦}) βΎt π΄)(πΉ β π£) β π€)) |
46 | 45 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ π¦ β π΄) β§ π€ β ((neiβπΎ)β{(πΉβπ¦)})) β (βπ£ β ((neiβ(π½ βΎt π΄))β{π¦})(πΉ β π£) β π€ β βπ£ β (((neiβπ½)β{π¦}) βΎt π΄)(πΉ β π£) β π€)) |
47 | 41, 46 | mpbid 231 |
. . . . . . . 8
β’ (((π β§ π¦ β π΄) β§ π€ β ((neiβπΎ)β{(πΉβπ¦)})) β βπ£ β (((neiβπ½)β{π¦}) βΎt π΄)(πΉ β π£) β π€) |
48 | 47 | ralrimiva 3140 |
. . . . . . 7
β’ ((π β§ π¦ β π΄) β βπ€ β ((neiβπΎ)β{(πΉβπ¦)})βπ£ β (((neiβπ½)β{π¦}) βΎt π΄)(πΉ β π£) β π€) |
49 | 4 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π¦ β π΄) β πΎ β Haus) |
50 | 2 | toptopon 22289 |
. . . . . . . . . 10
β’ (πΎ β Top β πΎ β (TopOnβπ΅)) |
51 | 50 | biimpi 215 |
. . . . . . . . 9
β’ (πΎ β Top β πΎ β (TopOnβπ΅)) |
52 | 49, 31, 51 | 3syl 18 |
. . . . . . . 8
β’ ((π β§ π¦ β π΄) β πΎ β (TopOnβπ΅)) |
53 | 7 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π¦ β π΄) β ((clsβπ½)βπ΄) = πΆ) |
54 | 16, 53 | eleqtrrd 2837 |
. . . . . . . . 9
β’ ((π β§ π¦ β π΄) β π¦ β ((clsβπ½)βπ΄)) |
55 | 1 | toptopon 22289 |
. . . . . . . . . . . 12
β’ (π½ β Top β π½ β (TopOnβπΆ)) |
56 | 3, 55 | sylib 217 |
. . . . . . . . . . 11
β’ (π β π½ β (TopOnβπΆ)) |
57 | 56 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π¦ β π΄) β π½ β (TopOnβπΆ)) |
58 | 6 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π¦ β π΄) β π΄ β πΆ) |
59 | | trnei 23266 |
. . . . . . . . . 10
β’ ((π½ β (TopOnβπΆ) β§ π΄ β πΆ β§ π¦ β πΆ) β (π¦ β ((clsβπ½)βπ΄) β (((neiβπ½)β{π¦}) βΎt π΄) β (Filβπ΄))) |
60 | 57, 58, 16, 59 | syl3anc 1372 |
. . . . . . . . 9
β’ ((π β§ π¦ β π΄) β (π¦ β ((clsβπ½)βπ΄) β (((neiβπ½)β{π¦}) βΎt π΄) β (Filβπ΄))) |
61 | 54, 60 | mpbid 231 |
. . . . . . . 8
β’ ((π β§ π¦ β π΄) β (((neiβπ½)β{π¦}) βΎt π΄) β (Filβπ΄)) |
62 | 5 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π¦ β π΄) β πΉ:π΄βΆπ΅) |
63 | | flfnei 23365 |
. . . . . . . 8
β’ ((πΎ β (TopOnβπ΅) β§ (((neiβπ½)β{π¦}) βΎt π΄) β (Filβπ΄) β§ πΉ:π΄βΆπ΅) β ((πΉβπ¦) β ((πΎ fLimf (((neiβπ½)β{π¦}) βΎt π΄))βπΉ) β ((πΉβπ¦) β π΅ β§ βπ€ β ((neiβπΎ)β{(πΉβπ¦)})βπ£ β (((neiβπ½)β{π¦}) βΎt π΄)(πΉ β π£) β π€))) |
64 | 52, 61, 62, 63 | syl3anc 1372 |
. . . . . . 7
β’ ((π β§ π¦ β π΄) β ((πΉβπ¦) β ((πΎ fLimf (((neiβπ½)β{π¦}) βΎt π΄))βπΉ) β ((πΉβπ¦) β π΅ β§ βπ€ β ((neiβπΎ)β{(πΉβπ¦)})βπ£ β (((neiβπ½)β{π¦}) βΎt π΄)(πΉ β π£) β π€))) |
65 | 19, 48, 64 | mpbir2and 712 |
. . . . . 6
β’ ((π β§ π¦ β π΄) β (πΉβπ¦) β ((πΎ fLimf (((neiβπ½)β{π¦}) βΎt π΄))βπΉ)) |
66 | | eleq1w 2817 |
. . . . . . . . . . 11
β’ (π₯ = π¦ β (π₯ β πΆ β π¦ β πΆ)) |
67 | 66 | anbi2d 630 |
. . . . . . . . . 10
β’ (π₯ = π¦ β ((π β§ π₯ β πΆ) β (π β§ π¦ β πΆ))) |
68 | | sneq 4600 |
. . . . . . . . . . . . . . 15
β’ (π₯ = π¦ β {π₯} = {π¦}) |
69 | 68 | fveq2d 6850 |
. . . . . . . . . . . . . 14
β’ (π₯ = π¦ β ((neiβπ½)β{π₯}) = ((neiβπ½)β{π¦})) |
70 | 69 | oveq1d 7376 |
. . . . . . . . . . . . 13
β’ (π₯ = π¦ β (((neiβπ½)β{π₯}) βΎt π΄) = (((neiβπ½)β{π¦}) βΎt π΄)) |
71 | 70 | oveq2d 7377 |
. . . . . . . . . . . 12
β’ (π₯ = π¦ β (πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄)) = (πΎ fLimf (((neiβπ½)β{π¦}) βΎt π΄))) |
72 | 71 | fveq1d 6848 |
. . . . . . . . . . 11
β’ (π₯ = π¦ β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ) = ((πΎ fLimf (((neiβπ½)β{π¦}) βΎt π΄))βπΉ)) |
73 | 72 | neeq1d 3000 |
. . . . . . . . . 10
β’ (π₯ = π¦ β (((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ) β β
β ((πΎ fLimf (((neiβπ½)β{π¦}) βΎt π΄))βπΉ) β β
)) |
74 | 67, 73 | imbi12d 345 |
. . . . . . . . 9
β’ (π₯ = π¦ β (((π β§ π₯ β πΆ) β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ) β β
) β ((π β§ π¦ β πΆ) β ((πΎ fLimf (((neiβπ½)β{π¦}) βΎt π΄))βπΉ) β β
))) |
75 | 74, 8 | chvarvv 2003 |
. . . . . . . 8
β’ ((π β§ π¦ β πΆ) β ((πΎ fLimf (((neiβπ½)β{π¦}) βΎt π΄))βπΉ) β β
) |
76 | 16, 75 | syldan 592 |
. . . . . . 7
β’ ((π β§ π¦ β π΄) β ((πΎ fLimf (((neiβπ½)β{π¦}) βΎt π΄))βπΉ) β β
) |
77 | 2 | hausflf2 23372 |
. . . . . . 7
β’ (((πΎ β Haus β§
(((neiβπ½)β{π¦}) βΎt π΄) β (Filβπ΄) β§ πΉ:π΄βΆπ΅) β§ ((πΎ fLimf (((neiβπ½)β{π¦}) βΎt π΄))βπΉ) β β
) β ((πΎ fLimf (((neiβπ½)β{π¦}) βΎt π΄))βπΉ) β 1o) |
78 | 49, 61, 62, 76, 77 | syl31anc 1374 |
. . . . . 6
β’ ((π β§ π¦ β π΄) β ((πΎ fLimf (((neiβπ½)β{π¦}) βΎt π΄))βπΉ) β 1o) |
79 | | en1eqsn 9224 |
. . . . . 6
β’ (((πΉβπ¦) β ((πΎ fLimf (((neiβπ½)β{π¦}) βΎt π΄))βπΉ) β§ ((πΎ fLimf (((neiβπ½)β{π¦}) βΎt π΄))βπΉ) β 1o) β ((πΎ fLimf (((neiβπ½)β{π¦}) βΎt π΄))βπΉ) = {(πΉβπ¦)}) |
80 | 65, 78, 79 | syl2anc 585 |
. . . . 5
β’ ((π β§ π¦ β π΄) β ((πΎ fLimf (((neiβπ½)β{π¦}) βΎt π΄))βπΉ) = {(πΉβπ¦)}) |
81 | 80 | unieqd 4883 |
. . . 4
β’ ((π β§ π¦ β π΄) β βͺ
((πΎ fLimf
(((neiβπ½)β{π¦}) βΎt π΄))βπΉ) = βͺ {(πΉβπ¦)}) |
82 | | fvex 6859 |
. . . . 5
β’ (πΉβπ¦) β V |
83 | 82 | unisn 4891 |
. . . 4
β’ βͺ {(πΉβπ¦)} = (πΉβπ¦) |
84 | 81, 83 | eqtrdi 2789 |
. . 3
β’ ((π β§ π¦ β π΄) β βͺ
((πΎ fLimf
(((neiβπ½)β{π¦}) βΎt π΄))βπΉ) = (πΉβπ¦)) |
85 | 15, 18, 84 | 3eqtrd 2777 |
. 2
β’ ((π β§ π¦ β π΄) β ((((π½CnExtπΎ)βπΉ) βΎ π΄)βπ¦) = (πΉβπ¦)) |
86 | 12, 13, 85 | eqfnfvd 6989 |
1
β’ (π β (((π½CnExtπΎ)βπΉ) βΎ π΄) = πΉ) |