Step | Hyp | Ref
| Expression |
1 | | haustop 23055 |
. . 3
β’ (πΎ β Haus β πΎ β Top) |
2 | | cnextfrel.1 |
. . . 4
β’ πΆ = βͺ
π½ |
3 | | cnextfrel.2 |
. . . 4
β’ π΅ = βͺ
πΎ |
4 | 2, 3 | cnextrel 23787 |
. . 3
β’ (((π½ β Top β§ πΎ β Top) β§ (πΉ:π΄βΆπ΅ β§ π΄ β πΆ)) β Rel ((π½CnExtπΎ)βπΉ)) |
5 | 1, 4 | sylanl2 677 |
. 2
β’ (((π½ β Top β§ πΎ β Haus) β§ (πΉ:π΄βΆπ΅ β§ π΄ β πΆ)) β Rel ((π½CnExtπΎ)βπΉ)) |
6 | | simpllr 772 |
. . . . . . 7
β’ ((((π½ β Top β§ πΎ β Haus) β§ (πΉ:π΄βΆπ΅ β§ π΄ β πΆ)) β§ π₯ β ((clsβπ½)βπ΄)) β πΎ β Haus) |
7 | 2 | toptopon 22639 |
. . . . . . . . . 10
β’ (π½ β Top β π½ β (TopOnβπΆ)) |
8 | 7 | biimpi 215 |
. . . . . . . . 9
β’ (π½ β Top β π½ β (TopOnβπΆ)) |
9 | 8 | ad3antrrr 726 |
. . . . . . . 8
β’ ((((π½ β Top β§ πΎ β Haus) β§ (πΉ:π΄βΆπ΅ β§ π΄ β πΆ)) β§ π₯ β ((clsβπ½)βπ΄)) β π½ β (TopOnβπΆ)) |
10 | | simplrr 774 |
. . . . . . . 8
β’ ((((π½ β Top β§ πΎ β Haus) β§ (πΉ:π΄βΆπ΅ β§ π΄ β πΆ)) β§ π₯ β ((clsβπ½)βπ΄)) β π΄ β πΆ) |
11 | 9, 7 | sylibr 233 |
. . . . . . . . . 10
β’ ((((π½ β Top β§ πΎ β Haus) β§ (πΉ:π΄βΆπ΅ β§ π΄ β πΆ)) β§ π₯ β ((clsβπ½)βπ΄)) β π½ β Top) |
12 | 2 | clsss3 22783 |
. . . . . . . . . 10
β’ ((π½ β Top β§ π΄ β πΆ) β ((clsβπ½)βπ΄) β πΆ) |
13 | 11, 10, 12 | syl2anc 582 |
. . . . . . . . 9
β’ ((((π½ β Top β§ πΎ β Haus) β§ (πΉ:π΄βΆπ΅ β§ π΄ β πΆ)) β§ π₯ β ((clsβπ½)βπ΄)) β ((clsβπ½)βπ΄) β πΆ) |
14 | | simpr 483 |
. . . . . . . . 9
β’ ((((π½ β Top β§ πΎ β Haus) β§ (πΉ:π΄βΆπ΅ β§ π΄ β πΆ)) β§ π₯ β ((clsβπ½)βπ΄)) β π₯ β ((clsβπ½)βπ΄)) |
15 | 13, 14 | sseldd 3982 |
. . . . . . . 8
β’ ((((π½ β Top β§ πΎ β Haus) β§ (πΉ:π΄βΆπ΅ β§ π΄ β πΆ)) β§ π₯ β ((clsβπ½)βπ΄)) β π₯ β πΆ) |
16 | | trnei 23616 |
. . . . . . . . 9
β’ ((π½ β (TopOnβπΆ) β§ π΄ β πΆ β§ π₯ β πΆ) β (π₯ β ((clsβπ½)βπ΄) β (((neiβπ½)β{π₯}) βΎt π΄) β (Filβπ΄))) |
17 | 16 | biimpa 475 |
. . . . . . . 8
β’ (((π½ β (TopOnβπΆ) β§ π΄ β πΆ β§ π₯ β πΆ) β§ π₯ β ((clsβπ½)βπ΄)) β (((neiβπ½)β{π₯}) βΎt π΄) β (Filβπ΄)) |
18 | 9, 10, 15, 14, 17 | syl31anc 1371 |
. . . . . . 7
β’ ((((π½ β Top β§ πΎ β Haus) β§ (πΉ:π΄βΆπ΅ β§ π΄ β πΆ)) β§ π₯ β ((clsβπ½)βπ΄)) β (((neiβπ½)β{π₯}) βΎt π΄) β (Filβπ΄)) |
19 | | simplrl 773 |
. . . . . . 7
β’ ((((π½ β Top β§ πΎ β Haus) β§ (πΉ:π΄βΆπ΅ β§ π΄ β πΆ)) β§ π₯ β ((clsβπ½)βπ΄)) β πΉ:π΄βΆπ΅) |
20 | 3 | hausflf 23721 |
. . . . . . 7
β’ ((πΎ β Haus β§
(((neiβπ½)β{π₯}) βΎt π΄) β (Filβπ΄) β§ πΉ:π΄βΆπ΅) β β*π¦ π¦ β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ)) |
21 | 6, 18, 19, 20 | syl3anc 1369 |
. . . . . 6
β’ ((((π½ β Top β§ πΎ β Haus) β§ (πΉ:π΄βΆπ΅ β§ π΄ β πΆ)) β§ π₯ β ((clsβπ½)βπ΄)) β β*π¦ π¦ β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ)) |
22 | 21 | ex 411 |
. . . . 5
β’ (((π½ β Top β§ πΎ β Haus) β§ (πΉ:π΄βΆπ΅ β§ π΄ β πΆ)) β (π₯ β ((clsβπ½)βπ΄) β β*π¦ π¦ β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ))) |
23 | 22 | alrimiv 1928 |
. . . 4
β’ (((π½ β Top β§ πΎ β Haus) β§ (πΉ:π΄βΆπ΅ β§ π΄ β πΆ)) β βπ₯(π₯ β ((clsβπ½)βπ΄) β β*π¦ π¦ β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ))) |
24 | | moanimv 2613 |
. . . . 5
β’
(β*π¦(π₯ β ((clsβπ½)βπ΄) β§ π¦ β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ)) β (π₯ β ((clsβπ½)βπ΄) β β*π¦ π¦ β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ))) |
25 | 24 | albii 1819 |
. . . 4
β’
(βπ₯β*π¦(π₯ β ((clsβπ½)βπ΄) β§ π¦ β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ)) β βπ₯(π₯ β ((clsβπ½)βπ΄) β β*π¦ π¦ β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ))) |
26 | 23, 25 | sylibr 233 |
. . 3
β’ (((π½ β Top β§ πΎ β Haus) β§ (πΉ:π΄βΆπ΅ β§ π΄ β πΆ)) β βπ₯β*π¦(π₯ β ((clsβπ½)βπ΄) β§ π¦ β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ))) |
27 | | df-br 5148 |
. . . . . . 7
β’ (π₯((π½CnExtπΎ)βπΉ)π¦ β β¨π₯, π¦β© β ((π½CnExtπΎ)βπΉ)) |
28 | 27 | a1i 11 |
. . . . . 6
β’ (((π½ β Top β§ πΎ β Haus) β§ (πΉ:π΄βΆπ΅ β§ π΄ β πΆ)) β (π₯((π½CnExtπΎ)βπΉ)π¦ β β¨π₯, π¦β© β ((π½CnExtπΎ)βπΉ))) |
29 | 2, 3 | cnextfval 23786 |
. . . . . . . 8
β’ (((π½ β Top β§ πΎ β Top) β§ (πΉ:π΄βΆπ΅ β§ π΄ β πΆ)) β ((π½CnExtπΎ)βπΉ) = βͺ
π₯ β ((clsβπ½)βπ΄)({π₯} Γ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ))) |
30 | 1, 29 | sylanl2 677 |
. . . . . . 7
β’ (((π½ β Top β§ πΎ β Haus) β§ (πΉ:π΄βΆπ΅ β§ π΄ β πΆ)) β ((π½CnExtπΎ)βπΉ) = βͺ
π₯ β ((clsβπ½)βπ΄)({π₯} Γ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ))) |
31 | 30 | eleq2d 2817 |
. . . . . 6
β’ (((π½ β Top β§ πΎ β Haus) β§ (πΉ:π΄βΆπ΅ β§ π΄ β πΆ)) β (β¨π₯, π¦β© β ((π½CnExtπΎ)βπΉ) β β¨π₯, π¦β© β βͺ π₯ β ((clsβπ½)βπ΄)({π₯} Γ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ)))) |
32 | | opeliunxp 5742 |
. . . . . . 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 304 |
. . . . 5
β’ (((π½ β Top β§ πΎ β Haus) β§ (πΉ:π΄βΆπ΅ β§ π΄ β πΆ)) β (π₯((π½CnExtπΎ)βπΉ)π¦ β (π₯ β ((clsβπ½)βπ΄) β§ π¦ β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ)))) |
35 | 34 | mobidv 2541 |
. . . 4
β’ (((π½ β Top β§ πΎ β Haus) β§ (πΉ:π΄βΆπ΅ β§ π΄ β πΆ)) β (β*π¦ π₯((π½CnExtπΎ)βπΉ)π¦ β β*π¦(π₯ β ((clsβπ½)βπ΄) β§ π¦ β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ)))) |
36 | 35 | albidv 1921 |
. . 3
β’ (((π½ β Top β§ πΎ β Haus) β§ (πΉ:π΄βΆπ΅ β§ π΄ β πΆ)) β (βπ₯β*π¦ π₯((π½CnExtπΎ)βπΉ)π¦ β βπ₯β*π¦(π₯ β ((clsβπ½)βπ΄) β§ π¦ β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ)))) |
37 | 26, 36 | mpbird 256 |
. 2
β’ (((π½ β Top β§ πΎ β Haus) β§ (πΉ:π΄βΆπ΅ β§ π΄ β πΆ)) β βπ₯β*π¦ π₯((π½CnExtπΎ)βπΉ)π¦) |
38 | | dffun6 6555 |
. 2
β’ (Fun
((π½CnExtπΎ)βπΉ) β (Rel ((π½CnExtπΎ)βπΉ) β§ βπ₯β*π¦ π₯((π½CnExtπΎ)βπΉ)π¦)) |
39 | 5, 37, 38 | sylanbrc 581 |
1
β’ (((π½ β Top β§ πΎ β Haus) β§ (πΉ:π΄βΆπ΅ β§ π΄ β πΆ)) β Fun ((π½CnExtπΎ)βπΉ)) |