Step | Hyp | Ref
| Expression |
1 | | limccl 25242 |
. . 3
β’ (πΊ limβ π΅) β
β |
2 | | limccog.3 |
. . 3
β’ (π β πΆ β (πΊ limβ π΅)) |
3 | 1, 2 | sselid 3943 |
. 2
β’ (π β πΆ β β) |
4 | | limcrcl 25241 |
. . . . . . . . . . . 12
β’ (πΆ β (πΊ limβ π΅) β (πΊ:dom πΊβΆβ β§ dom πΊ β β β§ π΅ β β)) |
5 | 2, 4 | syl 17 |
. . . . . . . . . . 11
β’ (π β (πΊ:dom πΊβΆβ β§ dom πΊ β β β§ π΅ β β)) |
6 | 5 | simp1d 1143 |
. . . . . . . . . 10
β’ (π β πΊ:dom πΊβΆβ) |
7 | 5 | simp2d 1144 |
. . . . . . . . . 10
β’ (π β dom πΊ β β) |
8 | 5 | simp3d 1145 |
. . . . . . . . . 10
β’ (π β π΅ β β) |
9 | | eqid 2737 |
. . . . . . . . . 10
β’
(TopOpenββfld) =
(TopOpenββfld) |
10 | 6, 7, 8, 9 | ellimc2 25244 |
. . . . . . . . 9
β’ (π β (πΆ β (πΊ limβ π΅) β (πΆ β β β§ βπ’ β
(TopOpenββfld)(πΆ β π’ β βπ£ β
(TopOpenββfld)(π΅ β π£ β§ (πΊ β (π£ β© (dom πΊ β {π΅}))) β π’))))) |
11 | 2, 10 | mpbid 231 |
. . . . . . . 8
β’ (π β (πΆ β β β§ βπ’ β
(TopOpenββfld)(πΆ β π’ β βπ£ β
(TopOpenββfld)(π΅ β π£ β§ (πΊ β (π£ β© (dom πΊ β {π΅}))) β π’)))) |
12 | 11 | simprd 497 |
. . . . . . 7
β’ (π β βπ’ β
(TopOpenββfld)(πΆ β π’ β βπ£ β
(TopOpenββfld)(π΅ β π£ β§ (πΊ β (π£ β© (dom πΊ β {π΅}))) β π’))) |
13 | 12 | r19.21bi 3235 |
. . . . . 6
β’ ((π β§ π’ β
(TopOpenββfld)) β (πΆ β π’ β βπ£ β
(TopOpenββfld)(π΅ β π£ β§ (πΊ β (π£ β© (dom πΊ β {π΅}))) β π’))) |
14 | 13 | imp 408 |
. . . . 5
β’ (((π β§ π’ β
(TopOpenββfld)) β§ πΆ β π’) β βπ£ β
(TopOpenββfld)(π΅ β π£ β§ (πΊ β (π£ β© (dom πΊ β {π΅}))) β π’)) |
15 | | simp1ll 1237 |
. . . . . . . 8
β’ ((((π β§ π’ β
(TopOpenββfld)) β§ πΆ β π’) β§ π£ β (TopOpenββfld)
β§ (π΅ β π£ β§ (πΊ β (π£ β© (dom πΊ β {π΅}))) β π’)) β π) |
16 | | simp2 1138 |
. . . . . . . 8
β’ ((((π β§ π’ β
(TopOpenββfld)) β§ πΆ β π’) β§ π£ β (TopOpenββfld)
β§ (π΅ β π£ β§ (πΊ β (π£ β© (dom πΊ β {π΅}))) β π’)) β π£ β
(TopOpenββfld)) |
17 | | simp3l 1202 |
. . . . . . . 8
β’ ((((π β§ π’ β
(TopOpenββfld)) β§ πΆ β π’) β§ π£ β (TopOpenββfld)
β§ (π΅ β π£ β§ (πΊ β (π£ β© (dom πΊ β {π΅}))) β π’)) β π΅ β π£) |
18 | | limccog.2 |
. . . . . . . . . . . 12
β’ (π β π΅ β (πΉ limβ π΄)) |
19 | | limcrcl 25241 |
. . . . . . . . . . . . . . 15
β’ (π΅ β (πΉ limβ π΄) β (πΉ:dom πΉβΆβ β§ dom πΉ β β β§ π΄ β β)) |
20 | 18, 19 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β (πΉ:dom πΉβΆβ β§ dom πΉ β β β§ π΄ β β)) |
21 | 20 | simp1d 1143 |
. . . . . . . . . . . . 13
β’ (π β πΉ:dom πΉβΆβ) |
22 | 20 | simp2d 1144 |
. . . . . . . . . . . . 13
β’ (π β dom πΉ β β) |
23 | 20 | simp3d 1145 |
. . . . . . . . . . . . 13
β’ (π β π΄ β β) |
24 | 21, 22, 23, 9 | ellimc2 25244 |
. . . . . . . . . . . 12
β’ (π β (π΅ β (πΉ limβ π΄) β (π΅ β β β§ βπ£ β
(TopOpenββfld)(π΅ β π£ β βπ€ β
(TopOpenββfld)(π΄ β π€ β§ (πΉ β (π€ β© (dom πΉ β {π΄}))) β π£))))) |
25 | 18, 24 | mpbid 231 |
. . . . . . . . . . 11
β’ (π β (π΅ β β β§ βπ£ β
(TopOpenββfld)(π΅ β π£ β βπ€ β
(TopOpenββfld)(π΄ β π€ β§ (πΉ β (π€ β© (dom πΉ β {π΄}))) β π£)))) |
26 | 25 | simprd 497 |
. . . . . . . . . 10
β’ (π β βπ£ β
(TopOpenββfld)(π΅ β π£ β βπ€ β
(TopOpenββfld)(π΄ β π€ β§ (πΉ β (π€ β© (dom πΉ β {π΄}))) β π£))) |
27 | 26 | r19.21bi 3235 |
. . . . . . . . 9
β’ ((π β§ π£ β
(TopOpenββfld)) β (π΅ β π£ β βπ€ β
(TopOpenββfld)(π΄ β π€ β§ (πΉ β (π€ β© (dom πΉ β {π΄}))) β π£))) |
28 | 27 | imp 408 |
. . . . . . . 8
β’ (((π β§ π£ β
(TopOpenββfld)) β§ π΅ β π£) β βπ€ β
(TopOpenββfld)(π΄ β π€ β§ (πΉ β (π€ β© (dom πΉ β {π΄}))) β π£)) |
29 | 15, 16, 17, 28 | syl21anc 837 |
. . . . . . 7
β’ ((((π β§ π’ β
(TopOpenββfld)) β§ πΆ β π’) β§ π£ β (TopOpenββfld)
β§ (π΅ β π£ β§ (πΊ β (π£ β© (dom πΊ β {π΅}))) β π’)) β βπ€ β
(TopOpenββfld)(π΄ β π€ β§ (πΉ β (π€ β© (dom πΉ β {π΄}))) β π£)) |
30 | | imaco 6204 |
. . . . . . . . . . 11
β’ ((πΊ β πΉ) β (π€ β© (dom πΉ β {π΄}))) = (πΊ β (πΉ β (π€ β© (dom πΉ β {π΄})))) |
31 | 15 | ad2antrr 725 |
. . . . . . . . . . . 12
β’
((((((π β§ π’ β
(TopOpenββfld)) β§ πΆ β π’) β§ π£ β (TopOpenββfld)
β§ (π΅ β π£ β§ (πΊ β (π£ β© (dom πΊ β {π΅}))) β π’)) β§ π€ β
(TopOpenββfld)) β§ (πΉ β (π€ β© (dom πΉ β {π΄}))) β π£) β π) |
32 | | simpl3r 1230 |
. . . . . . . . . . . . 13
β’
(((((π β§ π’ β
(TopOpenββfld)) β§ πΆ β π’) β§ π£ β (TopOpenββfld)
β§ (π΅ β π£ β§ (πΊ β (π£ β© (dom πΊ β {π΅}))) β π’)) β§ π€ β
(TopOpenββfld)) β (πΊ β (π£ β© (dom πΊ β {π΅}))) β π’) |
33 | 32 | adantr 482 |
. . . . . . . . . . . 12
β’
((((((π β§ π’ β
(TopOpenββfld)) β§ πΆ β π’) β§ π£ β (TopOpenββfld)
β§ (π΅ β π£ β§ (πΊ β (π£ β© (dom πΊ β {π΅}))) β π’)) β§ π€ β
(TopOpenββfld)) β§ (πΉ β (π€ β© (dom πΉ β {π΄}))) β π£) β (πΊ β (π£ β© (dom πΊ β {π΅}))) β π’) |
34 | | simpr 486 |
. . . . . . . . . . . 12
β’
((((((π β§ π’ β
(TopOpenββfld)) β§ πΆ β π’) β§ π£ β (TopOpenββfld)
β§ (π΅ β π£ β§ (πΊ β (π£ β© (dom πΊ β {π΅}))) β π’)) β§ π€ β
(TopOpenββfld)) β§ (πΉ β (π€ β© (dom πΉ β {π΄}))) β π£) β (πΉ β (π€ β© (dom πΉ β {π΄}))) β π£) |
35 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (πΉ β (π€ β© (dom πΉ β {π΄}))) β π£) β (πΉ β (π€ β© (dom πΉ β {π΄}))) β π£) |
36 | | imassrn 6025 |
. . . . . . . . . . . . . . . . . 18
β’ (πΉ β (π€ β© (dom πΉ β {π΄}))) β ran πΉ |
37 | | limccog.1 |
. . . . . . . . . . . . . . . . . 18
β’ (π β ran πΉ β (dom πΊ β {π΅})) |
38 | 36, 37 | sstrid 3956 |
. . . . . . . . . . . . . . . . 17
β’ (π β (πΉ β (π€ β© (dom πΉ β {π΄}))) β (dom πΊ β {π΅})) |
39 | 38 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (πΉ β (π€ β© (dom πΉ β {π΄}))) β π£) β (πΉ β (π€ β© (dom πΉ β {π΄}))) β (dom πΊ β {π΅})) |
40 | 35, 39 | ssind 4193 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (πΉ β (π€ β© (dom πΉ β {π΄}))) β π£) β (πΉ β (π€ β© (dom πΉ β {π΄}))) β (π£ β© (dom πΊ β {π΅}))) |
41 | | imass2 6055 |
. . . . . . . . . . . . . . 15
β’ ((πΉ β (π€ β© (dom πΉ β {π΄}))) β (π£ β© (dom πΊ β {π΅})) β (πΊ β (πΉ β (π€ β© (dom πΉ β {π΄})))) β (πΊ β (π£ β© (dom πΊ β {π΅})))) |
42 | 40, 41 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β§ (πΉ β (π€ β© (dom πΉ β {π΄}))) β π£) β (πΊ β (πΉ β (π€ β© (dom πΉ β {π΄})))) β (πΊ β (π£ β© (dom πΊ β {π΅})))) |
43 | 42 | adantlr 714 |
. . . . . . . . . . . . 13
β’ (((π β§ (πΊ β (π£ β© (dom πΊ β {π΅}))) β π’) β§ (πΉ β (π€ β© (dom πΉ β {π΄}))) β π£) β (πΊ β (πΉ β (π€ β© (dom πΉ β {π΄})))) β (πΊ β (π£ β© (dom πΊ β {π΅})))) |
44 | | simplr 768 |
. . . . . . . . . . . . 13
β’ (((π β§ (πΊ β (π£ β© (dom πΊ β {π΅}))) β π’) β§ (πΉ β (π€ β© (dom πΉ β {π΄}))) β π£) β (πΊ β (π£ β© (dom πΊ β {π΅}))) β π’) |
45 | 43, 44 | sstrd 3955 |
. . . . . . . . . . . 12
β’ (((π β§ (πΊ β (π£ β© (dom πΊ β {π΅}))) β π’) β§ (πΉ β (π€ β© (dom πΉ β {π΄}))) β π£) β (πΊ β (πΉ β (π€ β© (dom πΉ β {π΄})))) β π’) |
46 | 31, 33, 34, 45 | syl21anc 837 |
. . . . . . . . . . 11
β’
((((((π β§ π’ β
(TopOpenββfld)) β§ πΆ β π’) β§ π£ β (TopOpenββfld)
β§ (π΅ β π£ β§ (πΊ β (π£ β© (dom πΊ β {π΅}))) β π’)) β§ π€ β
(TopOpenββfld)) β§ (πΉ β (π€ β© (dom πΉ β {π΄}))) β π£) β (πΊ β (πΉ β (π€ β© (dom πΉ β {π΄})))) β π’) |
47 | 30, 46 | eqsstrid 3993 |
. . . . . . . . . 10
β’
((((((π β§ π’ β
(TopOpenββfld)) β§ πΆ β π’) β§ π£ β (TopOpenββfld)
β§ (π΅ β π£ β§ (πΊ β (π£ β© (dom πΊ β {π΅}))) β π’)) β§ π€ β
(TopOpenββfld)) β§ (πΉ β (π€ β© (dom πΉ β {π΄}))) β π£) β ((πΊ β πΉ) β (π€ β© (dom πΉ β {π΄}))) β π’) |
48 | 47 | ex 414 |
. . . . . . . . 9
β’
(((((π β§ π’ β
(TopOpenββfld)) β§ πΆ β π’) β§ π£ β (TopOpenββfld)
β§ (π΅ β π£ β§ (πΊ β (π£ β© (dom πΊ β {π΅}))) β π’)) β§ π€ β
(TopOpenββfld)) β ((πΉ β (π€ β© (dom πΉ β {π΄}))) β π£ β ((πΊ β πΉ) β (π€ β© (dom πΉ β {π΄}))) β π’)) |
49 | 48 | anim2d 613 |
. . . . . . . 8
β’
(((((π β§ π’ β
(TopOpenββfld)) β§ πΆ β π’) β§ π£ β (TopOpenββfld)
β§ (π΅ β π£ β§ (πΊ β (π£ β© (dom πΊ β {π΅}))) β π’)) β§ π€ β
(TopOpenββfld)) β ((π΄ β π€ β§ (πΉ β (π€ β© (dom πΉ β {π΄}))) β π£) β (π΄ β π€ β§ ((πΊ β πΉ) β (π€ β© (dom πΉ β {π΄}))) β π’))) |
50 | 49 | reximdva 3166 |
. . . . . . 7
β’ ((((π β§ π’ β
(TopOpenββfld)) β§ πΆ β π’) β§ π£ β (TopOpenββfld)
β§ (π΅ β π£ β§ (πΊ β (π£ β© (dom πΊ β {π΅}))) β π’)) β (βπ€ β
(TopOpenββfld)(π΄ β π€ β§ (πΉ β (π€ β© (dom πΉ β {π΄}))) β π£) β βπ€ β
(TopOpenββfld)(π΄ β π€ β§ ((πΊ β πΉ) β (π€ β© (dom πΉ β {π΄}))) β π’))) |
51 | 29, 50 | mpd 15 |
. . . . . 6
β’ ((((π β§ π’ β
(TopOpenββfld)) β§ πΆ β π’) β§ π£ β (TopOpenββfld)
β§ (π΅ β π£ β§ (πΊ β (π£ β© (dom πΊ β {π΅}))) β π’)) β βπ€ β
(TopOpenββfld)(π΄ β π€ β§ ((πΊ β πΉ) β (π€ β© (dom πΉ β {π΄}))) β π’)) |
52 | 51 | rexlimdv3a 3157 |
. . . . 5
β’ (((π β§ π’ β
(TopOpenββfld)) β§ πΆ β π’) β (βπ£ β
(TopOpenββfld)(π΅ β π£ β§ (πΊ β (π£ β© (dom πΊ β {π΅}))) β π’) β βπ€ β
(TopOpenββfld)(π΄ β π€ β§ ((πΊ β πΉ) β (π€ β© (dom πΉ β {π΄}))) β π’))) |
53 | 14, 52 | mpd 15 |
. . . 4
β’ (((π β§ π’ β
(TopOpenββfld)) β§ πΆ β π’) β βπ€ β
(TopOpenββfld)(π΄ β π€ β§ ((πΊ β πΉ) β (π€ β© (dom πΉ β {π΄}))) β π’)) |
54 | 53 | ex 414 |
. . 3
β’ ((π β§ π’ β
(TopOpenββfld)) β (πΆ β π’ β βπ€ β
(TopOpenββfld)(π΄ β π€ β§ ((πΊ β πΉ) β (π€ β© (dom πΉ β {π΄}))) β π’))) |
55 | 54 | ralrimiva 3144 |
. 2
β’ (π β βπ’ β
(TopOpenββfld)(πΆ β π’ β βπ€ β
(TopOpenββfld)(π΄ β π€ β§ ((πΊ β πΉ) β (π€ β© (dom πΉ β {π΄}))) β π’))) |
56 | 21 | ffund 6673 |
. . . . . 6
β’ (π β Fun πΉ) |
57 | | fdmrn 6701 |
. . . . . 6
β’ (Fun
πΉ β πΉ:dom πΉβΆran πΉ) |
58 | 56, 57 | sylib 217 |
. . . . 5
β’ (π β πΉ:dom πΉβΆran πΉ) |
59 | 37 | difss2d 4095 |
. . . . 5
β’ (π β ran πΉ β dom πΊ) |
60 | 58, 59 | fssd 6687 |
. . . 4
β’ (π β πΉ:dom πΉβΆdom πΊ) |
61 | | fco 6693 |
. . . 4
β’ ((πΊ:dom πΊβΆβ β§ πΉ:dom πΉβΆdom πΊ) β (πΊ β πΉ):dom πΉβΆβ) |
62 | 6, 60, 61 | syl2anc 585 |
. . 3
β’ (π β (πΊ β πΉ):dom πΉβΆβ) |
63 | 62, 22, 23, 9 | ellimc2 25244 |
. 2
β’ (π β (πΆ β ((πΊ β πΉ) limβ π΄) β (πΆ β β β§ βπ’ β
(TopOpenββfld)(πΆ β π’ β βπ€ β
(TopOpenββfld)(π΄ β π€ β§ ((πΊ β πΉ) β (π€ β© (dom πΉ β {π΄}))) β π’))))) |
64 | 3, 55, 63 | mpbir2and 712 |
1
β’ (π β πΆ β ((πΊ β πΉ) limβ π΄)) |