Step | Hyp | Ref
| Expression |
1 | | fclsbas.f |
. . . 4
β’ πΉ = (πfilGenπ΅) |
2 | | fgcl 23245 |
. . . . 5
β’ (π΅ β (fBasβπ) β (πfilGenπ΅) β (Filβπ)) |
3 | 2 | adantl 483 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ π΅ β (fBasβπ)) β (πfilGenπ΅) β (Filβπ)) |
4 | 1, 3 | eqeltrid 2842 |
. . 3
β’ ((π½ β (TopOnβπ) β§ π΅ β (fBasβπ)) β πΉ β (Filβπ)) |
5 | | fclsopn 23381 |
. . 3
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β (π΄ β (π½ fClus πΉ) β (π΄ β π β§ βπ β π½ (π΄ β π β βπ‘ β πΉ (π β© π‘) β β
)))) |
6 | 4, 5 | syldan 592 |
. 2
β’ ((π½ β (TopOnβπ) β§ π΅ β (fBasβπ)) β (π΄ β (π½ fClus πΉ) β (π΄ β π β§ βπ β π½ (π΄ β π β βπ‘ β πΉ (π β© π‘) β β
)))) |
7 | | ssfg 23239 |
. . . . . . . . . . 11
β’ (π΅ β (fBasβπ) β π΅ β (πfilGenπ΅)) |
8 | 7 | ad3antlr 730 |
. . . . . . . . . 10
β’ ((((π½ β (TopOnβπ) β§ π΅ β (fBasβπ)) β§ π΄ β π) β§ (π β π½ β§ π΄ β π)) β π΅ β (πfilGenπ΅)) |
9 | 8, 1 | sseqtrrdi 4000 |
. . . . . . . . 9
β’ ((((π½ β (TopOnβπ) β§ π΅ β (fBasβπ)) β§ π΄ β π) β§ (π β π½ β§ π΄ β π)) β π΅ β πΉ) |
10 | | ssralv 4015 |
. . . . . . . . 9
β’ (π΅ β πΉ β (βπ‘ β πΉ (π β© π‘) β β
β βπ‘ β π΅ (π β© π‘) β β
)) |
11 | 9, 10 | syl 17 |
. . . . . . . 8
β’ ((((π½ β (TopOnβπ) β§ π΅ β (fBasβπ)) β§ π΄ β π) β§ (π β π½ β§ π΄ β π)) β (βπ‘ β πΉ (π β© π‘) β β
β βπ‘ β π΅ (π β© π‘) β β
)) |
12 | | ineq2 4171 |
. . . . . . . . . 10
β’ (π‘ = π β (π β© π‘) = (π β© π )) |
13 | 12 | neeq1d 3004 |
. . . . . . . . 9
β’ (π‘ = π β ((π β© π‘) β β
β (π β© π ) β β
)) |
14 | 13 | cbvralvw 3228 |
. . . . . . . 8
β’
(βπ‘ β
π΅ (π β© π‘) β β
β βπ β π΅ (π β© π ) β β
) |
15 | 11, 14 | syl6ib 251 |
. . . . . . 7
β’ ((((π½ β (TopOnβπ) β§ π΅ β (fBasβπ)) β§ π΄ β π) β§ (π β π½ β§ π΄ β π)) β (βπ‘ β πΉ (π β© π‘) β β
β βπ β π΅ (π β© π ) β β
)) |
16 | 1 | eleq2i 2830 |
. . . . . . . . . . 11
β’ (π‘ β πΉ β π‘ β (πfilGenπ΅)) |
17 | | elfg 23238 |
. . . . . . . . . . . 12
β’ (π΅ β (fBasβπ) β (π‘ β (πfilGenπ΅) β (π‘ β π β§ βπ β π΅ π β π‘))) |
18 | 17 | ad3antlr 730 |
. . . . . . . . . . 11
β’ ((((π½ β (TopOnβπ) β§ π΅ β (fBasβπ)) β§ π΄ β π) β§ (π β π½ β§ π΄ β π)) β (π‘ β (πfilGenπ΅) β (π‘ β π β§ βπ β π΅ π β π‘))) |
19 | 16, 18 | bitrid 283 |
. . . . . . . . . 10
β’ ((((π½ β (TopOnβπ) β§ π΅ β (fBasβπ)) β§ π΄ β π) β§ (π β π½ β§ π΄ β π)) β (π‘ β πΉ β (π‘ β π β§ βπ β π΅ π β π‘))) |
20 | 19 | simplbda 501 |
. . . . . . . . 9
β’
(((((π½ β
(TopOnβπ) β§ π΅ β (fBasβπ)) β§ π΄ β π) β§ (π β π½ β§ π΄ β π)) β§ π‘ β πΉ) β βπ β π΅ π β π‘) |
21 | | r19.29r 3120 |
. . . . . . . . . . 11
β’
((βπ β
π΅ π β π‘ β§ βπ β π΅ (π β© π ) β β
) β βπ β π΅ (π β π‘ β§ (π β© π ) β β
)) |
22 | | sslin 4199 |
. . . . . . . . . . . . 13
β’ (π β π‘ β (π β© π ) β (π β© π‘)) |
23 | | ssn0 4365 |
. . . . . . . . . . . . 13
β’ (((π β© π ) β (π β© π‘) β§ (π β© π ) β β
) β (π β© π‘) β β
) |
24 | 22, 23 | sylan 581 |
. . . . . . . . . . . 12
β’ ((π β π‘ β§ (π β© π ) β β
) β (π β© π‘) β β
) |
25 | 24 | rexlimivw 3149 |
. . . . . . . . . . 11
β’
(βπ β
π΅ (π β π‘ β§ (π β© π ) β β
) β (π β© π‘) β β
) |
26 | 21, 25 | syl 17 |
. . . . . . . . . 10
β’
((βπ β
π΅ π β π‘ β§ βπ β π΅ (π β© π ) β β
) β (π β© π‘) β β
) |
27 | 26 | ex 414 |
. . . . . . . . 9
β’
(βπ β
π΅ π β π‘ β (βπ β π΅ (π β© π ) β β
β (π β© π‘) β β
)) |
28 | 20, 27 | syl 17 |
. . . . . . . 8
β’
(((((π½ β
(TopOnβπ) β§ π΅ β (fBasβπ)) β§ π΄ β π) β§ (π β π½ β§ π΄ β π)) β§ π‘ β πΉ) β (βπ β π΅ (π β© π ) β β
β (π β© π‘) β β
)) |
29 | 28 | ralrimdva 3152 |
. . . . . . 7
β’ ((((π½ β (TopOnβπ) β§ π΅ β (fBasβπ)) β§ π΄ β π) β§ (π β π½ β§ π΄ β π)) β (βπ β π΅ (π β© π ) β β
β βπ‘ β πΉ (π β© π‘) β β
)) |
30 | 15, 29 | impbid 211 |
. . . . . 6
β’ ((((π½ β (TopOnβπ) β§ π΅ β (fBasβπ)) β§ π΄ β π) β§ (π β π½ β§ π΄ β π)) β (βπ‘ β πΉ (π β© π‘) β β
β βπ β π΅ (π β© π ) β β
)) |
31 | 30 | anassrs 469 |
. . . . 5
β’
(((((π½ β
(TopOnβπ) β§ π΅ β (fBasβπ)) β§ π΄ β π) β§ π β π½) β§ π΄ β π) β (βπ‘ β πΉ (π β© π‘) β β
β βπ β π΅ (π β© π ) β β
)) |
32 | 31 | pm5.74da 803 |
. . . 4
β’ ((((π½ β (TopOnβπ) β§ π΅ β (fBasβπ)) β§ π΄ β π) β§ π β π½) β ((π΄ β π β βπ‘ β πΉ (π β© π‘) β β
) β (π΄ β π β βπ β π΅ (π β© π ) β β
))) |
33 | 32 | ralbidva 3173 |
. . 3
β’ (((π½ β (TopOnβπ) β§ π΅ β (fBasβπ)) β§ π΄ β π) β (βπ β π½ (π΄ β π β βπ‘ β πΉ (π β© π‘) β β
) β βπ β π½ (π΄ β π β βπ β π΅ (π β© π ) β β
))) |
34 | 33 | pm5.32da 580 |
. 2
β’ ((π½ β (TopOnβπ) β§ π΅ β (fBasβπ)) β ((π΄ β π β§ βπ β π½ (π΄ β π β βπ‘ β πΉ (π β© π‘) β β
)) β (π΄ β π β§ βπ β π½ (π΄ β π β βπ β π΅ (π β© π ) β β
)))) |
35 | 6, 34 | bitrd 279 |
1
β’ ((π½ β (TopOnβπ) β§ π΅ β (fBasβπ)) β (π΄ β (π½ fClus πΉ) β (π΄ β π β§ βπ β π½ (π΄ β π β βπ β π΅ (π β© π ) β β
)))) |