Step | Hyp | Ref
| Expression |
1 | | cnpf2 22975 |
. . . . 5
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β πΉ:πβΆπ) |
2 | 1 | 3expa 1117 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β πΉ:πβΆπ) |
3 | 2 | 3adantl3 1167 |
. . 3
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β πΉ:πβΆπ) |
4 | | simpl1 1190 |
. . . . 5
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β π½ β (TopOnβπ)) |
5 | | simpl3 1192 |
. . . . 5
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β π΄ β π) |
6 | | neiflim 23699 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ π΄ β π) β π΄ β (π½ fLim ((neiβπ½)β{π΄}))) |
7 | | cnpflf2.3 |
. . . . . . 7
β’ πΏ = ((neiβπ½)β{π΄}) |
8 | 7 | oveq2i 7423 |
. . . . . 6
β’ (π½ fLim πΏ) = (π½ fLim ((neiβπ½)β{π΄})) |
9 | 6, 8 | eleqtrrdi 2843 |
. . . . 5
β’ ((π½ β (TopOnβπ) β§ π΄ β π) β π΄ β (π½ fLim πΏ)) |
10 | 4, 5, 9 | syl2anc 583 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β π΄ β (π½ fLim πΏ)) |
11 | | simpr 484 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β πΉ β ((π½ CnP πΎ)βπ΄)) |
12 | | cnpflfi 23724 |
. . . 4
β’ ((π΄ β (π½ fLim πΏ) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β (πΉβπ΄) β ((πΎ fLimf πΏ)βπΉ)) |
13 | 10, 11, 12 | syl2anc 583 |
. . 3
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β (πΉβπ΄) β ((πΎ fLimf πΏ)βπΉ)) |
14 | 3, 13 | jca 511 |
. 2
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β (πΉ:πβΆπ β§ (πΉβπ΄) β ((πΎ fLimf πΏ)βπΉ))) |
15 | | simpl1 1190 |
. . . . . . . . . . . 12
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β π½ β (TopOnβπ)) |
16 | | topontop 22636 |
. . . . . . . . . . . 12
β’ (π½ β (TopOnβπ) β π½ β Top) |
17 | 15, 16 | syl 17 |
. . . . . . . . . . 11
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β π½ β Top) |
18 | | simpl3 1192 |
. . . . . . . . . . . 12
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β π΄ β π) |
19 | | toponuni 22637 |
. . . . . . . . . . . . 13
β’ (π½ β (TopOnβπ) β π = βͺ π½) |
20 | 15, 19 | syl 17 |
. . . . . . . . . . . 12
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β π = βͺ π½) |
21 | 18, 20 | eleqtrd 2834 |
. . . . . . . . . . 11
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β π΄ β βͺ π½) |
22 | 7 | eleq2i 2824 |
. . . . . . . . . . . 12
β’ (π§ β πΏ β π§ β ((neiβπ½)β{π΄})) |
23 | | eqid 2731 |
. . . . . . . . . . . . 13
β’ βͺ π½ =
βͺ π½ |
24 | 23 | isneip 22830 |
. . . . . . . . . . . 12
β’ ((π½ β Top β§ π΄ β βͺ π½)
β (π§ β
((neiβπ½)β{π΄}) β (π§ β βͺ π½ β§ βπ£ β π½ (π΄ β π£ β§ π£ β π§)))) |
25 | 22, 24 | bitrid 283 |
. . . . . . . . . . 11
β’ ((π½ β Top β§ π΄ β βͺ π½)
β (π§ β πΏ β (π§ β βͺ π½ β§ βπ£ β π½ (π΄ β π£ β§ π£ β π§)))) |
26 | 17, 21, 25 | syl2anc 583 |
. . . . . . . . . 10
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β (π§ β πΏ β (π§ β βͺ π½ β§ βπ£ β π½ (π΄ β π£ β§ π£ β π§)))) |
27 | | sstr2 3989 |
. . . . . . . . . . . . . . 15
β’ ((πΉ β π£) β (πΉ β π§) β ((πΉ β π§) β π’ β (πΉ β π£) β π’)) |
28 | | imass2 6101 |
. . . . . . . . . . . . . . 15
β’ (π£ β π§ β (πΉ β π£) β (πΉ β π§)) |
29 | 27, 28 | syl11 33 |
. . . . . . . . . . . . . 14
β’ ((πΉ β π§) β π’ β (π£ β π§ β (πΉ β π£) β π’)) |
30 | 29 | anim2d 611 |
. . . . . . . . . . . . 13
β’ ((πΉ β π§) β π’ β ((π΄ β π£ β§ π£ β π§) β (π΄ β π£ β§ (πΉ β π£) β π’))) |
31 | 30 | reximdv 3169 |
. . . . . . . . . . . 12
β’ ((πΉ β π§) β π’ β (βπ£ β π½ (π΄ β π£ β§ π£ β π§) β βπ£ β π½ (π΄ β π£ β§ (πΉ β π£) β π’))) |
32 | 31 | com12 32 |
. . . . . . . . . . 11
β’
(βπ£ β
π½ (π΄ β π£ β§ π£ β π§) β ((πΉ β π§) β π’ β βπ£ β π½ (π΄ β π£ β§ (πΉ β π£) β π’))) |
33 | 32 | adantl 481 |
. . . . . . . . . 10
β’ ((π§ β βͺ π½
β§ βπ£ β π½ (π΄ β π£ β§ π£ β π§)) β ((πΉ β π§) β π’ β βπ£ β π½ (π΄ β π£ β§ (πΉ β π£) β π’))) |
34 | 26, 33 | syl6bi 253 |
. . . . . . . . 9
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β (π§ β πΏ β ((πΉ β π§) β π’ β βπ£ β π½ (π΄ β π£ β§ (πΉ β π£) β π’)))) |
35 | 34 | rexlimdv 3152 |
. . . . . . . 8
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β (βπ§ β πΏ (πΉ β π§) β π’ β βπ£ β π½ (π΄ β π£ β§ (πΉ β π£) β π’))) |
36 | 35 | imim2d 57 |
. . . . . . 7
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β (((πΉβπ΄) β π’ β βπ§ β πΏ (πΉ β π§) β π’) β ((πΉβπ΄) β π’ β βπ£ β π½ (π΄ β π£ β§ (πΉ β π£) β π’)))) |
37 | 36 | ralimdv 3168 |
. . . . . 6
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β (βπ’ β πΎ ((πΉβπ΄) β π’ β βπ§ β πΏ (πΉ β π§) β π’) β βπ’ β πΎ ((πΉβπ΄) β π’ β βπ£ β π½ (π΄ β π£ β§ (πΉ β π£) β π’)))) |
38 | | simpr 484 |
. . . . . 6
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β πΉ:πβΆπ) |
39 | 37, 38 | jctild 525 |
. . . . 5
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β (βπ’ β πΎ ((πΉβπ΄) β π’ β βπ§ β πΏ (πΉ β π§) β π’) β (πΉ:πβΆπ β§ βπ’ β πΎ ((πΉβπ΄) β π’ β βπ£ β π½ (π΄ β π£ β§ (πΉ β π£) β π’))))) |
40 | 39 | adantld 490 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β (((πΉβπ΄) β π β§ βπ’ β πΎ ((πΉβπ΄) β π’ β βπ§ β πΏ (πΉ β π§) β π’)) β (πΉ:πβΆπ β§ βπ’ β πΎ ((πΉβπ΄) β π’ β βπ£ β π½ (π΄ β π£ β§ (πΉ β π£) β π’))))) |
41 | | simpl2 1191 |
. . . . 5
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β πΎ β (TopOnβπ)) |
42 | 18 | snssd 4812 |
. . . . . . 7
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β {π΄} β π) |
43 | 18 | snn0d 4779 |
. . . . . . 7
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β {π΄} β β
) |
44 | | neifil 23605 |
. . . . . . 7
β’ ((π½ β (TopOnβπ) β§ {π΄} β π β§ {π΄} β β
) β ((neiβπ½)β{π΄}) β (Filβπ)) |
45 | 15, 42, 43, 44 | syl3anc 1370 |
. . . . . 6
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β ((neiβπ½)β{π΄}) β (Filβπ)) |
46 | 7, 45 | eqeltrid 2836 |
. . . . 5
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β πΏ β (Filβπ)) |
47 | | isflf 23718 |
. . . . 5
β’ ((πΎ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β ((πΉβπ΄) β ((πΎ fLimf πΏ)βπΉ) β ((πΉβπ΄) β π β§ βπ’ β πΎ ((πΉβπ΄) β π’ β βπ§ β πΏ (πΉ β π§) β π’)))) |
48 | 41, 46, 38, 47 | syl3anc 1370 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β ((πΉβπ΄) β ((πΎ fLimf πΏ)βπΉ) β ((πΉβπ΄) β π β§ βπ’ β πΎ ((πΉβπ΄) β π’ β βπ§ β πΏ (πΉ β π§) β π’)))) |
49 | | iscnp 22962 |
. . . . 5
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β (πΉ β ((π½ CnP πΎ)βπ΄) β (πΉ:πβΆπ β§ βπ’ β πΎ ((πΉβπ΄) β π’ β βπ£ β π½ (π΄ β π£ β§ (πΉ β π£) β π’))))) |
50 | 49 | adantr 480 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β (πΉ β ((π½ CnP πΎ)βπ΄) β (πΉ:πβΆπ β§ βπ’ β πΎ ((πΉβπ΄) β π’ β βπ£ β π½ (π΄ β π£ β§ (πΉ β π£) β π’))))) |
51 | 40, 48, 50 | 3imtr4d 294 |
. . 3
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β ((πΉβπ΄) β ((πΎ fLimf πΏ)βπΉ) β πΉ β ((π½ CnP πΎ)βπ΄))) |
52 | 51 | impr 454 |
. 2
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ (πΉ:πβΆπ β§ (πΉβπ΄) β ((πΎ fLimf πΏ)βπΉ))) β πΉ β ((π½ CnP πΎ)βπ΄)) |
53 | 14, 52 | impbida 798 |
1
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β (πΉ β ((π½ CnP πΎ)βπ΄) β (πΉ:πβΆπ β§ (πΉβπ΄) β ((πΎ fLimf πΏ)βπΉ)))) |