Step | Hyp | Ref
| Expression |
1 | | inss1 4228 |
. . . . . . . 8
β’ (dom
πΉ β© π΅) β dom πΉ |
2 | | ssralv 4050 |
. . . . . . . 8
β’ ((dom
πΉ β© π΅) β dom πΉ β (βπ§ β dom πΉ(π¦ β€ π§ β (absβ((πΉβπ§) β π΄)) < π₯) β βπ§ β (dom πΉ β© π΅)(π¦ β€ π§ β (absβ((πΉβπ§) β π΄)) < π₯))) |
3 | 1, 2 | ax-mp 5 |
. . . . . . 7
β’
(βπ§ β
dom πΉ(π¦ β€ π§ β (absβ((πΉβπ§) β π΄)) < π₯) β βπ§ β (dom πΉ β© π΅)(π¦ β€ π§ β (absβ((πΉβπ§) β π΄)) < π₯)) |
4 | 3 | reximi 3084 |
. . . . . 6
β’
(βπ¦ β
β βπ§ β
dom πΉ(π¦ β€ π§ β (absβ((πΉβπ§) β π΄)) < π₯) β βπ¦ β β βπ§ β (dom πΉ β© π΅)(π¦ β€ π§ β (absβ((πΉβπ§) β π΄)) < π₯)) |
5 | 4 | ralimi 3083 |
. . . . 5
β’
(βπ₯ β
β+ βπ¦ β β βπ§ β dom πΉ(π¦ β€ π§ β (absβ((πΉβπ§) β π΄)) < π₯) β βπ₯ β β+ βπ¦ β β βπ§ β (dom πΉ β© π΅)(π¦ β€ π§ β (absβ((πΉβπ§) β π΄)) < π₯)) |
6 | 5 | anim2i 617 |
. . . 4
β’ ((π΄ β β β§
βπ₯ β
β+ βπ¦ β β βπ§ β dom πΉ(π¦ β€ π§ β (absβ((πΉβπ§) β π΄)) < π₯)) β (π΄ β β β§ βπ₯ β β+
βπ¦ β β
βπ§ β (dom πΉ β© π΅)(π¦ β€ π§ β (absβ((πΉβπ§) β π΄)) < π₯))) |
7 | 6 | a1i 11 |
. . 3
β’ (πΉ βπ
π΄ β ((π΄ β β β§
βπ₯ β
β+ βπ¦ β β βπ§ β dom πΉ(π¦ β€ π§ β (absβ((πΉβπ§) β π΄)) < π₯)) β (π΄ β β β§ βπ₯ β β+
βπ¦ β β
βπ§ β (dom πΉ β© π΅)(π¦ β€ π§ β (absβ((πΉβπ§) β π΄)) < π₯)))) |
8 | | rlimf 15444 |
. . . 4
β’ (πΉ βπ
π΄ β πΉ:dom πΉβΆβ) |
9 | | rlimss 15445 |
. . . 4
β’ (πΉ βπ
π΄ β dom πΉ β
β) |
10 | | eqidd 2733 |
. . . 4
β’ ((πΉ βπ
π΄ β§ π§ β dom πΉ) β (πΉβπ§) = (πΉβπ§)) |
11 | 8, 9, 10 | rlim 15438 |
. . 3
β’ (πΉ βπ
π΄ β (πΉ βπ π΄ β (π΄ β β β§ βπ₯ β β+
βπ¦ β β
βπ§ β dom πΉ(π¦ β€ π§ β (absβ((πΉβπ§) β π΄)) < π₯)))) |
12 | | fssres 6757 |
. . . . . 6
β’ ((πΉ:dom πΉβΆβ β§ (dom πΉ β© π΅) β dom πΉ) β (πΉ βΎ (dom πΉ β© π΅)):(dom πΉ β© π΅)βΆβ) |
13 | 8, 1, 12 | sylancl 586 |
. . . . 5
β’ (πΉ βπ
π΄ β (πΉ βΎ (dom πΉ β© π΅)):(dom πΉ β© π΅)βΆβ) |
14 | | resres 5994 |
. . . . . . 7
β’ ((πΉ βΎ dom πΉ) βΎ π΅) = (πΉ βΎ (dom πΉ β© π΅)) |
15 | | ffn 6717 |
. . . . . . . . 9
β’ (πΉ:dom πΉβΆβ β πΉ Fn dom πΉ) |
16 | | fnresdm 6669 |
. . . . . . . . 9
β’ (πΉ Fn dom πΉ β (πΉ βΎ dom πΉ) = πΉ) |
17 | 8, 15, 16 | 3syl 18 |
. . . . . . . 8
β’ (πΉ βπ
π΄ β (πΉ βΎ dom πΉ) = πΉ) |
18 | 17 | reseq1d 5980 |
. . . . . . 7
β’ (πΉ βπ
π΄ β ((πΉ βΎ dom πΉ) βΎ π΅) = (πΉ βΎ π΅)) |
19 | 14, 18 | eqtr3id 2786 |
. . . . . 6
β’ (πΉ βπ
π΄ β (πΉ βΎ (dom πΉ β© π΅)) = (πΉ βΎ π΅)) |
20 | 19 | feq1d 6702 |
. . . . 5
β’ (πΉ βπ
π΄ β ((πΉ βΎ (dom πΉ β© π΅)):(dom πΉ β© π΅)βΆβ β (πΉ βΎ π΅):(dom πΉ β© π΅)βΆβ)) |
21 | 13, 20 | mpbid 231 |
. . . 4
β’ (πΉ βπ
π΄ β (πΉ βΎ π΅):(dom πΉ β© π΅)βΆβ) |
22 | 1, 9 | sstrid 3993 |
. . . 4
β’ (πΉ βπ
π΄ β (dom πΉ β© π΅) β β) |
23 | | elinel2 4196 |
. . . . . 6
β’ (π§ β (dom πΉ β© π΅) β π§ β π΅) |
24 | 23 | fvresd 6911 |
. . . . 5
β’ (π§ β (dom πΉ β© π΅) β ((πΉ βΎ π΅)βπ§) = (πΉβπ§)) |
25 | 24 | adantl 482 |
. . . 4
β’ ((πΉ βπ
π΄ β§ π§ β (dom πΉ β© π΅)) β ((πΉ βΎ π΅)βπ§) = (πΉβπ§)) |
26 | 21, 22, 25 | rlim 15438 |
. . 3
β’ (πΉ βπ
π΄ β ((πΉ βΎ π΅) βπ π΄ β (π΄ β β β§ βπ₯ β β+
βπ¦ β β
βπ§ β (dom πΉ β© π΅)(π¦ β€ π§ β (absβ((πΉβπ§) β π΄)) < π₯)))) |
27 | 7, 11, 26 | 3imtr4d 293 |
. 2
β’ (πΉ βπ
π΄ β (πΉ βπ π΄ β (πΉ βΎ π΅) βπ π΄)) |
28 | 27 | pm2.43i 52 |
1
β’ (πΉ βπ
π΄ β (πΉ βΎ π΅) βπ π΄) |