Step | Hyp | Ref
| Expression |
1 | | id 19 |
. . . 4
β’ (π€ β (πΉ limβ π΅) β π€ β (πΉ limβ π΅)) |
2 | | df-limced 14128 |
. . . . . 6
β’
limβ = (π
β (β βpm β), π₯ β β β¦ {π¦ β β β£ ((π:dom πβΆβ β§ dom π β β) β§ (π₯ β β β§ βπ β β+
βπ β
β+ βπ§ β dom π((π§ # π₯ β§ (absβ(π§ β π₯)) < π) β (absβ((πβπ§) β π¦)) < π)))}) |
3 | 2 | elmpocl1 6070 |
. . . . 5
β’ (π€ β (πΉ limβ π΅) β πΉ β (β βpm
β)) |
4 | | limcrcl 14130 |
. . . . . 6
β’ (π€ β (πΉ limβ π΅) β (πΉ:dom πΉβΆβ β§ dom πΉ β β β§ π΅ β β)) |
5 | 4 | simp3d 1011 |
. . . . 5
β’ (π€ β (πΉ limβ π΅) β π΅ β β) |
6 | | cnex 7935 |
. . . . . . 7
β’ β
β V |
7 | 6 | rabex 4148 |
. . . . . 6
β’ {π¦ β β β£ ((πΉ:dom πΉβΆβ β§ dom πΉ β β) β§ (π΅ β β β§ βπ β β+
βπ β
β+ βπ§ β dom πΉ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ((πΉβπ§) β π¦)) < π)))} β V |
8 | 7 | a1i 9 |
. . . . 5
β’ (π€ β (πΉ limβ π΅) β {π¦ β β β£ ((πΉ:dom πΉβΆβ β§ dom πΉ β β) β§ (π΅ β β β§ βπ β β+
βπ β
β+ βπ§ β dom πΉ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ((πΉβπ§) β π¦)) < π)))} β V) |
9 | | simpl 109 |
. . . . . . . . . 10
β’ ((π = πΉ β§ π₯ = π΅) β π = πΉ) |
10 | 9 | dmeqd 4830 |
. . . . . . . . . 10
β’ ((π = πΉ β§ π₯ = π΅) β dom π = dom πΉ) |
11 | 9, 10 | feq12d 5356 |
. . . . . . . . 9
β’ ((π = πΉ β§ π₯ = π΅) β (π:dom πβΆβ β πΉ:dom πΉβΆβ)) |
12 | 10 | sseq1d 3185 |
. . . . . . . . 9
β’ ((π = πΉ β§ π₯ = π΅) β (dom π β β β dom πΉ β β)) |
13 | 11, 12 | anbi12d 473 |
. . . . . . . 8
β’ ((π = πΉ β§ π₯ = π΅) β ((π:dom πβΆβ β§ dom π β β) β (πΉ:dom πΉβΆβ β§ dom πΉ β β))) |
14 | | simpr 110 |
. . . . . . . . . 10
β’ ((π = πΉ β§ π₯ = π΅) β π₯ = π΅) |
15 | 14 | eleq1d 2246 |
. . . . . . . . 9
β’ ((π = πΉ β§ π₯ = π΅) β (π₯ β β β π΅ β β)) |
16 | 14 | breq2d 4016 |
. . . . . . . . . . . . . 14
β’ ((π = πΉ β§ π₯ = π΅) β (π§ # π₯ β π§ # π΅)) |
17 | 14 | oveq2d 5891 |
. . . . . . . . . . . . . . . 16
β’ ((π = πΉ β§ π₯ = π΅) β (π§ β π₯) = (π§ β π΅)) |
18 | 17 | fveq2d 5520 |
. . . . . . . . . . . . . . 15
β’ ((π = πΉ β§ π₯ = π΅) β (absβ(π§ β π₯)) = (absβ(π§ β π΅))) |
19 | 18 | breq1d 4014 |
. . . . . . . . . . . . . 14
β’ ((π = πΉ β§ π₯ = π΅) β ((absβ(π§ β π₯)) < π β (absβ(π§ β π΅)) < π)) |
20 | 16, 19 | anbi12d 473 |
. . . . . . . . . . . . 13
β’ ((π = πΉ β§ π₯ = π΅) β ((π§ # π₯ β§ (absβ(π§ β π₯)) < π) β (π§ # π΅ β§ (absβ(π§ β π΅)) < π))) |
21 | 9 | fveq1d 5518 |
. . . . . . . . . . . . . . 15
β’ ((π = πΉ β§ π₯ = π΅) β (πβπ§) = (πΉβπ§)) |
22 | 21 | fvoveq1d 5897 |
. . . . . . . . . . . . . 14
β’ ((π = πΉ β§ π₯ = π΅) β (absβ((πβπ§) β π¦)) = (absβ((πΉβπ§) β π¦))) |
23 | 22 | breq1d 4014 |
. . . . . . . . . . . . 13
β’ ((π = πΉ β§ π₯ = π΅) β ((absβ((πβπ§) β π¦)) < π β (absβ((πΉβπ§) β π¦)) < π)) |
24 | 20, 23 | imbi12d 234 |
. . . . . . . . . . . 12
β’ ((π = πΉ β§ π₯ = π΅) β (((π§ # π₯ β§ (absβ(π§ β π₯)) < π) β (absβ((πβπ§) β π¦)) < π) β ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ((πΉβπ§) β π¦)) < π))) |
25 | 10, 24 | raleqbidv 2685 |
. . . . . . . . . . 11
β’ ((π = πΉ β§ π₯ = π΅) β (βπ§ β dom π((π§ # π₯ β§ (absβ(π§ β π₯)) < π) β (absβ((πβπ§) β π¦)) < π) β βπ§ β dom πΉ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ((πΉβπ§) β π¦)) < π))) |
26 | 25 | rexbidv 2478 |
. . . . . . . . . 10
β’ ((π = πΉ β§ π₯ = π΅) β (βπ β β+ βπ§ β dom π((π§ # π₯ β§ (absβ(π§ β π₯)) < π) β (absβ((πβπ§) β π¦)) < π) β βπ β β+ βπ§ β dom πΉ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ((πΉβπ§) β π¦)) < π))) |
27 | 26 | ralbidv 2477 |
. . . . . . . . 9
β’ ((π = πΉ β§ π₯ = π΅) β (βπ β β+ βπ β β+
βπ§ β dom π((π§ # π₯ β§ (absβ(π§ β π₯)) < π) β (absβ((πβπ§) β π¦)) < π) β βπ β β+ βπ β β+
βπ§ β dom πΉ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ((πΉβπ§) β π¦)) < π))) |
28 | 15, 27 | anbi12d 473 |
. . . . . . . 8
β’ ((π = πΉ β§ π₯ = π΅) β ((π₯ β β β§ βπ β β+
βπ β
β+ βπ§ β dom π((π§ # π₯ β§ (absβ(π§ β π₯)) < π) β (absβ((πβπ§) β π¦)) < π)) β (π΅ β β β§ βπ β β+
βπ β
β+ βπ§ β dom πΉ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ((πΉβπ§) β π¦)) < π)))) |
29 | 13, 28 | anbi12d 473 |
. . . . . . 7
β’ ((π = πΉ β§ π₯ = π΅) β (((π:dom πβΆβ β§ dom π β β) β§ (π₯ β β β§ βπ β β+
βπ β
β+ βπ§ β dom π((π§ # π₯ β§ (absβ(π§ β π₯)) < π) β (absβ((πβπ§) β π¦)) < π))) β ((πΉ:dom πΉβΆβ β§ dom πΉ β β) β§ (π΅ β β β§ βπ β β+
βπ β
β+ βπ§ β dom πΉ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ((πΉβπ§) β π¦)) < π))))) |
30 | 29 | rabbidv 2727 |
. . . . . 6
β’ ((π = πΉ β§ π₯ = π΅) β {π¦ β β β£ ((π:dom πβΆβ β§ dom π β β) β§ (π₯ β β β§ βπ β β+
βπ β
β+ βπ§ β dom π((π§ # π₯ β§ (absβ(π§ β π₯)) < π) β (absβ((πβπ§) β π¦)) < π)))} = {π¦ β β β£ ((πΉ:dom πΉβΆβ β§ dom πΉ β β) β§ (π΅ β β β§ βπ β β+
βπ β
β+ βπ§ β dom πΉ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ((πΉβπ§) β π¦)) < π)))}) |
31 | 30, 2 | ovmpoga 6004 |
. . . . 5
β’ ((πΉ β (β
βpm β) β§ π΅ β β β§ {π¦ β β β£ ((πΉ:dom πΉβΆβ β§ dom πΉ β β) β§ (π΅ β β β§ βπ β β+
βπ β
β+ βπ§ β dom πΉ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ((πΉβπ§) β π¦)) < π)))} β V) β (πΉ limβ π΅) = {π¦ β β β£ ((πΉ:dom πΉβΆβ β§ dom πΉ β β) β§ (π΅ β β β§ βπ β β+
βπ β
β+ βπ§ β dom πΉ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ((πΉβπ§) β π¦)) < π)))}) |
32 | 3, 5, 8, 31 | syl3anc 1238 |
. . . 4
β’ (π€ β (πΉ limβ π΅) β (πΉ limβ π΅) = {π¦ β β β£ ((πΉ:dom πΉβΆβ β§ dom πΉ β β) β§ (π΅ β β β§ βπ β β+
βπ β
β+ βπ§ β dom πΉ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ((πΉβπ§) β π¦)) < π)))}) |
33 | 1, 32 | eleqtrd 2256 |
. . 3
β’ (π€ β (πΉ limβ π΅) β π€ β {π¦ β β β£ ((πΉ:dom πΉβΆβ β§ dom πΉ β β) β§ (π΅ β β β§ βπ β β+
βπ β
β+ βπ§ β dom πΉ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ((πΉβπ§) β π¦)) < π)))}) |
34 | | elrabi 2891 |
. . 3
β’ (π€ β {π¦ β β β£ ((πΉ:dom πΉβΆβ β§ dom πΉ β β) β§ (π΅ β β β§ βπ β β+
βπ β
β+ βπ§ β dom πΉ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ((πΉβπ§) β π¦)) < π)))} β π€ β β) |
35 | 33, 34 | syl 14 |
. 2
β’ (π€ β (πΉ limβ π΅) β π€ β β) |
36 | 35 | ssriv 3160 |
1
β’ (πΉ limβ π΅) β
β |