Step | Hyp | Ref
| Expression |
1 | | isfcf 23537 |
. 2
β’ ((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β (π΄ β ((π½ fClusf πΏ)βπΉ) β (π΄ β π β§ βπ β π½ (π΄ β π β βπ β πΏ (π β© (πΉ β π )) β β
)))) |
2 | | simpll1 1212 |
. . . . . . . 8
β’ ((((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π΄ β π) β§ π β ((neiβπ½)β{π΄})) β π½ β (TopOnβπ)) |
3 | | topontop 22414 |
. . . . . . . 8
β’ (π½ β (TopOnβπ) β π½ β Top) |
4 | 2, 3 | syl 17 |
. . . . . . 7
β’ ((((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π΄ β π) β§ π β ((neiβπ½)β{π΄})) β π½ β Top) |
5 | | simpr 485 |
. . . . . . . 8
β’ ((((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π΄ β π) β§ π β ((neiβπ½)β{π΄})) β π β ((neiβπ½)β{π΄})) |
6 | | eqid 2732 |
. . . . . . . . 9
β’ βͺ π½ =
βͺ π½ |
7 | 6 | neii1 22609 |
. . . . . . . 8
β’ ((π½ β Top β§ π β ((neiβπ½)β{π΄})) β π β βͺ π½) |
8 | 4, 5, 7 | syl2anc 584 |
. . . . . . 7
β’ ((((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π΄ β π) β§ π β ((neiβπ½)β{π΄})) β π β βͺ π½) |
9 | 6 | ntrss2 22560 |
. . . . . . 7
β’ ((π½ β Top β§ π β βͺ π½)
β ((intβπ½)βπ) β π) |
10 | 4, 8, 9 | syl2anc 584 |
. . . . . 6
β’ ((((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π΄ β π) β§ π β ((neiβπ½)β{π΄})) β ((intβπ½)βπ) β π) |
11 | | simplr 767 |
. . . . . . . . . . . 12
β’ ((((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π΄ β π) β§ π β ((neiβπ½)β{π΄})) β π΄ β π) |
12 | | toponuni 22415 |
. . . . . . . . . . . . 13
β’ (π½ β (TopOnβπ) β π = βͺ π½) |
13 | 2, 12 | syl 17 |
. . . . . . . . . . . 12
β’ ((((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π΄ β π) β§ π β ((neiβπ½)β{π΄})) β π = βͺ π½) |
14 | 11, 13 | eleqtrd 2835 |
. . . . . . . . . . 11
β’ ((((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π΄ β π) β§ π β ((neiβπ½)β{π΄})) β π΄ β βͺ π½) |
15 | 14 | snssd 4812 |
. . . . . . . . . 10
β’ ((((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π΄ β π) β§ π β ((neiβπ½)β{π΄})) β {π΄} β βͺ π½) |
16 | 6 | neiint 22607 |
. . . . . . . . . 10
β’ ((π½ β Top β§ {π΄} β βͺ π½
β§ π β βͺ π½)
β (π β
((neiβπ½)β{π΄}) β {π΄} β ((intβπ½)βπ))) |
17 | 4, 15, 8, 16 | syl3anc 1371 |
. . . . . . . . 9
β’ ((((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π΄ β π) β§ π β ((neiβπ½)β{π΄})) β (π β ((neiβπ½)β{π΄}) β {π΄} β ((intβπ½)βπ))) |
18 | 5, 17 | mpbid 231 |
. . . . . . . 8
β’ ((((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π΄ β π) β§ π β ((neiβπ½)β{π΄})) β {π΄} β ((intβπ½)βπ)) |
19 | | snssg 4787 |
. . . . . . . . 9
β’ (π΄ β π β (π΄ β ((intβπ½)βπ) β {π΄} β ((intβπ½)βπ))) |
20 | 11, 19 | syl 17 |
. . . . . . . 8
β’ ((((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π΄ β π) β§ π β ((neiβπ½)β{π΄})) β (π΄ β ((intβπ½)βπ) β {π΄} β ((intβπ½)βπ))) |
21 | 18, 20 | mpbird 256 |
. . . . . . 7
β’ ((((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π΄ β π) β§ π β ((neiβπ½)β{π΄})) β π΄ β ((intβπ½)βπ)) |
22 | 6 | ntropn 22552 |
. . . . . . . . 9
β’ ((π½ β Top β§ π β βͺ π½)
β ((intβπ½)βπ) β π½) |
23 | 4, 8, 22 | syl2anc 584 |
. . . . . . . 8
β’ ((((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π΄ β π) β§ π β ((neiβπ½)β{π΄})) β ((intβπ½)βπ) β π½) |
24 | | eleq2 2822 |
. . . . . . . . . 10
β’ (π = ((intβπ½)βπ) β (π΄ β π β π΄ β ((intβπ½)βπ))) |
25 | | ineq1 4205 |
. . . . . . . . . . . 12
β’ (π = ((intβπ½)βπ) β (π β© (πΉ β π )) = (((intβπ½)βπ) β© (πΉ β π ))) |
26 | 25 | neeq1d 3000 |
. . . . . . . . . . 11
β’ (π = ((intβπ½)βπ) β ((π β© (πΉ β π )) β β
β (((intβπ½)βπ) β© (πΉ β π )) β β
)) |
27 | 26 | ralbidv 3177 |
. . . . . . . . . 10
β’ (π = ((intβπ½)βπ) β (βπ β πΏ (π β© (πΉ β π )) β β
β βπ β πΏ (((intβπ½)βπ) β© (πΉ β π )) β β
)) |
28 | 24, 27 | imbi12d 344 |
. . . . . . . . 9
β’ (π = ((intβπ½)βπ) β ((π΄ β π β βπ β πΏ (π β© (πΉ β π )) β β
) β (π΄ β ((intβπ½)βπ) β βπ β πΏ (((intβπ½)βπ) β© (πΉ β π )) β β
))) |
29 | 28 | rspcv 3608 |
. . . . . . . 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 4233 |
. . . . . . . 8
β’
(((intβπ½)βπ) β π β (((intβπ½)βπ) β© (πΉ β π )) β (π β© (πΉ β π ))) |
33 | | ssn0 4400 |
. . . . . . . . 9
β’
(((((intβπ½)βπ) β© (πΉ β π )) β (π β© (πΉ β π )) β§ (((intβπ½)βπ) β© (πΉ β π )) β β
) β (π β© (πΉ β π )) β β
) |
34 | 33 | ex 413 |
. . . . . . . 8
β’
((((intβπ½)βπ) β© (πΉ β π )) β (π β© (πΉ β π )) β ((((intβπ½)βπ) β© (πΉ β π )) β β
β (π β© (πΉ β π )) β β
)) |
35 | 32, 34 | syl 17 |
. . . . . . 7
β’
(((intβπ½)βπ) β π β ((((intβπ½)βπ) β© (πΉ β π )) β β
β (π β© (πΉ β π )) β β
)) |
36 | 35 | ralimdv 3169 |
. . . . . 6
β’
(((intβπ½)βπ) β π β (βπ β πΏ (((intβπ½)βπ) β© (πΉ β π )) β β
β βπ β πΏ (π β© (πΉ β π )) β β
)) |
37 | 10, 31, 36 | sylsyld 61 |
. . . . 5
β’ ((((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π΄ β π) β§ π β ((neiβπ½)β{π΄})) β (βπ β π½ (π΄ β π β βπ β πΏ (π β© (πΉ β π )) β β
) β βπ β πΏ (π β© (πΉ β π )) β β
)) |
38 | 37 | ralrimdva 3154 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π΄ β π) β (βπ β π½ (π΄ β π β βπ β πΏ (π β© (πΉ β π )) β β
) β βπ β ((neiβπ½)β{π΄})βπ β πΏ (π β© (πΉ β π )) β β
)) |
39 | | simpl1 1191 |
. . . . . . . . . 10
β’ (((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π΄ β π) β π½ β (TopOnβπ)) |
40 | 39, 3 | syl 17 |
. . . . . . . . 9
β’ (((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π΄ β π) β π½ β Top) |
41 | | opnneip 22622 |
. . . . . . . . . 10
β’ ((π½ β Top β§ π β π½ β§ π΄ β π) β π β ((neiβπ½)β{π΄})) |
42 | 41 | 3expb 1120 |
. . . . . . . . 9
β’ ((π½ β Top β§ (π β π½ β§ π΄ β π)) β π β ((neiβπ½)β{π΄})) |
43 | 40, 42 | sylan 580 |
. . . . . . . 8
β’ ((((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π΄ β π) β§ (π β π½ β§ π΄ β π)) β π β ((neiβπ½)β{π΄})) |
44 | | ineq1 4205 |
. . . . . . . . . . 11
β’ (π = π β (π β© (πΉ β π )) = (π β© (πΉ β π ))) |
45 | 44 | neeq1d 3000 |
. . . . . . . . . 10
β’ (π = π β ((π β© (πΉ β π )) β β
β (π β© (πΉ β π )) β β
)) |
46 | 45 | ralbidv 3177 |
. . . . . . . . 9
β’ (π = π β (βπ β πΏ (π β© (πΉ β π )) β β
β βπ β πΏ (π β© (πΉ β π )) β β
)) |
47 | 46 | rspcv 3608 |
. . . . . . . 8
β’ (π β ((neiβπ½)β{π΄}) β (βπ β ((neiβπ½)β{π΄})βπ β πΏ (π β© (πΉ β π )) β β
β βπ β πΏ (π β© (πΉ β π )) β β
)) |
48 | 43, 47 | syl 17 |
. . . . . . 7
β’ ((((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π΄ β π) β§ (π β π½ β§ π΄ β π)) β (βπ β ((neiβπ½)β{π΄})βπ β πΏ (π β© (πΉ β π )) β β
β βπ β πΏ (π β© (πΉ β π )) β β
)) |
49 | 48 | expr 457 |
. . . . . 6
β’ ((((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π΄ β π) β§ π β π½) β (π΄ β π β (βπ β ((neiβπ½)β{π΄})βπ β πΏ (π β© (πΉ β π )) β β
β βπ β πΏ (π β© (πΉ β π )) β β
))) |
50 | 49 | com23 86 |
. . . . 5
β’ ((((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π΄ β π) β§ π β π½) β (βπ β ((neiβπ½)β{π΄})βπ β πΏ (π β© (πΉ β π )) β β
β (π΄ β π β βπ β πΏ (π β© (πΉ β π )) β β
))) |
51 | 50 | ralrimdva 3154 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π΄ β π) β (βπ β ((neiβπ½)β{π΄})βπ β πΏ (π β© (πΉ β π )) β β
β βπ β π½ (π΄ β π β βπ β πΏ (π β© (πΉ β π )) β β
))) |
52 | 38, 51 | impbid 211 |
. . 3
β’ (((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π΄ β π) β (βπ β π½ (π΄ β π β βπ β πΏ (π β© (πΉ β π )) β β
) β βπ β ((neiβπ½)β{π΄})βπ β πΏ (π β© (πΉ β π )) β β
)) |
53 | 52 | pm5.32da 579 |
. 2
β’ ((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β ((π΄ β π β§ βπ β π½ (π΄ β π β βπ β πΏ (π β© (πΉ β π )) β β
)) β (π΄ β π β§ βπ β ((neiβπ½)β{π΄})βπ β πΏ (π β© (πΉ β π )) β β
))) |
54 | 1, 53 | bitrd 278 |
1
β’ ((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β (π΄ β ((π½ fClusf πΏ)βπΉ) β (π΄ β π β§ βπ β ((neiβπ½)β{π΄})βπ β πΏ (π β© (πΉ β π )) β β
))) |