Step | Hyp | Ref
| Expression |
1 | | inss1 4192 |
. . . . . . . 8
β’ (dom
πΉ β© π΅) β dom πΉ |
2 | | ssralv 4014 |
. . . . . . . 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 618 |
. . . 4
β’ ((π΄ β β β§
βπ₯ β
β+ βπ¦ β β βπ§ β dom πΉ(π¦ β€ π§ β (absβ((πΉβπ§) β π΄)) < π₯)) β (π΄ β β β§ βπ₯ β β+
βπ¦ β β
βπ§ β (dom πΉ β© π΅)(π¦ β€ π§ β (absβ((πΉβπ§) β π΄)) < π₯))) |
7 | 6 | a1i 11 |
. . 3
β’ (πΉ βπ
π΄ β ((π΄ β β β§
βπ₯ β
β+ βπ¦ β β βπ§ β dom πΉ(π¦ β€ π§ β (absβ((πΉβπ§) β π΄)) < π₯)) β (π΄ β β β§ βπ₯ β β+
βπ¦ β β
βπ§ β (dom πΉ β© π΅)(π¦ β€ π§ β (absβ((πΉβπ§) β π΄)) < π₯)))) |
8 | | rlimf 15392 |
. . . 4
β’ (πΉ βπ
π΄ β πΉ:dom πΉβΆβ) |
9 | | rlimss 15393 |
. . . 4
β’ (πΉ βπ
π΄ β dom πΉ β
β) |
10 | | eqidd 2734 |
. . . 4
β’ ((πΉ βπ
π΄ β§ π§ β dom πΉ) β (πΉβπ§) = (πΉβπ§)) |
11 | 8, 9, 10 | rlim 15386 |
. . 3
β’ (πΉ βπ
π΄ β (πΉ βπ π΄ β (π΄ β β β§ βπ₯ β β+
βπ¦ β β
βπ§ β dom πΉ(π¦ β€ π§ β (absβ((πΉβπ§) β π΄)) < π₯)))) |
12 | | fssres 6712 |
. . . . . 6
β’ ((πΉ:dom πΉβΆβ β§ (dom πΉ β© π΅) β dom πΉ) β (πΉ βΎ (dom πΉ β© π΅)):(dom πΉ β© π΅)βΆβ) |
13 | 8, 1, 12 | sylancl 587 |
. . . . 5
β’ (πΉ βπ
π΄ β (πΉ βΎ (dom πΉ β© π΅)):(dom πΉ β© π΅)βΆβ) |
14 | | resres 5954 |
. . . . . . 7
β’ ((πΉ βΎ dom πΉ) βΎ π΅) = (πΉ βΎ (dom πΉ β© π΅)) |
15 | | ffn 6672 |
. . . . . . . . 9
β’ (πΉ:dom πΉβΆβ β πΉ Fn dom πΉ) |
16 | | fnresdm 6624 |
. . . . . . . . 9
β’ (πΉ Fn dom πΉ β (πΉ βΎ dom πΉ) = πΉ) |
17 | 8, 15, 16 | 3syl 18 |
. . . . . . . 8
β’ (πΉ βπ
π΄ β (πΉ βΎ dom πΉ) = πΉ) |
18 | 17 | reseq1d 5940 |
. . . . . . 7
β’ (πΉ βπ
π΄ β ((πΉ βΎ dom πΉ) βΎ π΅) = (πΉ βΎ π΅)) |
19 | 14, 18 | eqtr3id 2787 |
. . . . . 6
β’ (πΉ βπ
π΄ β (πΉ βΎ (dom πΉ β© π΅)) = (πΉ βΎ π΅)) |
20 | 19 | feq1d 6657 |
. . . . 5
β’ (πΉ βπ
π΄ β ((πΉ βΎ (dom πΉ β© π΅)):(dom πΉ β© π΅)βΆβ β (πΉ βΎ π΅):(dom πΉ β© π΅)βΆβ)) |
21 | 13, 20 | mpbid 231 |
. . . 4
β’ (πΉ βπ
π΄ β (πΉ βΎ π΅):(dom πΉ β© π΅)βΆβ) |
22 | 1, 9 | sstrid 3959 |
. . . 4
β’ (πΉ βπ
π΄ β (dom πΉ β© π΅) β β) |
23 | | elinel2 4160 |
. . . . . 6
β’ (π§ β (dom πΉ β© π΅) β π§ β π΅) |
24 | 23 | fvresd 6866 |
. . . . 5
β’ (π§ β (dom πΉ β© π΅) β ((πΉ βΎ π΅)βπ§) = (πΉβπ§)) |
25 | 24 | adantl 483 |
. . . 4
β’ ((πΉ βπ
π΄ β§ π§ β (dom πΉ β© π΅)) β ((πΉ βΎ π΅)βπ§) = (πΉβπ§)) |
26 | 21, 22, 25 | rlim 15386 |
. . 3
β’ (πΉ βπ
π΄ β ((πΉ βΎ π΅) βπ π΄ β (π΄ β β β§ βπ₯ β β+
βπ¦ β β
βπ§ β (dom πΉ β© π΅)(π¦ β€ π§ β (absβ((πΉβπ§) β π΄)) < π₯)))) |
27 | 7, 11, 26 | 3imtr4d 294 |
. 2
β’ (πΉ βπ
π΄ β (πΉ βπ π΄ β (πΉ βΎ π΅) βπ π΄)) |
28 | 27 | pm2.43i 52 |
1
β’ (πΉ βπ
π΄ β (πΉ βΎ π΅) βπ π΄) |