Step | Hyp | Ref
| Expression |
1 | | isfcf 23408 |
. 2
β’ ((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β (π΄ β ((π½ fClusf πΏ)βπΉ) β (π΄ β π β§ βπ β π½ (π΄ β π β βπ β πΏ (π β© (πΉ β π )) β β
)))) |
2 | | simpll1 1213 |
. . . . . . . 8
β’ ((((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π΄ β π) β§ π β ((neiβπ½)β{π΄})) β π½ β (TopOnβπ)) |
3 | | topontop 22285 |
. . . . . . . 8
β’ (π½ β (TopOnβπ) β π½ β Top) |
4 | 2, 3 | syl 17 |
. . . . . . 7
β’ ((((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π΄ β π) β§ π β ((neiβπ½)β{π΄})) β π½ β Top) |
5 | | simpr 486 |
. . . . . . . 8
β’ ((((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π΄ β π) β§ π β ((neiβπ½)β{π΄})) β π β ((neiβπ½)β{π΄})) |
6 | | eqid 2733 |
. . . . . . . . 9
β’ βͺ π½ =
βͺ π½ |
7 | 6 | neii1 22480 |
. . . . . . . 8
β’ ((π½ β Top β§ π β ((neiβπ½)β{π΄})) β π β βͺ π½) |
8 | 4, 5, 7 | syl2anc 585 |
. . . . . . 7
β’ ((((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π΄ β π) β§ π β ((neiβπ½)β{π΄})) β π β βͺ π½) |
9 | 6 | ntrss2 22431 |
. . . . . . 7
β’ ((π½ β Top β§ π β βͺ π½)
β ((intβπ½)βπ) β π) |
10 | 4, 8, 9 | syl2anc 585 |
. . . . . 6
β’ ((((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π΄ β π) β§ π β ((neiβπ½)β{π΄})) β ((intβπ½)βπ) β π) |
11 | | simplr 768 |
. . . . . . . . . . . 12
β’ ((((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π΄ β π) β§ π β ((neiβπ½)β{π΄})) β π΄ β π) |
12 | | toponuni 22286 |
. . . . . . . . . . . . 13
β’ (π½ β (TopOnβπ) β π = βͺ π½) |
13 | 2, 12 | syl 17 |
. . . . . . . . . . . 12
β’ ((((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π΄ β π) β§ π β ((neiβπ½)β{π΄})) β π = βͺ π½) |
14 | 11, 13 | eleqtrd 2836 |
. . . . . . . . . . 11
β’ ((((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π΄ β π) β§ π β ((neiβπ½)β{π΄})) β π΄ β βͺ π½) |
15 | 14 | snssd 4773 |
. . . . . . . . . 10
β’ ((((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π΄ β π) β§ π β ((neiβπ½)β{π΄})) β {π΄} β βͺ π½) |
16 | 6 | neiint 22478 |
. . . . . . . . . 10
β’ ((π½ β Top β§ {π΄} β βͺ π½
β§ π β βͺ π½)
β (π β
((neiβπ½)β{π΄}) β {π΄} β ((intβπ½)βπ))) |
17 | 4, 15, 8, 16 | syl3anc 1372 |
. . . . . . . . 9
β’ ((((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π΄ β π) β§ π β ((neiβπ½)β{π΄})) β (π β ((neiβπ½)β{π΄}) β {π΄} β ((intβπ½)βπ))) |
18 | 5, 17 | mpbid 231 |
. . . . . . . 8
β’ ((((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π΄ β π) β§ π β ((neiβπ½)β{π΄})) β {π΄} β ((intβπ½)βπ)) |
19 | | snssg 4748 |
. . . . . . . . 9
β’ (π΄ β π β (π΄ β ((intβπ½)βπ) β {π΄} β ((intβπ½)βπ))) |
20 | 11, 19 | syl 17 |
. . . . . . . 8
β’ ((((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π΄ β π) β§ π β ((neiβπ½)β{π΄})) β (π΄ β ((intβπ½)βπ) β {π΄} β ((intβπ½)βπ))) |
21 | 18, 20 | mpbird 257 |
. . . . . . 7
β’ ((((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π΄ β π) β§ π β ((neiβπ½)β{π΄})) β π΄ β ((intβπ½)βπ)) |
22 | 6 | ntropn 22423 |
. . . . . . . . 9
β’ ((π½ β Top β§ π β βͺ π½)
β ((intβπ½)βπ) β π½) |
23 | 4, 8, 22 | syl2anc 585 |
. . . . . . . 8
β’ ((((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π΄ β π) β§ π β ((neiβπ½)β{π΄})) β ((intβπ½)βπ) β π½) |
24 | | eleq2 2823 |
. . . . . . . . . 10
β’ (π = ((intβπ½)βπ) β (π΄ β π β π΄ β ((intβπ½)βπ))) |
25 | | ineq1 4169 |
. . . . . . . . . . . 12
β’ (π = ((intβπ½)βπ) β (π β© (πΉ β π )) = (((intβπ½)βπ) β© (πΉ β π ))) |
26 | 25 | neeq1d 3000 |
. . . . . . . . . . 11
β’ (π = ((intβπ½)βπ) β ((π β© (πΉ β π )) β β
β (((intβπ½)βπ) β© (πΉ β π )) β β
)) |
27 | 26 | ralbidv 3171 |
. . . . . . . . . 10
β’ (π = ((intβπ½)βπ) β (βπ β πΏ (π β© (πΉ β π )) β β
β βπ β πΏ (((intβπ½)βπ) β© (πΉ β π )) β β
)) |
28 | 24, 27 | imbi12d 345 |
. . . . . . . . 9
β’ (π = ((intβπ½)βπ) β ((π΄ β π β βπ β πΏ (π β© (πΉ β π )) β β
) β (π΄ β ((intβπ½)βπ) β βπ β πΏ (((intβπ½)βπ) β© (πΉ β π )) β β
))) |
29 | 28 | rspcv 3579 |
. . . . . . . 8
β’
(((intβπ½)βπ) β π½ β (βπ β π½ (π΄ β π β βπ β πΏ (π β© (πΉ β π )) β β
) β (π΄ β ((intβπ½)βπ) β βπ β πΏ (((intβπ½)βπ) β© (πΉ β π )) β β
))) |
30 | 23, 29 | syl 17 |
. . . . . . 7
β’ ((((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π΄ β π) β§ π β ((neiβπ½)β{π΄})) β (βπ β π½ (π΄ β π β βπ β πΏ (π β© (πΉ β π )) β β
) β (π΄ β ((intβπ½)βπ) β βπ β πΏ (((intβπ½)βπ) β© (πΉ β π )) β β
))) |
31 | 21, 30 | mpid 44 |
. . . . . 6
β’ ((((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π΄ β π) β§ π β ((neiβπ½)β{π΄})) β (βπ β π½ (π΄ β π β βπ β πΏ (π β© (πΉ β π )) β β
) β βπ β πΏ (((intβπ½)βπ) β© (πΉ β π )) β β
)) |
32 | | ssrin 4197 |
. . . . . . . 8
β’
(((intβπ½)βπ) β π β (((intβπ½)βπ) β© (πΉ β π )) β (π β© (πΉ β π ))) |
33 | | ssn0 4364 |
. . . . . . . . 9
β’
(((((intβπ½)βπ) β© (πΉ β π )) β (π β© (πΉ β π )) β§ (((intβπ½)βπ) β© (πΉ β π )) β β
) β (π β© (πΉ β π )) β β
) |
34 | 33 | ex 414 |
. . . . . . . 8
β’
((((intβπ½)βπ) β© (πΉ β π )) β (π β© (πΉ β π )) β ((((intβπ½)βπ) β© (πΉ β π )) β β
β (π β© (πΉ β π )) β β
)) |
35 | 32, 34 | syl 17 |
. . . . . . 7
β’
(((intβπ½)βπ) β π β ((((intβπ½)βπ) β© (πΉ β π )) β β
β (π β© (πΉ β π )) β β
)) |
36 | 35 | ralimdv 3163 |
. . . . . 6
β’
(((intβπ½)βπ) β π β (βπ β πΏ (((intβπ½)βπ) β© (πΉ β π )) β β
β βπ β πΏ (π β© (πΉ β π )) β β
)) |
37 | 10, 31, 36 | sylsyld 61 |
. . . . 5
β’ ((((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π΄ β π) β§ π β ((neiβπ½)β{π΄})) β (βπ β π½ (π΄ β π β βπ β πΏ (π β© (πΉ β π )) β β
) β βπ β πΏ (π β© (πΉ β π )) β β
)) |
38 | 37 | ralrimdva 3148 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π΄ β π) β (βπ β π½ (π΄ β π β βπ β πΏ (π β© (πΉ β π )) β β
) β βπ β ((neiβπ½)β{π΄})βπ β πΏ (π β© (πΉ β π )) β β
)) |
39 | | simpl1 1192 |
. . . . . . . . . 10
β’ (((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π΄ β π) β π½ β (TopOnβπ)) |
40 | 39, 3 | syl 17 |
. . . . . . . . 9
β’ (((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π΄ β π) β π½ β Top) |
41 | | opnneip 22493 |
. . . . . . . . . 10
β’ ((π½ β Top β§ π β π½ β§ π΄ β π) β π β ((neiβπ½)β{π΄})) |
42 | 41 | 3expb 1121 |
. . . . . . . . 9
β’ ((π½ β Top β§ (π β π½ β§ π΄ β π)) β π β ((neiβπ½)β{π΄})) |
43 | 40, 42 | sylan 581 |
. . . . . . . 8
β’ ((((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π΄ β π) β§ (π β π½ β§ π΄ β π)) β π β ((neiβπ½)β{π΄})) |
44 | | ineq1 4169 |
. . . . . . . . . . 11
β’ (π = π β (π β© (πΉ β π )) = (π β© (πΉ β π ))) |
45 | 44 | neeq1d 3000 |
. . . . . . . . . 10
β’ (π = π β ((π β© (πΉ β π )) β β
β (π β© (πΉ β π )) β β
)) |
46 | 45 | ralbidv 3171 |
. . . . . . . . 9
β’ (π = π β (βπ β πΏ (π β© (πΉ β π )) β β
β βπ β πΏ (π β© (πΉ β π )) β β
)) |
47 | 46 | rspcv 3579 |
. . . . . . . 8
β’ (π β ((neiβπ½)β{π΄}) β (βπ β ((neiβπ½)β{π΄})βπ β πΏ (π β© (πΉ β π )) β β
β βπ β πΏ (π β© (πΉ β π )) β β
)) |
48 | 43, 47 | syl 17 |
. . . . . . 7
β’ ((((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π΄ β π) β§ (π β π½ β§ π΄ β π)) β (βπ β ((neiβπ½)β{π΄})βπ β πΏ (π β© (πΉ β π )) β β
β βπ β πΏ (π β© (πΉ β π )) β β
)) |
49 | 48 | expr 458 |
. . . . . 6
β’ ((((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π΄ β π) β§ π β π½) β (π΄ β π β (βπ β ((neiβπ½)β{π΄})βπ β πΏ (π β© (πΉ β π )) β β
β βπ β πΏ (π β© (πΉ β π )) β β
))) |
50 | 49 | com23 86 |
. . . . 5
β’ ((((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π΄ β π) β§ π β π½) β (βπ β ((neiβπ½)β{π΄})βπ β πΏ (π β© (πΉ β π )) β β
β (π΄ β π β βπ β πΏ (π β© (πΉ β π )) β β
))) |
51 | 50 | ralrimdva 3148 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π΄ β π) β (βπ β ((neiβπ½)β{π΄})βπ β πΏ (π β© (πΉ β π )) β β
β βπ β π½ (π΄ β π β βπ β πΏ (π β© (πΉ β π )) β β
))) |
52 | 38, 51 | impbid 211 |
. . 3
β’ (((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π΄ β π) β (βπ β π½ (π΄ β π β βπ β πΏ (π β© (πΉ β π )) β β
) β βπ β ((neiβπ½)β{π΄})βπ β πΏ (π β© (πΉ β π )) β β
)) |
53 | 52 | pm5.32da 580 |
. 2
β’ ((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β ((π΄ β π β§ βπ β π½ (π΄ β π β βπ β πΏ (π β© (πΉ β π )) β β
)) β (π΄ β π β§ βπ β ((neiβπ½)β{π΄})βπ β πΏ (π β© (πΉ β π )) β β
))) |
54 | 1, 53 | bitrd 279 |
1
β’ ((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β (π΄ β ((π½ fClusf πΏ)βπΉ) β (π΄ β π β§ βπ β ((neiβπ½)β{π΄})βπ β πΏ (π β© (πΉ β π )) β β
))) |