Step | Hyp | Ref
| Expression |
1 | | cnextf.3 |
. . . 4
β’ (π β π½ β Top) |
2 | | cnextf.4 |
. . . 4
β’ (π β πΎ β Haus) |
3 | | cnextf.5 |
. . . 4
β’ (π β πΉ:π΄βΆπ΅) |
4 | | cnextf.a |
. . . 4
β’ (π β π΄ β πΆ) |
5 | | cnextf.1 |
. . . . 5
β’ πΆ = βͺ
π½ |
6 | | cnextf.2 |
. . . . 5
β’ π΅ = βͺ
πΎ |
7 | 5, 6 | cnextfun 23438 |
. . . 4
β’ (((π½ β Top β§ πΎ β Haus) β§ (πΉ:π΄βΆπ΅ β§ π΄ β πΆ)) β Fun ((π½CnExtπΎ)βπΉ)) |
8 | 1, 2, 3, 4, 7 | syl22anc 838 |
. . 3
β’ (π β Fun ((π½CnExtπΎ)βπΉ)) |
9 | | dfdm3 5847 |
. . . 4
β’ dom
((π½CnExtπΎ)βπΉ) = {π₯ β£ βπ¦β¨π₯, π¦β© β ((π½CnExtπΎ)βπΉ)} |
10 | | simpl 484 |
. . . . . . 7
β’ ((π β§ π₯ β πΆ) β π) |
11 | | cnextf.6 |
. . . . . . . . 9
β’ (π β ((clsβπ½)βπ΄) = πΆ) |
12 | 11 | eleq2d 2820 |
. . . . . . . 8
β’ (π β (π₯ β ((clsβπ½)βπ΄) β π₯ β πΆ)) |
13 | 12 | biimpar 479 |
. . . . . . 7
β’ ((π β§ π₯ β πΆ) β π₯ β ((clsβπ½)βπ΄)) |
14 | | cnextf.7 |
. . . . . . . 8
β’ ((π β§ π₯ β πΆ) β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ) β β
) |
15 | | n0 4310 |
. . . . . . . 8
β’ (((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ) β β
β βπ¦ π¦ β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ)) |
16 | 14, 15 | sylib 217 |
. . . . . . 7
β’ ((π β§ π₯ β πΆ) β βπ¦ π¦ β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ)) |
17 | | haustop 22705 |
. . . . . . . . . . . . . 14
β’ (πΎ β Haus β πΎ β Top) |
18 | 2, 17 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β πΎ β Top) |
19 | 5, 6 | cnextfval 23436 |
. . . . . . . . . . . . 13
β’ (((π½ β Top β§ πΎ β Top) β§ (πΉ:π΄βΆπ΅ β§ π΄ β πΆ)) β ((π½CnExtπΎ)βπΉ) = βͺ
π₯ β ((clsβπ½)βπ΄)({π₯} Γ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ))) |
20 | 1, 18, 3, 4, 19 | syl22anc 838 |
. . . . . . . . . . . 12
β’ (π β ((π½CnExtπΎ)βπΉ) = βͺ
π₯ β ((clsβπ½)βπ΄)({π₯} Γ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ))) |
21 | 20 | eleq2d 2820 |
. . . . . . . . . . 11
β’ (π β (β¨π₯, π¦β© β ((π½CnExtπΎ)βπΉ) β β¨π₯, π¦β© β βͺ π₯ β ((clsβπ½)βπ΄)({π₯} Γ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ)))) |
22 | | opeliunxp 5703 |
. . . . . . . . . . 11
β’
(β¨π₯, π¦β© β βͺ π₯ β ((clsβπ½)βπ΄)({π₯} Γ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ)) β (π₯ β ((clsβπ½)βπ΄) β§ π¦ β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ))) |
23 | 21, 22 | bitrdi 287 |
. . . . . . . . . 10
β’ (π β (β¨π₯, π¦β© β ((π½CnExtπΎ)βπΉ) β (π₯ β ((clsβπ½)βπ΄) β§ π¦ β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ)))) |
24 | 23 | exbidv 1925 |
. . . . . . . . 9
β’ (π β (βπ¦β¨π₯, π¦β© β ((π½CnExtπΎ)βπΉ) β βπ¦(π₯ β ((clsβπ½)βπ΄) β§ π¦ β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ)))) |
25 | | 19.42v 1958 |
. . . . . . . . 9
β’
(βπ¦(π₯ β ((clsβπ½)βπ΄) β§ π¦ β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ)) β (π₯ β ((clsβπ½)βπ΄) β§ βπ¦ π¦ β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ))) |
26 | 24, 25 | bitrdi 287 |
. . . . . . . 8
β’ (π β (βπ¦β¨π₯, π¦β© β ((π½CnExtπΎ)βπΉ) β (π₯ β ((clsβπ½)βπ΄) β§ βπ¦ π¦ β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ)))) |
27 | 26 | biimpar 479 |
. . . . . . 7
β’ ((π β§ (π₯ β ((clsβπ½)βπ΄) β§ βπ¦ π¦ β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ))) β βπ¦β¨π₯, π¦β© β ((π½CnExtπΎ)βπΉ)) |
28 | 10, 13, 16, 27 | syl12anc 836 |
. . . . . 6
β’ ((π β§ π₯ β πΆ) β βπ¦β¨π₯, π¦β© β ((π½CnExtπΎ)βπΉ)) |
29 | 26 | simprbda 500 |
. . . . . . 7
β’ ((π β§ βπ¦β¨π₯, π¦β© β ((π½CnExtπΎ)βπΉ)) β π₯ β ((clsβπ½)βπ΄)) |
30 | 12 | adantr 482 |
. . . . . . 7
β’ ((π β§ βπ¦β¨π₯, π¦β© β ((π½CnExtπΎ)βπΉ)) β (π₯ β ((clsβπ½)βπ΄) β π₯ β πΆ)) |
31 | 29, 30 | mpbid 231 |
. . . . . 6
β’ ((π β§ βπ¦β¨π₯, π¦β© β ((π½CnExtπΎ)βπΉ)) β π₯ β πΆ) |
32 | 28, 31 | impbida 800 |
. . . . 5
β’ (π β (π₯ β πΆ β βπ¦β¨π₯, π¦β© β ((π½CnExtπΎ)βπΉ))) |
33 | 32 | abbi2dv 2868 |
. . . 4
β’ (π β πΆ = {π₯ β£ βπ¦β¨π₯, π¦β© β ((π½CnExtπΎ)βπΉ)}) |
34 | 9, 33 | eqtr4id 2792 |
. . 3
β’ (π β dom ((π½CnExtπΎ)βπΉ) = πΆ) |
35 | | df-fn 6503 |
. . 3
β’ (((π½CnExtπΎ)βπΉ) Fn πΆ β (Fun ((π½CnExtπΎ)βπΉ) β§ dom ((π½CnExtπΎ)βπΉ) = πΆ)) |
36 | 8, 34, 35 | sylanbrc 584 |
. 2
β’ (π β ((π½CnExtπΎ)βπΉ) Fn πΆ) |
37 | 20 | rneqd 5897 |
. . 3
β’ (π β ran ((π½CnExtπΎ)βπΉ) = ran βͺ
π₯ β ((clsβπ½)βπ΄)({π₯} Γ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ))) |
38 | | rniun 6104 |
. . . 4
β’ ran
βͺ π₯ β ((clsβπ½)βπ΄)({π₯} Γ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ)) = βͺ
π₯ β ((clsβπ½)βπ΄)ran ({π₯} Γ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ)) |
39 | | vex 3451 |
. . . . . . . . 9
β’ π₯ β V |
40 | 39 | snnz 4741 |
. . . . . . . 8
β’ {π₯} β β
|
41 | | rnxp 6126 |
. . . . . . . 8
β’ ({π₯} β β
β ran
({π₯} Γ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ)) = ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ)) |
42 | 40, 41 | ax-mp 5 |
. . . . . . 7
β’ ran
({π₯} Γ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ)) = ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ) |
43 | 12 | biimpa 478 |
. . . . . . . 8
β’ ((π β§ π₯ β ((clsβπ½)βπ΄)) β π₯ β πΆ) |
44 | 6 | toptopon 22289 |
. . . . . . . . . . 11
β’ (πΎ β Top β πΎ β (TopOnβπ΅)) |
45 | 18, 44 | sylib 217 |
. . . . . . . . . 10
β’ (π β πΎ β (TopOnβπ΅)) |
46 | 45 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π₯ β πΆ) β πΎ β (TopOnβπ΅)) |
47 | 5 | toptopon 22289 |
. . . . . . . . . . . 12
β’ (π½ β Top β π½ β (TopOnβπΆ)) |
48 | 1, 47 | sylib 217 |
. . . . . . . . . . 11
β’ (π β π½ β (TopOnβπΆ)) |
49 | 48 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π₯ β πΆ) β π½ β (TopOnβπΆ)) |
50 | 4 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π₯ β πΆ) β π΄ β πΆ) |
51 | | simpr 486 |
. . . . . . . . . 10
β’ ((π β§ π₯ β πΆ) β π₯ β πΆ) |
52 | | trnei 23266 |
. . . . . . . . . . 11
β’ ((π½ β (TopOnβπΆ) β§ π΄ β πΆ β§ π₯ β πΆ) β (π₯ β ((clsβπ½)βπ΄) β (((neiβπ½)β{π₯}) βΎt π΄) β (Filβπ΄))) |
53 | 52 | biimpa 478 |
. . . . . . . . . 10
β’ (((π½ β (TopOnβπΆ) β§ π΄ β πΆ β§ π₯ β πΆ) β§ π₯ β ((clsβπ½)βπ΄)) β (((neiβπ½)β{π₯}) βΎt π΄) β (Filβπ΄)) |
54 | 49, 50, 51, 13, 53 | syl31anc 1374 |
. . . . . . . . 9
β’ ((π β§ π₯ β πΆ) β (((neiβπ½)β{π₯}) βΎt π΄) β (Filβπ΄)) |
55 | 3 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π₯ β πΆ) β πΉ:π΄βΆπ΅) |
56 | | flfelbas 23368 |
. . . . . . . . . . 11
β’ (((πΎ β (TopOnβπ΅) β§ (((neiβπ½)β{π₯}) βΎt π΄) β (Filβπ΄) β§ πΉ:π΄βΆπ΅) β§ π¦ β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ)) β π¦ β π΅) |
57 | 56 | ex 414 |
. . . . . . . . . 10
β’ ((πΎ β (TopOnβπ΅) β§ (((neiβπ½)β{π₯}) βΎt π΄) β (Filβπ΄) β§ πΉ:π΄βΆπ΅) β (π¦ β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ) β π¦ β π΅)) |
58 | 57 | ssrdv 3954 |
. . . . . . . . 9
β’ ((πΎ β (TopOnβπ΅) β§ (((neiβπ½)β{π₯}) βΎt π΄) β (Filβπ΄) β§ πΉ:π΄βΆπ΅) β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ) β π΅) |
59 | 46, 54, 55, 58 | syl3anc 1372 |
. . . . . . . 8
β’ ((π β§ π₯ β πΆ) β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ) β π΅) |
60 | 43, 59 | syldan 592 |
. . . . . . 7
β’ ((π β§ π₯ β ((clsβπ½)βπ΄)) β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ) β π΅) |
61 | 42, 60 | eqsstrid 3996 |
. . . . . 6
β’ ((π β§ π₯ β ((clsβπ½)βπ΄)) β ran ({π₯} Γ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ)) β π΅) |
62 | 61 | ralrimiva 3140 |
. . . . 5
β’ (π β βπ₯ β ((clsβπ½)βπ΄)ran ({π₯} Γ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ)) β π΅) |
63 | | iunss 5009 |
. . . . 5
β’ (βͺ π₯ β ((clsβπ½)βπ΄)ran ({π₯} Γ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ)) β π΅ β βπ₯ β ((clsβπ½)βπ΄)ran ({π₯} Γ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ)) β π΅) |
64 | 62, 63 | sylibr 233 |
. . . 4
β’ (π β βͺ π₯ β ((clsβπ½)βπ΄)ran ({π₯} Γ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ)) β π΅) |
65 | 38, 64 | eqsstrid 3996 |
. . 3
β’ (π β ran βͺ π₯ β ((clsβπ½)βπ΄)({π₯} Γ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ)) β π΅) |
66 | 37, 65 | eqsstrd 3986 |
. 2
β’ (π β ran ((π½CnExtπΎ)βπΉ) β π΅) |
67 | | df-f 6504 |
. 2
β’ (((π½CnExtπΎ)βπΉ):πΆβΆπ΅ β (((π½CnExtπΎ)βπΉ) Fn πΆ β§ ran ((π½CnExtπΎ)βπΉ) β π΅)) |
68 | 36, 66, 67 | sylanbrc 584 |
1
β’ (π β ((π½CnExtπΎ)βπΉ):πΆβΆπ΅) |