Step | Hyp | Ref
| Expression |
1 | | haustop 22705 |
. . 3
β’ (πΎ β Haus β πΎ β Top) |
2 | | cnextfrel.1 |
. . . 4
β’ πΆ = βͺ
π½ |
3 | | cnextfrel.2 |
. . . 4
β’ π΅ = βͺ
πΎ |
4 | 2, 3 | cnextrel 23437 |
. . 3
β’ (((π½ β Top β§ πΎ β Top) β§ (πΉ:π΄βΆπ΅ β§ π΄ β πΆ)) β Rel ((π½CnExtπΎ)βπΉ)) |
5 | 1, 4 | sylanl2 680 |
. 2
β’ (((π½ β Top β§ πΎ β Haus) β§ (πΉ:π΄βΆπ΅ β§ π΄ β πΆ)) β Rel ((π½CnExtπΎ)βπΉ)) |
6 | | simpllr 775 |
. . . . . . 7
β’ ((((π½ β Top β§ πΎ β Haus) β§ (πΉ:π΄βΆπ΅ β§ π΄ β πΆ)) β§ π₯ β ((clsβπ½)βπ΄)) β πΎ β Haus) |
7 | 2 | toptopon 22289 |
. . . . . . . . . 10
β’ (π½ β Top β π½ β (TopOnβπΆ)) |
8 | 7 | biimpi 215 |
. . . . . . . . 9
β’ (π½ β Top β π½ β (TopOnβπΆ)) |
9 | 8 | ad3antrrr 729 |
. . . . . . . 8
β’ ((((π½ β Top β§ πΎ β Haus) β§ (πΉ:π΄βΆπ΅ β§ π΄ β πΆ)) β§ π₯ β ((clsβπ½)βπ΄)) β π½ β (TopOnβπΆ)) |
10 | | simplrr 777 |
. . . . . . . 8
β’ ((((π½ β Top β§ πΎ β Haus) β§ (πΉ:π΄βΆπ΅ β§ π΄ β πΆ)) β§ π₯ β ((clsβπ½)βπ΄)) β π΄ β πΆ) |
11 | 9, 7 | sylibr 233 |
. . . . . . . . . 10
β’ ((((π½ β Top β§ πΎ β Haus) β§ (πΉ:π΄βΆπ΅ β§ π΄ β πΆ)) β§ π₯ β ((clsβπ½)βπ΄)) β π½ β Top) |
12 | 2 | clsss3 22433 |
. . . . . . . . . 10
β’ ((π½ β Top β§ π΄ β πΆ) β ((clsβπ½)βπ΄) β πΆ) |
13 | 11, 10, 12 | syl2anc 585 |
. . . . . . . . 9
β’ ((((π½ β Top β§ πΎ β Haus) β§ (πΉ:π΄βΆπ΅ β§ π΄ β πΆ)) β§ π₯ β ((clsβπ½)βπ΄)) β ((clsβπ½)βπ΄) β πΆ) |
14 | | simpr 486 |
. . . . . . . . 9
β’ ((((π½ β Top β§ πΎ β Haus) β§ (πΉ:π΄βΆπ΅ β§ π΄ β πΆ)) β§ π₯ β ((clsβπ½)βπ΄)) β π₯ β ((clsβπ½)βπ΄)) |
15 | 13, 14 | sseldd 3949 |
. . . . . . . 8
β’ ((((π½ β Top β§ πΎ β Haus) β§ (πΉ:π΄βΆπ΅ β§ π΄ β πΆ)) β§ π₯ β ((clsβπ½)βπ΄)) β π₯ β πΆ) |
16 | | trnei 23266 |
. . . . . . . . 9
β’ ((π½ β (TopOnβπΆ) β§ π΄ β πΆ β§ π₯ β πΆ) β (π₯ β ((clsβπ½)βπ΄) β (((neiβπ½)β{π₯}) βΎt π΄) β (Filβπ΄))) |
17 | 16 | biimpa 478 |
. . . . . . . 8
β’ (((π½ β (TopOnβπΆ) β§ π΄ β πΆ β§ π₯ β πΆ) β§ π₯ β ((clsβπ½)βπ΄)) β (((neiβπ½)β{π₯}) βΎt π΄) β (Filβπ΄)) |
18 | 9, 10, 15, 14, 17 | syl31anc 1374 |
. . . . . . 7
β’ ((((π½ β Top β§ πΎ β Haus) β§ (πΉ:π΄βΆπ΅ β§ π΄ β πΆ)) β§ π₯ β ((clsβπ½)βπ΄)) β (((neiβπ½)β{π₯}) βΎt π΄) β (Filβπ΄)) |
19 | | simplrl 776 |
. . . . . . 7
β’ ((((π½ β Top β§ πΎ β Haus) β§ (πΉ:π΄βΆπ΅ β§ π΄ β πΆ)) β§ π₯ β ((clsβπ½)βπ΄)) β πΉ:π΄βΆπ΅) |
20 | 3 | hausflf 23371 |
. . . . . . 7
β’ ((πΎ β Haus β§
(((neiβπ½)β{π₯}) βΎt π΄) β (Filβπ΄) β§ πΉ:π΄βΆπ΅) β β*π¦ π¦ β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ)) |
21 | 6, 18, 19, 20 | syl3anc 1372 |
. . . . . 6
β’ ((((π½ β Top β§ πΎ β Haus) β§ (πΉ:π΄βΆπ΅ β§ π΄ β πΆ)) β§ π₯ β ((clsβπ½)βπ΄)) β β*π¦ π¦ β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ)) |
22 | 21 | ex 414 |
. . . . 5
β’ (((π½ β Top β§ πΎ β Haus) β§ (πΉ:π΄βΆπ΅ β§ π΄ β πΆ)) β (π₯ β ((clsβπ½)βπ΄) β β*π¦ π¦ β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ))) |
23 | 22 | alrimiv 1931 |
. . . 4
β’ (((π½ β Top β§ πΎ β Haus) β§ (πΉ:π΄βΆπ΅ β§ π΄ β πΆ)) β βπ₯(π₯ β ((clsβπ½)βπ΄) β β*π¦ π¦ β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ))) |
24 | | moanimv 2616 |
. . . . 5
β’
(β*π¦(π₯ β ((clsβπ½)βπ΄) β§ π¦ β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ)) β (π₯ β ((clsβπ½)βπ΄) β β*π¦ π¦ β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ))) |
25 | 24 | albii 1822 |
. . . 4
β’
(βπ₯β*π¦(π₯ β ((clsβπ½)βπ΄) β§ π¦ β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ)) β βπ₯(π₯ β ((clsβπ½)βπ΄) β β*π¦ π¦ β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ))) |
26 | 23, 25 | sylibr 233 |
. . 3
β’ (((π½ β Top β§ πΎ β Haus) β§ (πΉ:π΄βΆπ΅ β§ π΄ β πΆ)) β βπ₯β*π¦(π₯ β ((clsβπ½)βπ΄) β§ π¦ β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ))) |
27 | | df-br 5110 |
. . . . . . 7
β’ (π₯((π½CnExtπΎ)βπΉ)π¦ β β¨π₯, π¦β© β ((π½CnExtπΎ)βπΉ)) |
28 | 27 | a1i 11 |
. . . . . 6
β’ (((π½ β Top β§ πΎ β Haus) β§ (πΉ:π΄βΆπ΅ β§ π΄ β πΆ)) β (π₯((π½CnExtπΎ)βπΉ)π¦ β β¨π₯, π¦β© β ((π½CnExtπΎ)βπΉ))) |
29 | 2, 3 | cnextfval 23436 |
. . . . . . . 8
β’ (((π½ β Top β§ πΎ β Top) β§ (πΉ:π΄βΆπ΅ β§ π΄ β πΆ)) β ((π½CnExtπΎ)βπΉ) = βͺ
π₯ β ((clsβπ½)βπ΄)({π₯} Γ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ))) |
30 | 1, 29 | sylanl2 680 |
. . . . . . 7
β’ (((π½ β Top β§ πΎ β Haus) β§ (πΉ:π΄βΆπ΅ β§ π΄ β πΆ)) β ((π½CnExtπΎ)βπΉ) = βͺ
π₯ β ((clsβπ½)βπ΄)({π₯} Γ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ))) |
31 | 30 | eleq2d 2820 |
. . . . . 6
β’ (((π½ β Top β§ πΎ β Haus) β§ (πΉ:π΄βΆπ΅ β§ π΄ β πΆ)) β (β¨π₯, π¦β© β ((π½CnExtπΎ)βπΉ) β β¨π₯, π¦β© β βͺ π₯ β ((clsβπ½)βπ΄)({π₯} Γ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ)))) |
32 | | opeliunxp 5703 |
. . . . . . 7
β’
(β¨π₯, π¦β© β βͺ π₯ β ((clsβπ½)βπ΄)({π₯} Γ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ)) β (π₯ β ((clsβπ½)βπ΄) β§ π¦ β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ))) |
33 | 32 | a1i 11 |
. . . . . 6
β’ (((π½ β Top β§ πΎ β Haus) β§ (πΉ:π΄βΆπ΅ β§ π΄ β πΆ)) β (β¨π₯, π¦β© β βͺ π₯ β ((clsβπ½)βπ΄)({π₯} Γ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ)) β (π₯ β ((clsβπ½)βπ΄) β§ π¦ β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ)))) |
34 | 28, 31, 33 | 3bitrd 305 |
. . . . 5
β’ (((π½ β Top β§ πΎ β Haus) β§ (πΉ:π΄βΆπ΅ β§ π΄ β πΆ)) β (π₯((π½CnExtπΎ)βπΉ)π¦ β (π₯ β ((clsβπ½)βπ΄) β§ π¦ β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ)))) |
35 | 34 | mobidv 2544 |
. . . 4
β’ (((π½ β Top β§ πΎ β Haus) β§ (πΉ:π΄βΆπ΅ β§ π΄ β πΆ)) β (β*π¦ π₯((π½CnExtπΎ)βπΉ)π¦ β β*π¦(π₯ β ((clsβπ½)βπ΄) β§ π¦ β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ)))) |
36 | 35 | albidv 1924 |
. . 3
β’ (((π½ β Top β§ πΎ β Haus) β§ (πΉ:π΄βΆπ΅ β§ π΄ β πΆ)) β (βπ₯β*π¦ π₯((π½CnExtπΎ)βπΉ)π¦ β βπ₯β*π¦(π₯ β ((clsβπ½)βπ΄) β§ π¦ β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ)))) |
37 | 26, 36 | mpbird 257 |
. 2
β’ (((π½ β Top β§ πΎ β Haus) β§ (πΉ:π΄βΆπ΅ β§ π΄ β πΆ)) β βπ₯β*π¦ π₯((π½CnExtπΎ)βπΉ)π¦) |
38 | | dffun6 6513 |
. 2
β’ (Fun
((π½CnExtπΎ)βπΉ) β (Rel ((π½CnExtπΎ)βπΉ) β§ βπ₯β*π¦ π₯((π½CnExtπΎ)βπΉ)π¦)) |
39 | 5, 37, 38 | sylanbrc 584 |
1
β’ (((π½ β Top β§ πΎ β Haus) β§ (πΉ:π΄βΆπ΅ β§ π΄ β πΆ)) β Fun ((π½CnExtπΎ)βπΉ)) |