Step | Hyp | Ref
| Expression |
1 | | limcrcl 14166 |
. . . . . . 7
β’ (π₯ β (πΉ limβ π΅) β (πΉ:dom πΉβΆβ β§ dom πΉ β β β§ π΅ β β)) |
2 | 1 | simp1d 1009 |
. . . . . 6
β’ (π₯ β (πΉ limβ π΅) β πΉ:dom πΉβΆβ) |
3 | 1 | simp2d 1010 |
. . . . . 6
β’ (π₯ β (πΉ limβ π΅) β dom πΉ β β) |
4 | 1 | simp3d 1011 |
. . . . . 6
β’ (π₯ β (πΉ limβ π΅) β π΅ β β) |
5 | 2, 3, 4 | ellimc3ap 14169 |
. . . . 5
β’ (π₯ β (πΉ limβ π΅) β (π₯ β (πΉ limβ π΅) β (π₯ β β β§ βπ β β+
βπ β
β+ βπ’ β dom πΉ((π’ # π΅ β§ (absβ(π’ β π΅)) < π) β (absβ((πΉβπ’) β π₯)) < π)))) |
6 | 5 | ibi 176 |
. . . 4
β’ (π₯ β (πΉ limβ π΅) β (π₯ β β β§ βπ β β+
βπ β
β+ βπ’ β dom πΉ((π’ # π΅ β§ (absβ(π’ β π΅)) < π) β (absβ((πΉβπ’) β π₯)) < π))) |
7 | | inss1 3357 |
. . . . . . . . 9
β’ (dom
πΉ β© πΆ) β dom πΉ |
8 | | ssralv 3221 |
. . . . . . . . 9
β’ ((dom
πΉ β© πΆ) β dom πΉ β (βπ’ β dom πΉ((π’ # π΅ β§ (absβ(π’ β π΅)) < π) β (absβ((πΉβπ’) β π₯)) < π) β βπ’ β (dom πΉ β© πΆ)((π’ # π΅ β§ (absβ(π’ β π΅)) < π) β (absβ((πΉβπ’) β π₯)) < π))) |
9 | 7, 8 | ax-mp 5 |
. . . . . . . 8
β’
(βπ’ β
dom πΉ((π’ # π΅ β§ (absβ(π’ β π΅)) < π) β (absβ((πΉβπ’) β π₯)) < π) β βπ’ β (dom πΉ β© πΆ)((π’ # π΅ β§ (absβ(π’ β π΅)) < π) β (absβ((πΉβπ’) β π₯)) < π)) |
10 | | elinel2 3324 |
. . . . . . . . . . . . . . 15
β’ (π’ β (dom πΉ β© πΆ) β π’ β πΆ) |
11 | | fvres 5541 |
. . . . . . . . . . . . . . 15
β’ (π’ β πΆ β ((πΉ βΎ πΆ)βπ’) = (πΉβπ’)) |
12 | 10, 11 | syl 14 |
. . . . . . . . . . . . . 14
β’ (π’ β (dom πΉ β© πΆ) β ((πΉ βΎ πΆ)βπ’) = (πΉβπ’)) |
13 | 12 | adantl 277 |
. . . . . . . . . . . . 13
β’ ((π₯ β (πΉ limβ π΅) β§ π’ β (dom πΉ β© πΆ)) β ((πΉ βΎ πΆ)βπ’) = (πΉβπ’)) |
14 | 13 | fvoveq1d 5899 |
. . . . . . . . . . . 12
β’ ((π₯ β (πΉ limβ π΅) β§ π’ β (dom πΉ β© πΆ)) β (absβ(((πΉ βΎ πΆ)βπ’) β π₯)) = (absβ((πΉβπ’) β π₯))) |
15 | 14 | breq1d 4015 |
. . . . . . . . . . 11
β’ ((π₯ β (πΉ limβ π΅) β§ π’ β (dom πΉ β© πΆ)) β ((absβ(((πΉ βΎ πΆ)βπ’) β π₯)) < π β (absβ((πΉβπ’) β π₯)) < π)) |
16 | 15 | imbi2d 230 |
. . . . . . . . . 10
β’ ((π₯ β (πΉ limβ π΅) β§ π’ β (dom πΉ β© πΆ)) β (((π’ # π΅ β§ (absβ(π’ β π΅)) < π) β (absβ(((πΉ βΎ πΆ)βπ’) β π₯)) < π) β ((π’ # π΅ β§ (absβ(π’ β π΅)) < π) β (absβ((πΉβπ’) β π₯)) < π))) |
17 | 16 | biimprd 158 |
. . . . . . . . 9
β’ ((π₯ β (πΉ limβ π΅) β§ π’ β (dom πΉ β© πΆ)) β (((π’ # π΅ β§ (absβ(π’ β π΅)) < π) β (absβ((πΉβπ’) β π₯)) < π) β ((π’ # π΅ β§ (absβ(π’ β π΅)) < π) β (absβ(((πΉ βΎ πΆ)βπ’) β π₯)) < π))) |
18 | 17 | ralimdva 2544 |
. . . . . . . 8
β’ (π₯ β (πΉ limβ π΅) β (βπ’ β (dom πΉ β© πΆ)((π’ # π΅ β§ (absβ(π’ β π΅)) < π) β (absβ((πΉβπ’) β π₯)) < π) β βπ’ β (dom πΉ β© πΆ)((π’ # π΅ β§ (absβ(π’ β π΅)) < π) β (absβ(((πΉ βΎ πΆ)βπ’) β π₯)) < π))) |
19 | 9, 18 | syl5 32 |
. . . . . . 7
β’ (π₯ β (πΉ limβ π΅) β (βπ’ β dom πΉ((π’ # π΅ β§ (absβ(π’ β π΅)) < π) β (absβ((πΉβπ’) β π₯)) < π) β βπ’ β (dom πΉ β© πΆ)((π’ # π΅ β§ (absβ(π’ β π΅)) < π) β (absβ(((πΉ βΎ πΆ)βπ’) β π₯)) < π))) |
20 | 19 | reximdv 2578 |
. . . . . 6
β’ (π₯ β (πΉ limβ π΅) β (βπ β β+ βπ’ β dom πΉ((π’ # π΅ β§ (absβ(π’ β π΅)) < π) β (absβ((πΉβπ’) β π₯)) < π) β βπ β β+ βπ’ β (dom πΉ β© πΆ)((π’ # π΅ β§ (absβ(π’ β π΅)) < π) β (absβ(((πΉ βΎ πΆ)βπ’) β π₯)) < π))) |
21 | 20 | ralimdv 2545 |
. . . . 5
β’ (π₯ β (πΉ limβ π΅) β (βπ β β+ βπ β β+
βπ’ β dom πΉ((π’ # π΅ β§ (absβ(π’ β π΅)) < π) β (absβ((πΉβπ’) β π₯)) < π) β βπ β β+ βπ β β+
βπ’ β (dom πΉ β© πΆ)((π’ # π΅ β§ (absβ(π’ β π΅)) < π) β (absβ(((πΉ βΎ πΆ)βπ’) β π₯)) < π))) |
22 | 21 | anim2d 337 |
. . . 4
β’ (π₯ β (πΉ limβ π΅) β ((π₯ β β β§ βπ β β+
βπ β
β+ βπ’ β dom πΉ((π’ # π΅ β§ (absβ(π’ β π΅)) < π) β (absβ((πΉβπ’) β π₯)) < π)) β (π₯ β β β§ βπ β β+
βπ β
β+ βπ’ β (dom πΉ β© πΆ)((π’ # π΅ β§ (absβ(π’ β π΅)) < π) β (absβ(((πΉ βΎ πΆ)βπ’) β π₯)) < π)))) |
23 | 6, 22 | mpd 13 |
. . 3
β’ (π₯ β (πΉ limβ π΅) β (π₯ β β β§ βπ β β+
βπ β
β+ βπ’ β (dom πΉ β© πΆ)((π’ # π΅ β§ (absβ(π’ β π΅)) < π) β (absβ(((πΉ βΎ πΆ)βπ’) β π₯)) < π))) |
24 | | fresin 5396 |
. . . . 5
β’ (πΉ:dom πΉβΆβ β (πΉ βΎ πΆ):(dom πΉ β© πΆ)βΆβ) |
25 | 2, 24 | syl 14 |
. . . 4
β’ (π₯ β (πΉ limβ π΅) β (πΉ βΎ πΆ):(dom πΉ β© πΆ)βΆβ) |
26 | 7, 3 | sstrid 3168 |
. . . 4
β’ (π₯ β (πΉ limβ π΅) β (dom πΉ β© πΆ) β β) |
27 | 25, 26, 4 | ellimc3ap 14169 |
. . 3
β’ (π₯ β (πΉ limβ π΅) β (π₯ β ((πΉ βΎ πΆ) limβ π΅) β (π₯ β β β§ βπ β β+
βπ β
β+ βπ’ β (dom πΉ β© πΆ)((π’ # π΅ β§ (absβ(π’ β π΅)) < π) β (absβ(((πΉ βΎ πΆ)βπ’) β π₯)) < π)))) |
28 | 23, 27 | mpbird 167 |
. 2
β’ (π₯ β (πΉ limβ π΅) β π₯ β ((πΉ βΎ πΆ) limβ π΅)) |
29 | 28 | ssriv 3161 |
1
β’ (πΉ limβ π΅) β ((πΉ βΎ πΆ) limβ π΅) |