Step | Hyp | Ref
| Expression |
1 | | cnextfres.j |
. . 3
β’ (π β π½ β Top) |
2 | | cnextfres.k |
. . 3
β’ (π β πΎ β Haus) |
3 | | cnextfres.1 |
. . . . 5
β’ (π β πΉ β ((π½ βΎt π΄) Cn πΎ)) |
4 | | eqid 2733 |
. . . . . 6
β’ βͺ (π½
βΎt π΄) =
βͺ (π½ βΎt π΄) |
5 | | cnextfres.b |
. . . . . 6
β’ π΅ = βͺ
πΎ |
6 | 4, 5 | cnf 22620 |
. . . . 5
β’ (πΉ β ((π½ βΎt π΄) Cn πΎ) β πΉ:βͺ (π½ βΎt π΄)βΆπ΅) |
7 | 3, 6 | syl 17 |
. . . 4
β’ (π β πΉ:βͺ (π½ βΎt π΄)βΆπ΅) |
8 | | cnextfres.a |
. . . . . 6
β’ (π β π΄ β πΆ) |
9 | | cnextfres.c |
. . . . . . 7
β’ πΆ = βͺ
π½ |
10 | 9 | restuni 22536 |
. . . . . 6
β’ ((π½ β Top β§ π΄ β πΆ) β π΄ = βͺ (π½ βΎt π΄)) |
11 | 1, 8, 10 | syl2anc 585 |
. . . . 5
β’ (π β π΄ = βͺ (π½ βΎt π΄)) |
12 | 11 | feq2d 6658 |
. . . 4
β’ (π β (πΉ:π΄βΆπ΅ β πΉ:βͺ (π½ βΎt π΄)βΆπ΅)) |
13 | 7, 12 | mpbird 257 |
. . 3
β’ (π β πΉ:π΄βΆπ΅) |
14 | 9, 5 | cnextfun 23438 |
. . 3
β’ (((π½ β Top β§ πΎ β Haus) β§ (πΉ:π΄βΆπ΅ β§ π΄ β πΆ)) β Fun ((π½CnExtπΎ)βπΉ)) |
15 | 1, 2, 13, 8, 14 | syl22anc 838 |
. 2
β’ (π β Fun ((π½CnExtπΎ)βπΉ)) |
16 | 9 | sscls 22430 |
. . . . . . 7
β’ ((π½ β Top β§ π΄ β πΆ) β π΄ β ((clsβπ½)βπ΄)) |
17 | 1, 8, 16 | syl2anc 585 |
. . . . . 6
β’ (π β π΄ β ((clsβπ½)βπ΄)) |
18 | | cnextfres.x |
. . . . . 6
β’ (π β π β π΄) |
19 | 17, 18 | sseldd 3949 |
. . . . 5
β’ (π β π β ((clsβπ½)βπ΄)) |
20 | 9, 5, 1, 8, 3, 18 | flfcntr 23417 |
. . . . 5
β’ (π β (πΉβπ) β ((πΎ fLimf (((neiβπ½)β{π}) βΎt π΄))βπΉ)) |
21 | | sneq 4600 |
. . . . . . . . . 10
β’ (π₯ = π β {π₯} = {π}) |
22 | 21 | fveq2d 6850 |
. . . . . . . . 9
β’ (π₯ = π β ((neiβπ½)β{π₯}) = ((neiβπ½)β{π})) |
23 | 22 | oveq1d 7376 |
. . . . . . . 8
β’ (π₯ = π β (((neiβπ½)β{π₯}) βΎt π΄) = (((neiβπ½)β{π}) βΎt π΄)) |
24 | 23 | oveq2d 7377 |
. . . . . . 7
β’ (π₯ = π β (πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄)) = (πΎ fLimf (((neiβπ½)β{π}) βΎt π΄))) |
25 | 24 | fveq1d 6848 |
. . . . . 6
β’ (π₯ = π β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ) = ((πΎ fLimf (((neiβπ½)β{π}) βΎt π΄))βπΉ)) |
26 | 25 | opeliunxp2 5798 |
. . . . 5
β’
(β¨π, (πΉβπ)β© β βͺ π₯ β ((clsβπ½)βπ΄)({π₯} Γ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ)) β (π β ((clsβπ½)βπ΄) β§ (πΉβπ) β ((πΎ fLimf (((neiβπ½)β{π}) βΎt π΄))βπΉ))) |
27 | 19, 20, 26 | sylanbrc 584 |
. . . 4
β’ (π β β¨π, (πΉβπ)β© β βͺ π₯ β ((clsβπ½)βπ΄)({π₯} Γ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ))) |
28 | | haustop 22705 |
. . . . . 6
β’ (πΎ β Haus β πΎ β Top) |
29 | 2, 28 | syl 17 |
. . . . 5
β’ (π β πΎ β Top) |
30 | 9, 5 | cnextfval 23436 |
. . . . 5
β’ (((π½ β Top β§ πΎ β Top) β§ (πΉ:π΄βΆπ΅ β§ π΄ β πΆ)) β ((π½CnExtπΎ)βπΉ) = βͺ
π₯ β ((clsβπ½)βπ΄)({π₯} Γ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ))) |
31 | 1, 29, 13, 8, 30 | syl22anc 838 |
. . . 4
β’ (π β ((π½CnExtπΎ)βπΉ) = βͺ
π₯ β ((clsβπ½)βπ΄)({π₯} Γ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ))) |
32 | 27, 31 | eleqtrrd 2837 |
. . 3
β’ (π β β¨π, (πΉβπ)β© β ((π½CnExtπΎ)βπΉ)) |
33 | | df-br 5110 |
. . 3
β’ (π((π½CnExtπΎ)βπΉ)(πΉβπ) β β¨π, (πΉβπ)β© β ((π½CnExtπΎ)βπΉ)) |
34 | 32, 33 | sylibr 233 |
. 2
β’ (π β π((π½CnExtπΎ)βπΉ)(πΉβπ)) |
35 | | funbrfv 6897 |
. 2
β’ (Fun
((π½CnExtπΎ)βπΉ) β (π((π½CnExtπΎ)βπΉ)(πΉβπ) β (((π½CnExtπΎ)βπΉ)βπ) = (πΉβπ))) |
36 | 15, 34, 35 | sylc 65 |
1
β’ (π β (((π½CnExtπΎ)βπΉ)βπ) = (πΉβπ)) |