Step | Hyp | Ref
| Expression |
1 | | cmptop 22769 |
. . . 4
β’ (π½ β Comp β π½ β Top) |
2 | | flimfnfcls.x |
. . . . . 6
β’ π = βͺ
π½ |
3 | 2 | fclsval 23382 |
. . . . 5
β’ ((π½ β Top β§ πΉ β (Filβπ)) β (π½ fClus πΉ) = if(π = π, β© π₯ β πΉ ((clsβπ½)βπ₯), β
)) |
4 | | eqid 2733 |
. . . . . 6
β’ π = π |
5 | 4 | iftruei 4497 |
. . . . 5
β’ if(π = π, β© π₯ β πΉ ((clsβπ½)βπ₯), β
) = β© π₯ β πΉ ((clsβπ½)βπ₯) |
6 | 3, 5 | eqtrdi 2789 |
. . . 4
β’ ((π½ β Top β§ πΉ β (Filβπ)) β (π½ fClus πΉ) = β©
π₯ β πΉ ((clsβπ½)βπ₯)) |
7 | 1, 6 | sylan 581 |
. . 3
β’ ((π½ β Comp β§ πΉ β (Filβπ)) β (π½ fClus πΉ) = β©
π₯ β πΉ ((clsβπ½)βπ₯)) |
8 | | fvex 6859 |
. . . 4
β’
((clsβπ½)βπ₯) β V |
9 | 8 | dfiin3 5926 |
. . 3
β’ β© π₯ β πΉ ((clsβπ½)βπ₯) = β© ran (π₯ β πΉ β¦ ((clsβπ½)βπ₯)) |
10 | 7, 9 | eqtrdi 2789 |
. 2
β’ ((π½ β Comp β§ πΉ β (Filβπ)) β (π½ fClus πΉ) = β© ran (π₯ β πΉ β¦ ((clsβπ½)βπ₯))) |
11 | | simpl 484 |
. . 3
β’ ((π½ β Comp β§ πΉ β (Filβπ)) β π½ β Comp) |
12 | 11 | adantr 482 |
. . . . . . 7
β’ (((π½ β Comp β§ πΉ β (Filβπ)) β§ π₯ β πΉ) β π½ β Comp) |
13 | 12, 1 | syl 17 |
. . . . . 6
β’ (((π½ β Comp β§ πΉ β (Filβπ)) β§ π₯ β πΉ) β π½ β Top) |
14 | | filelss 23226 |
. . . . . . 7
β’ ((πΉ β (Filβπ) β§ π₯ β πΉ) β π₯ β π) |
15 | 14 | adantll 713 |
. . . . . 6
β’ (((π½ β Comp β§ πΉ β (Filβπ)) β§ π₯ β πΉ) β π₯ β π) |
16 | 2 | clscld 22421 |
. . . . . 6
β’ ((π½ β Top β§ π₯ β π) β ((clsβπ½)βπ₯) β (Clsdβπ½)) |
17 | 13, 15, 16 | syl2anc 585 |
. . . . 5
β’ (((π½ β Comp β§ πΉ β (Filβπ)) β§ π₯ β πΉ) β ((clsβπ½)βπ₯) β (Clsdβπ½)) |
18 | 17 | fmpttd 7067 |
. . . 4
β’ ((π½ β Comp β§ πΉ β (Filβπ)) β (π₯ β πΉ β¦ ((clsβπ½)βπ₯)):πΉβΆ(Clsdβπ½)) |
19 | 18 | frnd 6680 |
. . 3
β’ ((π½ β Comp β§ πΉ β (Filβπ)) β ran (π₯ β πΉ β¦ ((clsβπ½)βπ₯)) β (Clsdβπ½)) |
20 | | simpr 486 |
. . . . . 6
β’ ((π½ β Comp β§ πΉ β (Filβπ)) β πΉ β (Filβπ)) |
21 | 20 | adantr 482 |
. . . . . . . . 9
β’ (((π½ β Comp β§ πΉ β (Filβπ)) β§ π₯ β πΉ) β πΉ β (Filβπ)) |
22 | | simpr 486 |
. . . . . . . . 9
β’ (((π½ β Comp β§ πΉ β (Filβπ)) β§ π₯ β πΉ) β π₯ β πΉ) |
23 | 2 | clsss3 22433 |
. . . . . . . . . 10
β’ ((π½ β Top β§ π₯ β π) β ((clsβπ½)βπ₯) β π) |
24 | 13, 15, 23 | syl2anc 585 |
. . . . . . . . 9
β’ (((π½ β Comp β§ πΉ β (Filβπ)) β§ π₯ β πΉ) β ((clsβπ½)βπ₯) β π) |
25 | 2 | sscls 22430 |
. . . . . . . . . 10
β’ ((π½ β Top β§ π₯ β π) β π₯ β ((clsβπ½)βπ₯)) |
26 | 13, 15, 25 | syl2anc 585 |
. . . . . . . . 9
β’ (((π½ β Comp β§ πΉ β (Filβπ)) β§ π₯ β πΉ) β π₯ β ((clsβπ½)βπ₯)) |
27 | | filss 23227 |
. . . . . . . . 9
β’ ((πΉ β (Filβπ) β§ (π₯ β πΉ β§ ((clsβπ½)βπ₯) β π β§ π₯ β ((clsβπ½)βπ₯))) β ((clsβπ½)βπ₯) β πΉ) |
28 | 21, 22, 24, 26, 27 | syl13anc 1373 |
. . . . . . . 8
β’ (((π½ β Comp β§ πΉ β (Filβπ)) β§ π₯ β πΉ) β ((clsβπ½)βπ₯) β πΉ) |
29 | 28 | fmpttd 7067 |
. . . . . . 7
β’ ((π½ β Comp β§ πΉ β (Filβπ)) β (π₯ β πΉ β¦ ((clsβπ½)βπ₯)):πΉβΆπΉ) |
30 | 29 | frnd 6680 |
. . . . . 6
β’ ((π½ β Comp β§ πΉ β (Filβπ)) β ran (π₯ β πΉ β¦ ((clsβπ½)βπ₯)) β πΉ) |
31 | | fiss 9368 |
. . . . . 6
β’ ((πΉ β (Filβπ) β§ ran (π₯ β πΉ β¦ ((clsβπ½)βπ₯)) β πΉ) β (fiβran (π₯ β πΉ β¦ ((clsβπ½)βπ₯))) β (fiβπΉ)) |
32 | 20, 30, 31 | syl2anc 585 |
. . . . 5
β’ ((π½ β Comp β§ πΉ β (Filβπ)) β (fiβran (π₯ β πΉ β¦ ((clsβπ½)βπ₯))) β (fiβπΉ)) |
33 | | filfi 23233 |
. . . . . 6
β’ (πΉ β (Filβπ) β (fiβπΉ) = πΉ) |
34 | 20, 33 | syl 17 |
. . . . 5
β’ ((π½ β Comp β§ πΉ β (Filβπ)) β (fiβπΉ) = πΉ) |
35 | 32, 34 | sseqtrd 3988 |
. . . 4
β’ ((π½ β Comp β§ πΉ β (Filβπ)) β (fiβran (π₯ β πΉ β¦ ((clsβπ½)βπ₯))) β πΉ) |
36 | | 0nelfil 23223 |
. . . . 5
β’ (πΉ β (Filβπ) β Β¬ β
β
πΉ) |
37 | 20, 36 | syl 17 |
. . . 4
β’ ((π½ β Comp β§ πΉ β (Filβπ)) β Β¬ β
β
πΉ) |
38 | 35, 37 | ssneldd 3951 |
. . 3
β’ ((π½ β Comp β§ πΉ β (Filβπ)) β Β¬ β
β
(fiβran (π₯ β
πΉ β¦ ((clsβπ½)βπ₯)))) |
39 | | cmpfii 22783 |
. . 3
β’ ((π½ β Comp β§ ran (π₯ β πΉ β¦ ((clsβπ½)βπ₯)) β (Clsdβπ½) β§ Β¬ β
β (fiβran
(π₯ β πΉ β¦ ((clsβπ½)βπ₯)))) β β© ran
(π₯ β πΉ β¦ ((clsβπ½)βπ₯)) β β
) |
40 | 11, 19, 38, 39 | syl3anc 1372 |
. 2
β’ ((π½ β Comp β§ πΉ β (Filβπ)) β β© ran (π₯ β πΉ β¦ ((clsβπ½)βπ₯)) β β
) |
41 | 10, 40 | eqnetrd 3008 |
1
β’ ((π½ β Comp β§ πΉ β (Filβπ)) β (π½ fClus πΉ) β β
) |