Step | Hyp | Ref
| Expression |
1 | | simpll 766 |
. . . . . . 7
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (π½ β πΎ β§ π₯ β (πΎ fClus π))) β π½ β (TopOnβπ)) |
2 | | simplr 768 |
. . . . . . . 8
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (π½ β πΎ β§ π₯ β (πΎ fClus π))) β πΎ β (TopOnβπ)) |
3 | | fclstopon 23379 |
. . . . . . . . 9
β’ (π₯ β (πΎ fClus π) β (πΎ β (TopOnβπ) β π β (Filβπ))) |
4 | 3 | ad2antll 728 |
. . . . . . . 8
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (π½ β πΎ β§ π₯ β (πΎ fClus π))) β (πΎ β (TopOnβπ) β π β (Filβπ))) |
5 | 2, 4 | mpbid 231 |
. . . . . . 7
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (π½ β πΎ β§ π₯ β (πΎ fClus π))) β π β (Filβπ)) |
6 | | simprl 770 |
. . . . . . 7
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (π½ β πΎ β§ π₯ β (πΎ fClus π))) β π½ β πΎ) |
7 | | fclsss1 23389 |
. . . . . . 7
β’ ((π½ β (TopOnβπ) β§ π β (Filβπ) β§ π½ β πΎ) β (πΎ fClus π) β (π½ fClus π)) |
8 | 1, 5, 6, 7 | syl3anc 1372 |
. . . . . 6
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (π½ β πΎ β§ π₯ β (πΎ fClus π))) β (πΎ fClus π) β (π½ fClus π)) |
9 | | simprr 772 |
. . . . . 6
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (π½ β πΎ β§ π₯ β (πΎ fClus π))) β π₯ β (πΎ fClus π)) |
10 | 8, 9 | sseldd 3950 |
. . . . 5
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (π½ β πΎ β§ π₯ β (πΎ fClus π))) β π₯ β (π½ fClus π)) |
11 | 10 | expr 458 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ π½ β πΎ) β (π₯ β (πΎ fClus π) β π₯ β (π½ fClus π))) |
12 | 11 | ssrdv 3955 |
. . 3
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ π½ β πΎ) β (πΎ fClus π) β (π½ fClus π)) |
13 | 12 | ralrimivw 3148 |
. 2
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ π½ β πΎ) β βπ β (Filβπ)(πΎ fClus π) β (π½ fClus π)) |
14 | | simpllr 775 |
. . . . . . . . 9
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ βπ β (Filβπ)(πΎ fClus π) β (π½ fClus π)) β§ π₯ β π½) β πΎ β (TopOnβπ)) |
15 | | toponmax 22291 |
. . . . . . . . 9
β’ (πΎ β (TopOnβπ) β π β πΎ) |
16 | | ssid 3971 |
. . . . . . . . . . 11
β’ π β π |
17 | | eleq2 2827 |
. . . . . . . . . . . . 13
β’ (π’ = π β (π¦ β π’ β π¦ β π)) |
18 | | sseq1 3974 |
. . . . . . . . . . . . 13
β’ (π’ = π β (π’ β π β π β π)) |
19 | 17, 18 | anbi12d 632 |
. . . . . . . . . . . 12
β’ (π’ = π β ((π¦ β π’ β§ π’ β π) β (π¦ β π β§ π β π))) |
20 | 19 | rspcev 3584 |
. . . . . . . . . . 11
β’ ((π β πΎ β§ (π¦ β π β§ π β π)) β βπ’ β πΎ (π¦ β π’ β§ π’ β π)) |
21 | 16, 20 | mpanr2 703 |
. . . . . . . . . 10
β’ ((π β πΎ β§ π¦ β π) β βπ’ β πΎ (π¦ β π’ β§ π’ β π)) |
22 | 21 | ex 414 |
. . . . . . . . 9
β’ (π β πΎ β (π¦ β π β βπ’ β πΎ (π¦ β π’ β§ π’ β π))) |
23 | 14, 15, 22 | 3syl 18 |
. . . . . . . 8
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ βπ β (Filβπ)(πΎ fClus π) β (π½ fClus π)) β§ π₯ β π½) β (π¦ β π β βπ’ β πΎ (π¦ β π’ β§ π’ β π))) |
24 | | eleq2 2827 |
. . . . . . . . 9
β’ (π₯ = π β (π¦ β π₯ β π¦ β π)) |
25 | | sseq2 3975 |
. . . . . . . . . . 11
β’ (π₯ = π β (π’ β π₯ β π’ β π)) |
26 | 25 | anbi2d 630 |
. . . . . . . . . 10
β’ (π₯ = π β ((π¦ β π’ β§ π’ β π₯) β (π¦ β π’ β§ π’ β π))) |
27 | 26 | rexbidv 3176 |
. . . . . . . . 9
β’ (π₯ = π β (βπ’ β πΎ (π¦ β π’ β§ π’ β π₯) β βπ’ β πΎ (π¦ β π’ β§ π’ β π))) |
28 | 24, 27 | imbi12d 345 |
. . . . . . . 8
β’ (π₯ = π β ((π¦ β π₯ β βπ’ β πΎ (π¦ β π’ β§ π’ β π₯)) β (π¦ β π β βπ’ β πΎ (π¦ β π’ β§ π’ β π)))) |
29 | 23, 28 | syl5ibrcom 247 |
. . . . . . 7
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ βπ β (Filβπ)(πΎ fClus π) β (π½ fClus π)) β§ π₯ β π½) β (π₯ = π β (π¦ β π₯ β βπ’ β πΎ (π¦ β π’ β§ π’ β π₯)))) |
30 | | simplll 774 |
. . . . . . . . . . . 12
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ βπ β (Filβπ)(πΎ fClus π) β (π½ fClus π)) β§ (π₯ β π½ β§ (π₯ β π β§ π¦ β π₯))) β π½ β (TopOnβπ)) |
31 | | simprl 770 |
. . . . . . . . . . . 12
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ βπ β (Filβπ)(πΎ fClus π) β (π½ fClus π)) β§ (π₯ β π½ β§ (π₯ β π β§ π¦ β π₯))) β π₯ β π½) |
32 | | simprrr 781 |
. . . . . . . . . . . 12
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ βπ β (Filβπ)(πΎ fClus π) β (π½ fClus π)) β§ (π₯ β π½ β§ (π₯ β π β§ π¦ β π₯))) β π¦ β π₯) |
33 | | supnfcls 23387 |
. . . . . . . . . . . 12
β’ ((π½ β (TopOnβπ) β§ π₯ β π½ β§ π¦ β π₯) β Β¬ π¦ β (π½ fClus {π¦ β π« π β£ (π β π₯) β π¦})) |
34 | 30, 31, 32, 33 | syl3anc 1372 |
. . . . . . . . . . 11
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ βπ β (Filβπ)(πΎ fClus π) β (π½ fClus π)) β§ (π₯ β π½ β§ (π₯ β π β§ π¦ β π₯))) β Β¬ π¦ β (π½ fClus {π¦ β π« π β£ (π β π₯) β π¦})) |
35 | | toponss 22292 |
. . . . . . . . . . . . . . 15
β’ ((π½ β (TopOnβπ) β§ π₯ β π½) β π₯ β π) |
36 | 30, 31, 35 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ βπ β (Filβπ)(πΎ fClus π) β (π½ fClus π)) β§ (π₯ β π½ β§ (π₯ β π β§ π¦ β π₯))) β π₯ β π) |
37 | 36, 32 | sseldd 3950 |
. . . . . . . . . . . . 13
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ βπ β (Filβπ)(πΎ fClus π) β (π½ fClus π)) β§ (π₯ β π½ β§ (π₯ β π β§ π¦ β π₯))) β π¦ β π) |
38 | | simpllr 775 |
. . . . . . . . . . . . . 14
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ βπ β (Filβπ)(πΎ fClus π) β (π½ fClus π)) β§ (π₯ β π½ β§ (π₯ β π β§ π¦ β π₯))) β πΎ β (TopOnβπ)) |
39 | | toponmax 22291 |
. . . . . . . . . . . . . . . 16
β’ (π½ β (TopOnβπ) β π β π½) |
40 | 30, 39 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ βπ β (Filβπ)(πΎ fClus π) β (π½ fClus π)) β§ (π₯ β π½ β§ (π₯ β π β§ π¦ β π₯))) β π β π½) |
41 | | difssd 4097 |
. . . . . . . . . . . . . . 15
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ βπ β (Filβπ)(πΎ fClus π) β (π½ fClus π)) β§ (π₯ β π½ β§ (π₯ β π β§ π¦ β π₯))) β (π β π₯) β π) |
42 | | simprrl 780 |
. . . . . . . . . . . . . . . 16
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ βπ β (Filβπ)(πΎ fClus π) β (π½ fClus π)) β§ (π₯ β π½ β§ (π₯ β π β§ π¦ β π₯))) β π₯ β π) |
43 | | pssdifn0 4330 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β π β§ π₯ β π) β (π β π₯) β β
) |
44 | 36, 42, 43 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ βπ β (Filβπ)(πΎ fClus π) β (π½ fClus π)) β§ (π₯ β π½ β§ (π₯ β π β§ π¦ β π₯))) β (π β π₯) β β
) |
45 | | supfil 23262 |
. . . . . . . . . . . . . . 15
β’ ((π β π½ β§ (π β π₯) β π β§ (π β π₯) β β
) β {π¦ β π« π β£ (π β π₯) β π¦} β (Filβπ)) |
46 | 40, 41, 44, 45 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ βπ β (Filβπ)(πΎ fClus π) β (π½ fClus π)) β§ (π₯ β π½ β§ (π₯ β π β§ π¦ β π₯))) β {π¦ β π« π β£ (π β π₯) β π¦} β (Filβπ)) |
47 | | fclsopn 23381 |
. . . . . . . . . . . . . 14
β’ ((πΎ β (TopOnβπ) β§ {π¦ β π« π β£ (π β π₯) β π¦} β (Filβπ)) β (π¦ β (πΎ fClus {π¦ β π« π β£ (π β π₯) β π¦}) β (π¦ β π β§ βπ’ β πΎ (π¦ β π’ β βπ β {π¦ β π« π β£ (π β π₯) β π¦} (π’ β© π) β β
)))) |
48 | 38, 46, 47 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ βπ β (Filβπ)(πΎ fClus π) β (π½ fClus π)) β§ (π₯ β π½ β§ (π₯ β π β§ π¦ β π₯))) β (π¦ β (πΎ fClus {π¦ β π« π β£ (π β π₯) β π¦}) β (π¦ β π β§ βπ’ β πΎ (π¦ β π’ β βπ β {π¦ β π« π β£ (π β π₯) β π¦} (π’ β© π) β β
)))) |
49 | 37, 48 | mpbirand 706 |
. . . . . . . . . . . 12
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ βπ β (Filβπ)(πΎ fClus π) β (π½ fClus π)) β§ (π₯ β π½ β§ (π₯ β π β§ π¦ β π₯))) β (π¦ β (πΎ fClus {π¦ β π« π β£ (π β π₯) β π¦}) β βπ’ β πΎ (π¦ β π’ β βπ β {π¦ β π« π β£ (π β π₯) β π¦} (π’ β© π) β β
))) |
50 | | oveq2 7370 |
. . . . . . . . . . . . . . 15
β’ (π = {π¦ β π« π β£ (π β π₯) β π¦} β (πΎ fClus π) = (πΎ fClus {π¦ β π« π β£ (π β π₯) β π¦})) |
51 | | oveq2 7370 |
. . . . . . . . . . . . . . 15
β’ (π = {π¦ β π« π β£ (π β π₯) β π¦} β (π½ fClus π) = (π½ fClus {π¦ β π« π β£ (π β π₯) β π¦})) |
52 | 50, 51 | sseq12d 3982 |
. . . . . . . . . . . . . 14
β’ (π = {π¦ β π« π β£ (π β π₯) β π¦} β ((πΎ fClus π) β (π½ fClus π) β (πΎ fClus {π¦ β π« π β£ (π β π₯) β π¦}) β (π½ fClus {π¦ β π« π β£ (π β π₯) β π¦}))) |
53 | | simplr 768 |
. . . . . . . . . . . . . 14
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ βπ β (Filβπ)(πΎ fClus π) β (π½ fClus π)) β§ (π₯ β π½ β§ (π₯ β π β§ π¦ β π₯))) β βπ β (Filβπ)(πΎ fClus π) β (π½ fClus π)) |
54 | 52, 53, 46 | rspcdva 3585 |
. . . . . . . . . . . . 13
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ βπ β (Filβπ)(πΎ fClus π) β (π½ fClus π)) β§ (π₯ β π½ β§ (π₯ β π β§ π¦ β π₯))) β (πΎ fClus {π¦ β π« π β£ (π β π₯) β π¦}) β (π½ fClus {π¦ β π« π β£ (π β π₯) β π¦})) |
55 | 54 | sseld 3948 |
. . . . . . . . . . . 12
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ βπ β (Filβπ)(πΎ fClus π) β (π½ fClus π)) β§ (π₯ β π½ β§ (π₯ β π β§ π¦ β π₯))) β (π¦ β (πΎ fClus {π¦ β π« π β£ (π β π₯) β π¦}) β π¦ β (π½ fClus {π¦ β π« π β£ (π β π₯) β π¦}))) |
56 | 49, 55 | sylbird 260 |
. . . . . . . . . . 11
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ βπ β (Filβπ)(πΎ fClus π) β (π½ fClus π)) β§ (π₯ β π½ β§ (π₯ β π β§ π¦ β π₯))) β (βπ’ β πΎ (π¦ β π’ β βπ β {π¦ β π« π β£ (π β π₯) β π¦} (π’ β© π) β β
) β π¦ β (π½ fClus {π¦ β π« π β£ (π β π₯) β π¦}))) |
57 | 34, 56 | mtod 197 |
. . . . . . . . . 10
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ βπ β (Filβπ)(πΎ fClus π) β (π½ fClus π)) β§ (π₯ β π½ β§ (π₯ β π β§ π¦ β π₯))) β Β¬ βπ’ β πΎ (π¦ β π’ β βπ β {π¦ β π« π β£ (π β π₯) β π¦} (π’ β© π) β β
)) |
58 | | rexanali 3106 |
. . . . . . . . . . 11
β’
(βπ’ β
πΎ (π¦ β π’ β§ Β¬ βπ β {π¦ β π« π β£ (π β π₯) β π¦} (π’ β© π) β β
) β Β¬ βπ’ β πΎ (π¦ β π’ β βπ β {π¦ β π« π β£ (π β π₯) β π¦} (π’ β© π) β β
)) |
59 | | rexnal 3104 |
. . . . . . . . . . . . . 14
β’
(βπ β
{π¦ β π« π β£ (π β π₯) β π¦} Β¬ (π’ β© π) β β
β Β¬ βπ β {π¦ β π« π β£ (π β π₯) β π¦} (π’ β© π) β β
) |
60 | | sseq2 3975 |
. . . . . . . . . . . . . . . . . 18
β’ (π¦ = π β ((π β π₯) β π¦ β (π β π₯) β π)) |
61 | 60 | elrab 3650 |
. . . . . . . . . . . . . . . . 17
β’ (π β {π¦ β π« π β£ (π β π₯) β π¦} β (π β π« π β§ (π β π₯) β π)) |
62 | | sslin 4199 |
. . . . . . . . . . . . . . . . 17
β’ ((π β π₯) β π β (π’ β© (π β π₯)) β (π’ β© π)) |
63 | 61, 62 | simplbiim 506 |
. . . . . . . . . . . . . . . 16
β’ (π β {π¦ β π« π β£ (π β π₯) β π¦} β (π’ β© (π β π₯)) β (π’ β© π)) |
64 | | ssn0 4365 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π’ β© (π β π₯)) β (π’ β© π) β§ (π’ β© (π β π₯)) β β
) β (π’ β© π) β β
) |
65 | 64 | ex 414 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π’ β© (π β π₯)) β (π’ β© π) β ((π’ β© (π β π₯)) β β
β (π’ β© π) β β
)) |
66 | 65 | necon1bd 2962 |
. . . . . . . . . . . . . . . . . 18
β’ ((π’ β© (π β π₯)) β (π’ β© π) β (Β¬ (π’ β© π) β β
β (π’ β© (π β π₯)) = β
)) |
67 | | inssdif0 4334 |
. . . . . . . . . . . . . . . . . 18
β’ ((π’ β© π) β π₯ β (π’ β© (π β π₯)) = β
) |
68 | 66, 67 | syl6ibr 252 |
. . . . . . . . . . . . . . . . 17
β’ ((π’ β© (π β π₯)) β (π’ β© π) β (Β¬ (π’ β© π) β β
β (π’ β© π) β π₯)) |
69 | | toponss 22292 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((πΎ β (TopOnβπ) β§ π’ β πΎ) β π’ β π) |
70 | 38, 69 | sylan 581 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π½ β
(TopOnβπ) β§ πΎ β (TopOnβπ)) β§ βπ β (Filβπ)(πΎ fClus π) β (π½ fClus π)) β§ (π₯ β π½ β§ (π₯ β π β§ π¦ β π₯))) β§ π’ β πΎ) β π’ β π) |
71 | | df-ss 3932 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π’ β π β (π’ β© π) = π’) |
72 | 70, 71 | sylib 217 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π½ β
(TopOnβπ) β§ πΎ β (TopOnβπ)) β§ βπ β (Filβπ)(πΎ fClus π) β (π½ fClus π)) β§ (π₯ β π½ β§ (π₯ β π β§ π¦ β π₯))) β§ π’ β πΎ) β (π’ β© π) = π’) |
73 | 72 | sseq1d 3980 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π½ β
(TopOnβπ) β§ πΎ β (TopOnβπ)) β§ βπ β (Filβπ)(πΎ fClus π) β (π½ fClus π)) β§ (π₯ β π½ β§ (π₯ β π β§ π¦ β π₯))) β§ π’ β πΎ) β ((π’ β© π) β π₯ β π’ β π₯)) |
74 | 73 | biimpd 228 |
. . . . . . . . . . . . . . . . 17
β’
(((((π½ β
(TopOnβπ) β§ πΎ β (TopOnβπ)) β§ βπ β (Filβπ)(πΎ fClus π) β (π½ fClus π)) β§ (π₯ β π½ β§ (π₯ β π β§ π¦ β π₯))) β§ π’ β πΎ) β ((π’ β© π) β π₯ β π’ β π₯)) |
75 | 68, 74 | syl9r 78 |
. . . . . . . . . . . . . . . 16
β’
(((((π½ β
(TopOnβπ) β§ πΎ β (TopOnβπ)) β§ βπ β (Filβπ)(πΎ fClus π) β (π½ fClus π)) β§ (π₯ β π½ β§ (π₯ β π β§ π¦ β π₯))) β§ π’ β πΎ) β ((π’ β© (π β π₯)) β (π’ β© π) β (Β¬ (π’ β© π) β β
β π’ β π₯))) |
76 | 63, 75 | syl5 34 |
. . . . . . . . . . . . . . 15
β’
(((((π½ β
(TopOnβπ) β§ πΎ β (TopOnβπ)) β§ βπ β (Filβπ)(πΎ fClus π) β (π½ fClus π)) β§ (π₯ β π½ β§ (π₯ β π β§ π¦ β π₯))) β§ π’ β πΎ) β (π β {π¦ β π« π β£ (π β π₯) β π¦} β (Β¬ (π’ β© π) β β
β π’ β π₯))) |
77 | 76 | rexlimdv 3151 |
. . . . . . . . . . . . . 14
β’
(((((π½ β
(TopOnβπ) β§ πΎ β (TopOnβπ)) β§ βπ β (Filβπ)(πΎ fClus π) β (π½ fClus π)) β§ (π₯ β π½ β§ (π₯ β π β§ π¦ β π₯))) β§ π’ β πΎ) β (βπ β {π¦ β π« π β£ (π β π₯) β π¦} Β¬ (π’ β© π) β β
β π’ β π₯)) |
78 | 59, 77 | biimtrrid 242 |
. . . . . . . . . . . . 13
β’
(((((π½ β
(TopOnβπ) β§ πΎ β (TopOnβπ)) β§ βπ β (Filβπ)(πΎ fClus π) β (π½ fClus π)) β§ (π₯ β π½ β§ (π₯ β π β§ π¦ β π₯))) β§ π’ β πΎ) β (Β¬ βπ β {π¦ β π« π β£ (π β π₯) β π¦} (π’ β© π) β β
β π’ β π₯)) |
79 | 78 | anim2d 613 |
. . . . . . . . . . . 12
β’
(((((π½ β
(TopOnβπ) β§ πΎ β (TopOnβπ)) β§ βπ β (Filβπ)(πΎ fClus π) β (π½ fClus π)) β§ (π₯ β π½ β§ (π₯ β π β§ π¦ β π₯))) β§ π’ β πΎ) β ((π¦ β π’ β§ Β¬ βπ β {π¦ β π« π β£ (π β π₯) β π¦} (π’ β© π) β β
) β (π¦ β π’ β§ π’ β π₯))) |
80 | 79 | reximdva 3166 |
. . . . . . . . . . 11
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ βπ β (Filβπ)(πΎ fClus π) β (π½ fClus π)) β§ (π₯ β π½ β§ (π₯ β π β§ π¦ β π₯))) β (βπ’ β πΎ (π¦ β π’ β§ Β¬ βπ β {π¦ β π« π β£ (π β π₯) β π¦} (π’ β© π) β β
) β βπ’ β πΎ (π¦ β π’ β§ π’ β π₯))) |
81 | 58, 80 | biimtrrid 242 |
. . . . . . . . . 10
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ βπ β (Filβπ)(πΎ fClus π) β (π½ fClus π)) β§ (π₯ β π½ β§ (π₯ β π β§ π¦ β π₯))) β (Β¬ βπ’ β πΎ (π¦ β π’ β βπ β {π¦ β π« π β£ (π β π₯) β π¦} (π’ β© π) β β
) β βπ’ β πΎ (π¦ β π’ β§ π’ β π₯))) |
82 | 57, 81 | mpd 15 |
. . . . . . . . 9
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ βπ β (Filβπ)(πΎ fClus π) β (π½ fClus π)) β§ (π₯ β π½ β§ (π₯ β π β§ π¦ β π₯))) β βπ’ β πΎ (π¦ β π’ β§ π’ β π₯)) |
83 | 82 | anassrs 469 |
. . . . . . . 8
β’
(((((π½ β
(TopOnβπ) β§ πΎ β (TopOnβπ)) β§ βπ β (Filβπ)(πΎ fClus π) β (π½ fClus π)) β§ π₯ β π½) β§ (π₯ β π β§ π¦ β π₯)) β βπ’ β πΎ (π¦ β π’ β§ π’ β π₯)) |
84 | 83 | exp32 422 |
. . . . . . 7
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ βπ β (Filβπ)(πΎ fClus π) β (π½ fClus π)) β§ π₯ β π½) β (π₯ β π β (π¦ β π₯ β βπ’ β πΎ (π¦ β π’ β§ π’ β π₯)))) |
85 | 29, 84 | pm2.61dne 3032 |
. . . . . 6
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ βπ β (Filβπ)(πΎ fClus π) β (π½ fClus π)) β§ π₯ β π½) β (π¦ β π₯ β βπ’ β πΎ (π¦ β π’ β§ π’ β π₯))) |
86 | 85 | ralrimiv 3143 |
. . . . 5
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ βπ β (Filβπ)(πΎ fClus π) β (π½ fClus π)) β§ π₯ β π½) β βπ¦ β π₯ βπ’ β πΎ (π¦ β π’ β§ π’ β π₯)) |
87 | | topontop 22278 |
. . . . . 6
β’ (πΎ β (TopOnβπ) β πΎ β Top) |
88 | | eltop2 22341 |
. . . . . 6
β’ (πΎ β Top β (π₯ β πΎ β βπ¦ β π₯ βπ’ β πΎ (π¦ β π’ β§ π’ β π₯))) |
89 | 14, 87, 88 | 3syl 18 |
. . . . 5
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ βπ β (Filβπ)(πΎ fClus π) β (π½ fClus π)) β§ π₯ β π½) β (π₯ β πΎ β βπ¦ β π₯ βπ’ β πΎ (π¦ β π’ β§ π’ β π₯))) |
90 | 86, 89 | mpbird 257 |
. . . 4
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ βπ β (Filβπ)(πΎ fClus π) β (π½ fClus π)) β§ π₯ β π½) β π₯ β πΎ) |
91 | 90 | ex 414 |
. . 3
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ βπ β (Filβπ)(πΎ fClus π) β (π½ fClus π)) β (π₯ β π½ β π₯ β πΎ)) |
92 | 91 | ssrdv 3955 |
. 2
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ βπ β (Filβπ)(πΎ fClus π) β (π½ fClus π)) β π½ β πΎ) |
93 | 13, 92 | impbida 800 |
1
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β (π½ β πΎ β βπ β (Filβπ)(πΎ fClus π) β (π½ fClus π))) |