Step | Hyp | Ref
| Expression |
1 | | anass 467 |
. 2
β’ ((((π½ β Top β§ πΉ β βͺ ran Fil) β§ πΉ β π« π) β§ (π΄ β π β§ ((neiβπ½)β{π΄}) β πΉ)) β ((π½ β Top β§ πΉ β βͺ ran
Fil) β§ (πΉ β
π« π β§ (π΄ β π β§ ((neiβπ½)β{π΄}) β πΉ)))) |
2 | | df-3an 1087 |
. . 3
β’ ((π½ β Top β§ πΉ β βͺ ran Fil β§ πΉ β π« π) β ((π½ β Top β§ πΉ β βͺ ran
Fil) β§ πΉ β
π« π)) |
3 | 2 | anbi1i 622 |
. 2
β’ (((π½ β Top β§ πΉ β βͺ ran Fil β§ πΉ β π« π) β§ (π΄ β π β§ ((neiβπ½)β{π΄}) β πΉ)) β (((π½ β Top β§ πΉ β βͺ ran
Fil) β§ πΉ β
π« π) β§ (π΄ β π β§ ((neiβπ½)β{π΄}) β πΉ))) |
4 | | df-flim 23663 |
. . . 4
β’ fLim =
(π β Top, π β βͺ ran Fil β¦ {π₯ β βͺ π β£ (((neiβπ)β{π₯}) β π β§ π β π« βͺ π)}) |
5 | 4 | elmpocl 7650 |
. . 3
β’ (π΄ β (π½ fLim πΉ) β (π½ β Top β§ πΉ β βͺ ran
Fil)) |
6 | | flimval.1 |
. . . . . 6
β’ π = βͺ
π½ |
7 | 6 | flimval 23687 |
. . . . 5
β’ ((π½ β Top β§ πΉ β βͺ ran Fil) β (π½ fLim πΉ) = {π₯ β π β£ (((neiβπ½)β{π₯}) β πΉ β§ πΉ β π« π)}) |
8 | 7 | eleq2d 2817 |
. . . 4
β’ ((π½ β Top β§ πΉ β βͺ ran Fil) β (π΄ β (π½ fLim πΉ) β π΄ β {π₯ β π β£ (((neiβπ½)β{π₯}) β πΉ β§ πΉ β π« π)})) |
9 | | sneq 4637 |
. . . . . . . . . 10
β’ (π₯ = π΄ β {π₯} = {π΄}) |
10 | 9 | fveq2d 6894 |
. . . . . . . . 9
β’ (π₯ = π΄ β ((neiβπ½)β{π₯}) = ((neiβπ½)β{π΄})) |
11 | 10 | sseq1d 4012 |
. . . . . . . 8
β’ (π₯ = π΄ β (((neiβπ½)β{π₯}) β πΉ β ((neiβπ½)β{π΄}) β πΉ)) |
12 | 11 | anbi1d 628 |
. . . . . . 7
β’ (π₯ = π΄ β ((((neiβπ½)β{π₯}) β πΉ β§ πΉ β π« π) β (((neiβπ½)β{π΄}) β πΉ β§ πΉ β π« π))) |
13 | 12 | biancomd 462 |
. . . . . 6
β’ (π₯ = π΄ β ((((neiβπ½)β{π₯}) β πΉ β§ πΉ β π« π) β (πΉ β π« π β§ ((neiβπ½)β{π΄}) β πΉ))) |
14 | 13 | elrab 3682 |
. . . . 5
β’ (π΄ β {π₯ β π β£ (((neiβπ½)β{π₯}) β πΉ β§ πΉ β π« π)} β (π΄ β π β§ (πΉ β π« π β§ ((neiβπ½)β{π΄}) β πΉ))) |
15 | | an12 641 |
. . . . 5
β’ ((π΄ β π β§ (πΉ β π« π β§ ((neiβπ½)β{π΄}) β πΉ)) β (πΉ β π« π β§ (π΄ β π β§ ((neiβπ½)β{π΄}) β πΉ))) |
16 | 14, 15 | bitri 274 |
. . . 4
β’ (π΄ β {π₯ β π β£ (((neiβπ½)β{π₯}) β πΉ β§ πΉ β π« π)} β (πΉ β π« π β§ (π΄ β π β§ ((neiβπ½)β{π΄}) β πΉ))) |
17 | 8, 16 | bitrdi 286 |
. . 3
β’ ((π½ β Top β§ πΉ β βͺ ran Fil) β (π΄ β (π½ fLim πΉ) β (πΉ β π« π β§ (π΄ β π β§ ((neiβπ½)β{π΄}) β πΉ)))) |
18 | 5, 17 | biadanii 818 |
. 2
β’ (π΄ β (π½ fLim πΉ) β ((π½ β Top β§ πΉ β βͺ ran
Fil) β§ (πΉ β
π« π β§ (π΄ β π β§ ((neiβπ½)β{π΄}) β πΉ)))) |
19 | 1, 3, 18 | 3bitr4ri 303 |
1
β’ (π΄ β (π½ fLim πΉ) β ((π½ β Top β§ πΉ β βͺ ran Fil
β§ πΉ β π«
π) β§ (π΄ β π β§ ((neiβπ½)β{π΄}) β πΉ))) |