Step | Hyp | Ref
| Expression |
1 | | simp1l 1198 |
. . 3
β’ (((π΄ β (π½ fLim πΉ) β§ π΅ β (π½ fLim πΉ)) β§ (π β π½ β§ π β π½) β§ (π΄ β π β§ π΅ β π)) β π΄ β (π½ fLim πΉ)) |
2 | | eqid 2733 |
. . . 4
β’ βͺ π½ =
βͺ π½ |
3 | 2 | flimfil 23473 |
. . 3
β’ (π΄ β (π½ fLim πΉ) β πΉ β (Filββͺ π½)) |
4 | 1, 3 | syl 17 |
. 2
β’ (((π΄ β (π½ fLim πΉ) β§ π΅ β (π½ fLim πΉ)) β§ (π β π½ β§ π β π½) β§ (π΄ β π β§ π΅ β π)) β πΉ β (Filββͺ π½)) |
5 | | flimtop 23469 |
. . . . 5
β’ (π΄ β (π½ fLim πΉ) β π½ β Top) |
6 | 1, 5 | syl 17 |
. . . 4
β’ (((π΄ β (π½ fLim πΉ) β§ π΅ β (π½ fLim πΉ)) β§ (π β π½ β§ π β π½) β§ (π΄ β π β§ π΅ β π)) β π½ β Top) |
7 | | simp2l 1200 |
. . . 4
β’ (((π΄ β (π½ fLim πΉ) β§ π΅ β (π½ fLim πΉ)) β§ (π β π½ β§ π β π½) β§ (π΄ β π β§ π΅ β π)) β π β π½) |
8 | | simp3l 1202 |
. . . 4
β’ (((π΄ β (π½ fLim πΉ) β§ π΅ β (π½ fLim πΉ)) β§ (π β π½ β§ π β π½) β§ (π΄ β π β§ π΅ β π)) β π΄ β π) |
9 | | opnneip 22623 |
. . . 4
β’ ((π½ β Top β§ π β π½ β§ π΄ β π) β π β ((neiβπ½)β{π΄})) |
10 | 6, 7, 8, 9 | syl3anc 1372 |
. . 3
β’ (((π΄ β (π½ fLim πΉ) β§ π΅ β (π½ fLim πΉ)) β§ (π β π½ β§ π β π½) β§ (π΄ β π β§ π΅ β π)) β π β ((neiβπ½)β{π΄})) |
11 | | flimnei 23471 |
. . 3
β’ ((π΄ β (π½ fLim πΉ) β§ π β ((neiβπ½)β{π΄})) β π β πΉ) |
12 | 1, 10, 11 | syl2anc 585 |
. 2
β’ (((π΄ β (π½ fLim πΉ) β§ π΅ β (π½ fLim πΉ)) β§ (π β π½ β§ π β π½) β§ (π΄ β π β§ π΅ β π)) β π β πΉ) |
13 | | simp1r 1199 |
. . 3
β’ (((π΄ β (π½ fLim πΉ) β§ π΅ β (π½ fLim πΉ)) β§ (π β π½ β§ π β π½) β§ (π΄ β π β§ π΅ β π)) β π΅ β (π½ fLim πΉ)) |
14 | | simp2r 1201 |
. . . 4
β’ (((π΄ β (π½ fLim πΉ) β§ π΅ β (π½ fLim πΉ)) β§ (π β π½ β§ π β π½) β§ (π΄ β π β§ π΅ β π)) β π β π½) |
15 | | simp3r 1203 |
. . . 4
β’ (((π΄ β (π½ fLim πΉ) β§ π΅ β (π½ fLim πΉ)) β§ (π β π½ β§ π β π½) β§ (π΄ β π β§ π΅ β π)) β π΅ β π) |
16 | | opnneip 22623 |
. . . 4
β’ ((π½ β Top β§ π β π½ β§ π΅ β π) β π β ((neiβπ½)β{π΅})) |
17 | 6, 14, 15, 16 | syl3anc 1372 |
. . 3
β’ (((π΄ β (π½ fLim πΉ) β§ π΅ β (π½ fLim πΉ)) β§ (π β π½ β§ π β π½) β§ (π΄ β π β§ π΅ β π)) β π β ((neiβπ½)β{π΅})) |
18 | | flimnei 23471 |
. . 3
β’ ((π΅ β (π½ fLim πΉ) β§ π β ((neiβπ½)β{π΅})) β π β πΉ) |
19 | 13, 17, 18 | syl2anc 585 |
. 2
β’ (((π΄ β (π½ fLim πΉ) β§ π΅ β (π½ fLim πΉ)) β§ (π β π½ β§ π β π½) β§ (π΄ β π β§ π΅ β π)) β π β πΉ) |
20 | | filinn0 23364 |
. 2
β’ ((πΉ β (Filββͺ π½)
β§ π β πΉ β§ π β πΉ) β (π β© π) β β
) |
21 | 4, 12, 19, 20 | syl3anc 1372 |
1
β’ (((π΄ β (π½ fLim πΉ) β§ π΅ β (π½ fLim πΉ)) β§ (π β π½ β§ π β π½) β§ (π΄ β π β§ π΅ β π)) β (π β© π) β β
) |