Step | Hyp | Ref
| Expression |
1 | | fcfval 23400 |
. . 3
β’ ((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β ((π½ fClusf πΏ)βπΉ) = (π½ fClus ((π FilMap πΉ)βπΏ))) |
2 | 1 | eleq2d 2824 |
. 2
β’ ((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β (π΄ β ((π½ fClusf πΏ)βπΉ) β π΄ β (π½ fClus ((π FilMap πΉ)βπΏ)))) |
3 | | simp1 1137 |
. . 3
β’ ((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β π½ β (TopOnβπ)) |
4 | | toponmax 22291 |
. . . 4
β’ (π½ β (TopOnβπ) β π β π½) |
5 | | filfbas 23215 |
. . . 4
β’ (πΏ β (Filβπ) β πΏ β (fBasβπ)) |
6 | | id 22 |
. . . 4
β’ (πΉ:πβΆπ β πΉ:πβΆπ) |
7 | | fmfil 23311 |
. . . 4
β’ ((π β π½ β§ πΏ β (fBasβπ) β§ πΉ:πβΆπ) β ((π FilMap πΉ)βπΏ) β (Filβπ)) |
8 | 4, 5, 6, 7 | syl3an 1161 |
. . 3
β’ ((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β ((π FilMap πΉ)βπΏ) β (Filβπ)) |
9 | | fclsopn 23381 |
. . 3
β’ ((π½ β (TopOnβπ) β§ ((π FilMap πΉ)βπΏ) β (Filβπ)) β (π΄ β (π½ fClus ((π FilMap πΉ)βπΏ)) β (π΄ β π β§ βπ β π½ (π΄ β π β βπ₯ β ((π FilMap πΉ)βπΏ)(π β© π₯) β β
)))) |
10 | 3, 8, 9 | syl2anc 585 |
. 2
β’ ((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β (π΄ β (π½ fClus ((π FilMap πΉ)βπΏ)) β (π΄ β π β§ βπ β π½ (π΄ β π β βπ₯ β ((π FilMap πΉ)βπΏ)(π β© π₯) β β
)))) |
11 | | simpll1 1213 |
. . . . . . . . . 10
β’ ((((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π β π½) β§ π β πΏ) β π½ β (TopOnβπ)) |
12 | 11, 4 | syl 17 |
. . . . . . . . 9
β’ ((((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π β π½) β§ π β πΏ) β π β π½) |
13 | | simpll2 1214 |
. . . . . . . . . 10
β’ ((((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π β π½) β§ π β πΏ) β πΏ β (Filβπ)) |
14 | 13, 5 | syl 17 |
. . . . . . . . 9
β’ ((((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π β π½) β§ π β πΏ) β πΏ β (fBasβπ)) |
15 | | simpll3 1215 |
. . . . . . . . 9
β’ ((((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π β π½) β§ π β πΏ) β πΉ:πβΆπ) |
16 | | simpl2 1193 |
. . . . . . . . . . . 12
β’ (((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π β π½) β πΏ β (Filβπ)) |
17 | | fgfil 23242 |
. . . . . . . . . . . 12
β’ (πΏ β (Filβπ) β (πfilGenπΏ) = πΏ) |
18 | 16, 17 | syl 17 |
. . . . . . . . . . 11
β’ (((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π β π½) β (πfilGenπΏ) = πΏ) |
19 | 18 | eleq2d 2824 |
. . . . . . . . . 10
β’ (((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π β π½) β (π β (πfilGenπΏ) β π β πΏ)) |
20 | 19 | biimpar 479 |
. . . . . . . . 9
β’ ((((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π β π½) β§ π β πΏ) β π β (πfilGenπΏ)) |
21 | | eqid 2737 |
. . . . . . . . . 10
β’ (πfilGenπΏ) = (πfilGenπΏ) |
22 | 21 | imaelfm 23318 |
. . . . . . . . 9
β’ (((π β π½ β§ πΏ β (fBasβπ) β§ πΉ:πβΆπ) β§ π β (πfilGenπΏ)) β (πΉ β π ) β ((π FilMap πΉ)βπΏ)) |
23 | 12, 14, 15, 20, 22 | syl31anc 1374 |
. . . . . . . 8
β’ ((((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π β π½) β§ π β πΏ) β (πΉ β π ) β ((π FilMap πΉ)βπΏ)) |
24 | | ineq2 4171 |
. . . . . . . . . 10
β’ (π₯ = (πΉ β π ) β (π β© π₯) = (π β© (πΉ β π ))) |
25 | 24 | neeq1d 3004 |
. . . . . . . . 9
β’ (π₯ = (πΉ β π ) β ((π β© π₯) β β
β (π β© (πΉ β π )) β β
)) |
26 | 25 | rspcv 3580 |
. . . . . . . 8
β’ ((πΉ β π ) β ((π FilMap πΉ)βπΏ) β (βπ₯ β ((π FilMap πΉ)βπΏ)(π β© π₯) β β
β (π β© (πΉ β π )) β β
)) |
27 | 23, 26 | syl 17 |
. . . . . . 7
β’ ((((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π β π½) β§ π β πΏ) β (βπ₯ β ((π FilMap πΉ)βπΏ)(π β© π₯) β β
β (π β© (πΉ β π )) β β
)) |
28 | 27 | ralrimdva 3152 |
. . . . . 6
β’ (((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π β π½) β (βπ₯ β ((π FilMap πΉ)βπΏ)(π β© π₯) β β
β βπ β πΏ (π β© (πΉ β π )) β β
)) |
29 | | elfm 23314 |
. . . . . . . . . . 11
β’ ((π β π½ β§ πΏ β (fBasβπ) β§ πΉ:πβΆπ) β (π₯ β ((π FilMap πΉ)βπΏ) β (π₯ β π β§ βπ β πΏ (πΉ β π ) β π₯))) |
30 | 4, 5, 6, 29 | syl3an 1161 |
. . . . . . . . . 10
β’ ((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β (π₯ β ((π FilMap πΉ)βπΏ) β (π₯ β π β§ βπ β πΏ (πΉ β π ) β π₯))) |
31 | 30 | adantr 482 |
. . . . . . . . 9
β’ (((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π β π½) β (π₯ β ((π FilMap πΉ)βπΏ) β (π₯ β π β§ βπ β πΏ (πΉ β π ) β π₯))) |
32 | 31 | simplbda 501 |
. . . . . . . 8
β’ ((((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π β π½) β§ π₯ β ((π FilMap πΉ)βπΏ)) β βπ β πΏ (πΉ β π ) β π₯) |
33 | | r19.29r 3120 |
. . . . . . . . . 10
β’
((βπ β
πΏ (πΉ β π ) β π₯ β§ βπ β πΏ (π β© (πΉ β π )) β β
) β βπ β πΏ ((πΉ β π ) β π₯ β§ (π β© (πΉ β π )) β β
)) |
34 | | sslin 4199 |
. . . . . . . . . . . 12
β’ ((πΉ β π ) β π₯ β (π β© (πΉ β π )) β (π β© π₯)) |
35 | | ssn0 4365 |
. . . . . . . . . . . 12
β’ (((π β© (πΉ β π )) β (π β© π₯) β§ (π β© (πΉ β π )) β β
) β (π β© π₯) β β
) |
36 | 34, 35 | sylan 581 |
. . . . . . . . . . 11
β’ (((πΉ β π ) β π₯ β§ (π β© (πΉ β π )) β β
) β (π β© π₯) β β
) |
37 | 36 | rexlimivw 3149 |
. . . . . . . . . 10
β’
(βπ β
πΏ ((πΉ β π ) β π₯ β§ (π β© (πΉ β π )) β β
) β (π β© π₯) β β
) |
38 | 33, 37 | syl 17 |
. . . . . . . . 9
β’
((βπ β
πΏ (πΉ β π ) β π₯ β§ βπ β πΏ (π β© (πΉ β π )) β β
) β (π β© π₯) β β
) |
39 | 38 | ex 414 |
. . . . . . . 8
β’
(βπ β
πΏ (πΉ β π ) β π₯ β (βπ β πΏ (π β© (πΉ β π )) β β
β (π β© π₯) β β
)) |
40 | 32, 39 | syl 17 |
. . . . . . 7
β’ ((((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π β π½) β§ π₯ β ((π FilMap πΉ)βπΏ)) β (βπ β πΏ (π β© (πΉ β π )) β β
β (π β© π₯) β β
)) |
41 | 40 | ralrimdva 3152 |
. . . . . 6
β’ (((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π β π½) β (βπ β πΏ (π β© (πΉ β π )) β β
β βπ₯ β ((π FilMap πΉ)βπΏ)(π β© π₯) β β
)) |
42 | 28, 41 | impbid 211 |
. . . . 5
β’ (((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π β π½) β (βπ₯ β ((π FilMap πΉ)βπΏ)(π β© π₯) β β
β βπ β πΏ (π β© (πΉ β π )) β β
)) |
43 | 42 | imbi2d 341 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π β π½) β ((π΄ β π β βπ₯ β ((π FilMap πΉ)βπΏ)(π β© π₯) β β
) β (π΄ β π β βπ β πΏ (π β© (πΉ β π )) β β
))) |
44 | 43 | ralbidva 3173 |
. . 3
β’ ((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β (βπ β π½ (π΄ β π β βπ₯ β ((π FilMap πΉ)βπΏ)(π β© π₯) β β
) β βπ β π½ (π΄ β π β βπ β πΏ (π β© (πΉ β π )) β β
))) |
45 | 44 | anbi2d 630 |
. 2
β’ ((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β ((π΄ β π β§ βπ β π½ (π΄ β π β βπ₯ β ((π FilMap πΉ)βπΏ)(π β© π₯) β β
)) β (π΄ β π β§ βπ β π½ (π΄ β π β βπ β πΏ (π β© (πΉ β π )) β β
)))) |
46 | 2, 10, 45 | 3bitrd 305 |
1
β’ ((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β (π΄ β ((π½ fClusf πΏ)βπΉ) β (π΄ β π β§ βπ β π½ (π΄ β π β βπ β πΏ (π β© (πΉ β π )) β β
)))) |