Step | Hyp | Ref
| Expression |
1 | | cnextf.3 |
. . . 4
β’ (π β π½ β Top) |
2 | 1 | adantr 482 |
. . 3
β’ ((π β§ π β πΆ) β π½ β Top) |
3 | | cnextf.4 |
. . . 4
β’ (π β πΎ β Haus) |
4 | 3 | adantr 482 |
. . 3
β’ ((π β§ π β πΆ) β πΎ β Haus) |
5 | | cnextf.5 |
. . . 4
β’ (π β πΉ:π΄βΆπ΅) |
6 | 5 | adantr 482 |
. . 3
β’ ((π β§ π β πΆ) β πΉ:π΄βΆπ΅) |
7 | | cnextf.a |
. . . 4
β’ (π β π΄ β πΆ) |
8 | 7 | adantr 482 |
. . 3
β’ ((π β§ π β πΆ) β π΄ β πΆ) |
9 | | cnextf.1 |
. . . 4
β’ πΆ = βͺ
π½ |
10 | | cnextf.2 |
. . . 4
β’ π΅ = βͺ
πΎ |
11 | 9, 10 | cnextfun 23438 |
. . 3
β’ (((π½ β Top β§ πΎ β Haus) β§ (πΉ:π΄βΆπ΅ β§ π΄ β πΆ)) β Fun ((π½CnExtπΎ)βπΉ)) |
12 | 2, 4, 6, 8, 11 | syl22anc 838 |
. 2
β’ ((π β§ π β πΆ) β Fun ((π½CnExtπΎ)βπΉ)) |
13 | | cnextf.6 |
. . . . . 6
β’ (π β ((clsβπ½)βπ΄) = πΆ) |
14 | 13 | eleq2d 2820 |
. . . . 5
β’ (π β (π β ((clsβπ½)βπ΄) β π β πΆ)) |
15 | 14 | biimpar 479 |
. . . 4
β’ ((π β§ π β πΆ) β π β ((clsβπ½)βπ΄)) |
16 | | fvex 6859 |
. . . . . . 7
β’ ((πΎ fLimf (((neiβπ½)β{π}) βΎt π΄))βπΉ) β V |
17 | 16 | uniex 7682 |
. . . . . 6
β’ βͺ ((πΎ
fLimf (((neiβπ½)β{π}) βΎt π΄))βπΉ) β V |
18 | 17 | snid 4626 |
. . . . 5
β’ βͺ ((πΎ
fLimf (((neiβπ½)β{π}) βΎt π΄))βπΉ) β {βͺ
((πΎ fLimf
(((neiβπ½)β{π}) βΎt π΄))βπΉ)} |
19 | | sneq 4600 |
. . . . . . . . . . . . . 14
β’ (π₯ = π β {π₯} = {π}) |
20 | 19 | fveq2d 6850 |
. . . . . . . . . . . . 13
β’ (π₯ = π β ((neiβπ½)β{π₯}) = ((neiβπ½)β{π})) |
21 | 20 | oveq1d 7376 |
. . . . . . . . . . . 12
β’ (π₯ = π β (((neiβπ½)β{π₯}) βΎt π΄) = (((neiβπ½)β{π}) βΎt π΄)) |
22 | 21 | oveq2d 7377 |
. . . . . . . . . . 11
β’ (π₯ = π β (πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄)) = (πΎ fLimf (((neiβπ½)β{π}) βΎt π΄))) |
23 | 22 | fveq1d 6848 |
. . . . . . . . . 10
β’ (π₯ = π β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ) = ((πΎ fLimf (((neiβπ½)β{π}) βΎt π΄))βπΉ)) |
24 | 23 | breq1d 5119 |
. . . . . . . . 9
β’ (π₯ = π β (((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ) β 1o β ((πΎ fLimf (((neiβπ½)β{π}) βΎt π΄))βπΉ) β 1o)) |
25 | 24 | imbi2d 341 |
. . . . . . . 8
β’ (π₯ = π β ((π β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ) β 1o) β (π β ((πΎ fLimf (((neiβπ½)β{π}) βΎt π΄))βπΉ) β 1o))) |
26 | 3 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π₯ β πΆ) β πΎ β Haus) |
27 | 1 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β πΆ) β π½ β Top) |
28 | 9 | toptopon 22289 |
. . . . . . . . . . . 12
β’ (π½ β Top β π½ β (TopOnβπΆ)) |
29 | 27, 28 | sylib 217 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β πΆ) β π½ β (TopOnβπΆ)) |
30 | 7 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β πΆ) β π΄ β πΆ) |
31 | | simpr 486 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β πΆ) β π₯ β πΆ) |
32 | 13 | eleq2d 2820 |
. . . . . . . . . . . 12
β’ (π β (π₯ β ((clsβπ½)βπ΄) β π₯ β πΆ)) |
33 | 32 | biimpar 479 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β πΆ) β π₯ β ((clsβπ½)βπ΄)) |
34 | | trnei 23266 |
. . . . . . . . . . . 12
β’ ((π½ β (TopOnβπΆ) β§ π΄ β πΆ β§ π₯ β πΆ) β (π₯ β ((clsβπ½)βπ΄) β (((neiβπ½)β{π₯}) βΎt π΄) β (Filβπ΄))) |
35 | 34 | biimpa 478 |
. . . . . . . . . . 11
β’ (((π½ β (TopOnβπΆ) β§ π΄ β πΆ β§ π₯ β πΆ) β§ π₯ β ((clsβπ½)βπ΄)) β (((neiβπ½)β{π₯}) βΎt π΄) β (Filβπ΄)) |
36 | 29, 30, 31, 33, 35 | syl31anc 1374 |
. . . . . . . . . 10
β’ ((π β§ π₯ β πΆ) β (((neiβπ½)β{π₯}) βΎt π΄) β (Filβπ΄)) |
37 | 5 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π₯ β πΆ) β πΉ:π΄βΆπ΅) |
38 | | cnextf.7 |
. . . . . . . . . 10
β’ ((π β§ π₯ β πΆ) β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ) β β
) |
39 | 10 | hausflf2 23372 |
. . . . . . . . . 10
β’ (((πΎ β Haus β§
(((neiβπ½)β{π₯}) βΎt π΄) β (Filβπ΄) β§ πΉ:π΄βΆπ΅) β§ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ) β β
) β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ) β 1o) |
40 | 26, 36, 37, 38, 39 | syl31anc 1374 |
. . . . . . . . 9
β’ ((π β§ π₯ β πΆ) β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ) β 1o) |
41 | 40 | expcom 415 |
. . . . . . . 8
β’ (π₯ β πΆ β (π β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ) β 1o)) |
42 | 25, 41 | vtoclga 3536 |
. . . . . . 7
β’ (π β πΆ β (π β ((πΎ fLimf (((neiβπ½)β{π}) βΎt π΄))βπΉ) β 1o)) |
43 | 42 | impcom 409 |
. . . . . 6
β’ ((π β§ π β πΆ) β ((πΎ fLimf (((neiβπ½)β{π}) βΎt π΄))βπΉ) β 1o) |
44 | | en1b 8973 |
. . . . . 6
β’ (((πΎ fLimf (((neiβπ½)β{π}) βΎt π΄))βπΉ) β 1o β ((πΎ fLimf (((neiβπ½)β{π}) βΎt π΄))βπΉ) = {βͺ ((πΎ fLimf (((neiβπ½)β{π}) βΎt π΄))βπΉ)}) |
45 | 43, 44 | sylib 217 |
. . . . 5
β’ ((π β§ π β πΆ) β ((πΎ fLimf (((neiβπ½)β{π}) βΎt π΄))βπΉ) = {βͺ ((πΎ fLimf (((neiβπ½)β{π}) βΎt π΄))βπΉ)}) |
46 | 18, 45 | eleqtrrid 2841 |
. . . 4
β’ ((π β§ π β πΆ) β βͺ
((πΎ fLimf
(((neiβπ½)β{π}) βΎt π΄))βπΉ) β ((πΎ fLimf (((neiβπ½)β{π}) βΎt π΄))βπΉ)) |
47 | | nfiu1 4992 |
. . . . . . . 8
β’
β²π₯βͺ π₯ β ((clsβπ½)βπ΄)({π₯} Γ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ)) |
48 | 47 | nfel2 2922 |
. . . . . . 7
β’
β²π₯β¨π, βͺ
((πΎ fLimf
(((neiβπ½)β{π}) βΎt π΄))βπΉ)β© β βͺ π₯ β ((clsβπ½)βπ΄)({π₯} Γ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ)) |
49 | | nfv 1918 |
. . . . . . 7
β’
β²π₯(π β ((clsβπ½)βπ΄) β§ βͺ ((πΎ fLimf (((neiβπ½)β{π}) βΎt π΄))βπΉ) β ((πΎ fLimf (((neiβπ½)β{π}) βΎt π΄))βπΉ)) |
50 | 48, 49 | nfbi 1907 |
. . . . . 6
β’
β²π₯(β¨π, βͺ
((πΎ fLimf
(((neiβπ½)β{π}) βΎt π΄))βπΉ)β© β βͺ π₯ β ((clsβπ½)βπ΄)({π₯} Γ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ)) β (π β ((clsβπ½)βπ΄) β§ βͺ ((πΎ fLimf (((neiβπ½)β{π}) βΎt π΄))βπΉ) β ((πΎ fLimf (((neiβπ½)β{π}) βΎt π΄))βπΉ))) |
51 | | opeq1 4834 |
. . . . . . . 8
β’ (π₯ = π β β¨π₯, βͺ ((πΎ fLimf (((neiβπ½)β{π}) βΎt π΄))βπΉ)β© = β¨π, βͺ ((πΎ fLimf (((neiβπ½)β{π}) βΎt π΄))βπΉ)β©) |
52 | 51 | eleq1d 2819 |
. . . . . . 7
β’ (π₯ = π β (β¨π₯, βͺ ((πΎ fLimf (((neiβπ½)β{π}) βΎt π΄))βπΉ)β© β βͺ π₯ β ((clsβπ½)βπ΄)({π₯} Γ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ)) β β¨π, βͺ ((πΎ fLimf (((neiβπ½)β{π}) βΎt π΄))βπΉ)β© β βͺ π₯ β ((clsβπ½)βπ΄)({π₯} Γ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ)))) |
53 | | eleq1 2822 |
. . . . . . . 8
β’ (π₯ = π β (π₯ β ((clsβπ½)βπ΄) β π β ((clsβπ½)βπ΄))) |
54 | 23 | eleq2d 2820 |
. . . . . . . 8
β’ (π₯ = π β (βͺ
((πΎ fLimf
(((neiβπ½)β{π}) βΎt π΄))βπΉ) β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ) β βͺ
((πΎ fLimf
(((neiβπ½)β{π}) βΎt π΄))βπΉ) β ((πΎ fLimf (((neiβπ½)β{π}) βΎt π΄))βπΉ))) |
55 | 53, 54 | anbi12d 632 |
. . . . . . 7
β’ (π₯ = π β ((π₯ β ((clsβπ½)βπ΄) β§ βͺ ((πΎ fLimf (((neiβπ½)β{π}) βΎt π΄))βπΉ) β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ)) β (π β ((clsβπ½)βπ΄) β§ βͺ ((πΎ fLimf (((neiβπ½)β{π}) βΎt π΄))βπΉ) β ((πΎ fLimf (((neiβπ½)β{π}) βΎt π΄))βπΉ)))) |
56 | 52, 55 | bibi12d 346 |
. . . . . 6
β’ (π₯ = π β ((β¨π₯, βͺ ((πΎ fLimf (((neiβπ½)β{π}) βΎt π΄))βπΉ)β© β βͺ π₯ β ((clsβπ½)βπ΄)({π₯} Γ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ)) β (π₯ β ((clsβπ½)βπ΄) β§ βͺ ((πΎ fLimf (((neiβπ½)β{π}) βΎt π΄))βπΉ) β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ))) β (β¨π, βͺ ((πΎ fLimf (((neiβπ½)β{π}) βΎt π΄))βπΉ)β© β βͺ π₯ β ((clsβπ½)βπ΄)({π₯} Γ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ)) β (π β ((clsβπ½)βπ΄) β§ βͺ ((πΎ fLimf (((neiβπ½)β{π}) βΎt π΄))βπΉ) β ((πΎ fLimf (((neiβπ½)β{π}) βΎt π΄))βπΉ))))) |
57 | | opeliunxp 5703 |
. . . . . 6
β’
(β¨π₯, βͺ ((πΎ
fLimf (((neiβπ½)β{π}) βΎt π΄))βπΉ)β© β βͺ π₯ β ((clsβπ½)βπ΄)({π₯} Γ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ)) β (π₯ β ((clsβπ½)βπ΄) β§ βͺ ((πΎ fLimf (((neiβπ½)β{π}) βΎt π΄))βπΉ) β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ))) |
58 | 50, 56, 57 | vtoclg1f 3526 |
. . . . 5
β’ (π β πΆ β (β¨π, βͺ ((πΎ fLimf (((neiβπ½)β{π}) βΎt π΄))βπΉ)β© β βͺ π₯ β ((clsβπ½)βπ΄)({π₯} Γ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ)) β (π β ((clsβπ½)βπ΄) β§ βͺ ((πΎ fLimf (((neiβπ½)β{π}) βΎt π΄))βπΉ) β ((πΎ fLimf (((neiβπ½)β{π}) βΎt π΄))βπΉ)))) |
59 | 58 | adantl 483 |
. . . 4
β’ ((π β§ π β πΆ) β (β¨π, βͺ ((πΎ fLimf (((neiβπ½)β{π}) βΎt π΄))βπΉ)β© β βͺ π₯ β ((clsβπ½)βπ΄)({π₯} Γ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ)) β (π β ((clsβπ½)βπ΄) β§ βͺ ((πΎ fLimf (((neiβπ½)β{π}) βΎt π΄))βπΉ) β ((πΎ fLimf (((neiβπ½)β{π}) βΎt π΄))βπΉ)))) |
60 | 15, 46, 59 | mpbir2and 712 |
. . 3
β’ ((π β§ π β πΆ) β β¨π, βͺ ((πΎ fLimf (((neiβπ½)β{π}) βΎt π΄))βπΉ)β© β βͺ π₯ β ((clsβπ½)βπ΄)({π₯} Γ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ))) |
61 | | df-br 5110 |
. . . 4
β’ (π((π½CnExtπΎ)βπΉ)βͺ ((πΎ fLimf (((neiβπ½)β{π}) βΎt π΄))βπΉ) β β¨π, βͺ ((πΎ fLimf (((neiβπ½)β{π}) βΎt π΄))βπΉ)β© β ((π½CnExtπΎ)βπΉ)) |
62 | | haustop 22705 |
. . . . . . . 8
β’ (πΎ β Haus β πΎ β Top) |
63 | 3, 62 | syl 17 |
. . . . . . 7
β’ (π β πΎ β Top) |
64 | 63 | adantr 482 |
. . . . . 6
β’ ((π β§ π β πΆ) β πΎ β Top) |
65 | 9, 10 | cnextfval 23436 |
. . . . . 6
β’ (((π½ β Top β§ πΎ β Top) β§ (πΉ:π΄βΆπ΅ β§ π΄ β πΆ)) β ((π½CnExtπΎ)βπΉ) = βͺ
π₯ β ((clsβπ½)βπ΄)({π₯} Γ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ))) |
66 | 2, 64, 6, 8, 65 | syl22anc 838 |
. . . . 5
β’ ((π β§ π β πΆ) β ((π½CnExtπΎ)βπΉ) = βͺ
π₯ β ((clsβπ½)βπ΄)({π₯} Γ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ))) |
67 | 66 | eleq2d 2820 |
. . . 4
β’ ((π β§ π β πΆ) β (β¨π, βͺ ((πΎ fLimf (((neiβπ½)β{π}) βΎt π΄))βπΉ)β© β ((π½CnExtπΎ)βπΉ) β β¨π, βͺ ((πΎ fLimf (((neiβπ½)β{π}) βΎt π΄))βπΉ)β© β βͺ π₯ β ((clsβπ½)βπ΄)({π₯} Γ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ)))) |
68 | 61, 67 | bitrid 283 |
. . 3
β’ ((π β§ π β πΆ) β (π((π½CnExtπΎ)βπΉ)βͺ ((πΎ fLimf (((neiβπ½)β{π}) βΎt π΄))βπΉ) β β¨π, βͺ ((πΎ fLimf (((neiβπ½)β{π}) βΎt π΄))βπΉ)β© β βͺ π₯ β ((clsβπ½)βπ΄)({π₯} Γ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ)))) |
69 | 60, 68 | mpbird 257 |
. 2
β’ ((π β§ π β πΆ) β π((π½CnExtπΎ)βπΉ)βͺ ((πΎ fLimf (((neiβπ½)β{π}) βΎt π΄))βπΉ)) |
70 | | funbrfv 6897 |
. 2
β’ (Fun
((π½CnExtπΎ)βπΉ) β (π((π½CnExtπΎ)βπΉ)βͺ ((πΎ fLimf (((neiβπ½)β{π}) βΎt π΄))βπΉ) β (((π½CnExtπΎ)βπΉ)βπ) = βͺ ((πΎ fLimf (((neiβπ½)β{π}) βΎt π΄))βπΉ))) |
71 | 12, 69, 70 | sylc 65 |
1
β’ ((π β§ π β πΆ) β (((π½CnExtπΎ)βπΉ)βπ) = βͺ ((πΎ fLimf (((neiβπ½)β{π}) βΎt π΄))βπΉ)) |