Step | Hyp | Ref
| Expression |
1 | | df-limc 25750 |
. . . 4
β’
limβ = (π
β (β βpm β), π₯ β β β¦ {π¦ β£
[(TopOpenββfld) / π](π§ β (dom π βͺ {π₯}) β¦ if(π§ = π₯, π¦, (πβπ§))) β (((π βΎt (dom π βͺ {π₯})) CnP π)βπ₯)}) |
2 | 1 | a1i 11 |
. . 3
β’ ((πΉ:π΄βΆβ β§ π΄ β β β§ π΅ β β) β
limβ = (π
β (β βpm β), π₯ β β β¦ {π¦ β£
[(TopOpenββfld) / π](π§ β (dom π βͺ {π₯}) β¦ if(π§ = π₯, π¦, (πβπ§))) β (((π βΎt (dom π βͺ {π₯})) CnP π)βπ₯)})) |
3 | | fvexd 6900 |
. . . . 5
β’ (((πΉ:π΄βΆβ β§ π΄ β β β§ π΅ β β) β§ (π = πΉ β§ π₯ = π΅)) β
(TopOpenββfld) β V) |
4 | | simplrl 774 |
. . . . . . . . . 10
β’ ((((πΉ:π΄βΆβ β§ π΄ β β β§ π΅ β β) β§ (π = πΉ β§ π₯ = π΅)) β§ π = (TopOpenββfld))
β π = πΉ) |
5 | 4 | dmeqd 5899 |
. . . . . . . . 9
β’ ((((πΉ:π΄βΆβ β§ π΄ β β β§ π΅ β β) β§ (π = πΉ β§ π₯ = π΅)) β§ π = (TopOpenββfld))
β dom π = dom πΉ) |
6 | | simpll1 1209 |
. . . . . . . . . 10
β’ ((((πΉ:π΄βΆβ β§ π΄ β β β§ π΅ β β) β§ (π = πΉ β§ π₯ = π΅)) β§ π = (TopOpenββfld))
β πΉ:π΄βΆβ) |
7 | 6 | fdmd 6722 |
. . . . . . . . 9
β’ ((((πΉ:π΄βΆβ β§ π΄ β β β§ π΅ β β) β§ (π = πΉ β§ π₯ = π΅)) β§ π = (TopOpenββfld))
β dom πΉ = π΄) |
8 | 5, 7 | eqtrd 2766 |
. . . . . . . 8
β’ ((((πΉ:π΄βΆβ β§ π΄ β β β§ π΅ β β) β§ (π = πΉ β§ π₯ = π΅)) β§ π = (TopOpenββfld))
β dom π = π΄) |
9 | | simplrr 775 |
. . . . . . . . 9
β’ ((((πΉ:π΄βΆβ β§ π΄ β β β§ π΅ β β) β§ (π = πΉ β§ π₯ = π΅)) β§ π = (TopOpenββfld))
β π₯ = π΅) |
10 | 9 | sneqd 4635 |
. . . . . . . 8
β’ ((((πΉ:π΄βΆβ β§ π΄ β β β§ π΅ β β) β§ (π = πΉ β§ π₯ = π΅)) β§ π = (TopOpenββfld))
β {π₯} = {π΅}) |
11 | 8, 10 | uneq12d 4159 |
. . . . . . 7
β’ ((((πΉ:π΄βΆβ β§ π΄ β β β§ π΅ β β) β§ (π = πΉ β§ π₯ = π΅)) β§ π = (TopOpenββfld))
β (dom π βͺ {π₯}) = (π΄ βͺ {π΅})) |
12 | 9 | eqeq2d 2737 |
. . . . . . . 8
β’ ((((πΉ:π΄βΆβ β§ π΄ β β β§ π΅ β β) β§ (π = πΉ β§ π₯ = π΅)) β§ π = (TopOpenββfld))
β (π§ = π₯ β π§ = π΅)) |
13 | 4 | fveq1d 6887 |
. . . . . . . 8
β’ ((((πΉ:π΄βΆβ β§ π΄ β β β§ π΅ β β) β§ (π = πΉ β§ π₯ = π΅)) β§ π = (TopOpenββfld))
β (πβπ§) = (πΉβπ§)) |
14 | 12, 13 | ifbieq2d 4549 |
. . . . . . 7
β’ ((((πΉ:π΄βΆβ β§ π΄ β β β§ π΅ β β) β§ (π = πΉ β§ π₯ = π΅)) β§ π = (TopOpenββfld))
β if(π§ = π₯, π¦, (πβπ§)) = if(π§ = π΅, π¦, (πΉβπ§))) |
15 | 11, 14 | mpteq12dv 5232 |
. . . . . 6
β’ ((((πΉ:π΄βΆβ β§ π΄ β β β§ π΅ β β) β§ (π = πΉ β§ π₯ = π΅)) β§ π = (TopOpenββfld))
β (π§ β (dom π βͺ {π₯}) β¦ if(π§ = π₯, π¦, (πβπ§))) = (π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, π¦, (πΉβπ§)))) |
16 | | simpr 484 |
. . . . . . . . . . 11
β’ ((((πΉ:π΄βΆβ β§ π΄ β β β§ π΅ β β) β§ (π = πΉ β§ π₯ = π΅)) β§ π = (TopOpenββfld))
β π =
(TopOpenββfld)) |
17 | | limcval.k |
. . . . . . . . . . 11
β’ πΎ =
(TopOpenββfld) |
18 | 16, 17 | eqtr4di 2784 |
. . . . . . . . . 10
β’ ((((πΉ:π΄βΆβ β§ π΄ β β β§ π΅ β β) β§ (π = πΉ β§ π₯ = π΅)) β§ π = (TopOpenββfld))
β π = πΎ) |
19 | 18, 11 | oveq12d 7423 |
. . . . . . . . 9
β’ ((((πΉ:π΄βΆβ β§ π΄ β β β§ π΅ β β) β§ (π = πΉ β§ π₯ = π΅)) β§ π = (TopOpenββfld))
β (π
βΎt (dom π
βͺ {π₯})) = (πΎ βΎt (π΄ βͺ {π΅}))) |
20 | | limcval.j |
. . . . . . . . 9
β’ π½ = (πΎ βΎt (π΄ βͺ {π΅})) |
21 | 19, 20 | eqtr4di 2784 |
. . . . . . . 8
β’ ((((πΉ:π΄βΆβ β§ π΄ β β β§ π΅ β β) β§ (π = πΉ β§ π₯ = π΅)) β§ π = (TopOpenββfld))
β (π
βΎt (dom π
βͺ {π₯})) = π½) |
22 | 21, 18 | oveq12d 7423 |
. . . . . . 7
β’ ((((πΉ:π΄βΆβ β§ π΄ β β β§ π΅ β β) β§ (π = πΉ β§ π₯ = π΅)) β§ π = (TopOpenββfld))
β ((π
βΎt (dom π
βͺ {π₯})) CnP π) = (π½ CnP πΎ)) |
23 | 22, 9 | fveq12d 6892 |
. . . . . 6
β’ ((((πΉ:π΄βΆβ β§ π΄ β β β§ π΅ β β) β§ (π = πΉ β§ π₯ = π΅)) β§ π = (TopOpenββfld))
β (((π
βΎt (dom π
βͺ {π₯})) CnP π)βπ₯) = ((π½ CnP πΎ)βπ΅)) |
24 | 15, 23 | eleq12d 2821 |
. . . . 5
β’ ((((πΉ:π΄βΆβ β§ π΄ β β β§ π΅ β β) β§ (π = πΉ β§ π₯ = π΅)) β§ π = (TopOpenββfld))
β ((π§ β (dom
π βͺ {π₯}) β¦ if(π§ = π₯, π¦, (πβπ§))) β (((π βΎt (dom π βͺ {π₯})) CnP π)βπ₯) β (π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, π¦, (πΉβπ§))) β ((π½ CnP πΎ)βπ΅))) |
25 | 3, 24 | sbcied 3817 |
. . . 4
β’ (((πΉ:π΄βΆβ β§ π΄ β β β§ π΅ β β) β§ (π = πΉ β§ π₯ = π΅)) β
([(TopOpenββfld) / π](π§ β (dom π βͺ {π₯}) β¦ if(π§ = π₯, π¦, (πβπ§))) β (((π βΎt (dom π βͺ {π₯})) CnP π)βπ₯) β (π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, π¦, (πΉβπ§))) β ((π½ CnP πΎ)βπ΅))) |
26 | 25 | abbidv 2795 |
. . 3
β’ (((πΉ:π΄βΆβ β§ π΄ β β β§ π΅ β β) β§ (π = πΉ β§ π₯ = π΅)) β {π¦ β£
[(TopOpenββfld) / π](π§ β (dom π βͺ {π₯}) β¦ if(π§ = π₯, π¦, (πβπ§))) β (((π βΎt (dom π βͺ {π₯})) CnP π)βπ₯)} = {π¦ β£ (π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, π¦, (πΉβπ§))) β ((π½ CnP πΎ)βπ΅)}) |
27 | | cnex 11193 |
. . . . 5
β’ β
β V |
28 | | elpm2r 8841 |
. . . . 5
β’
(((β β V β§ β β V) β§ (πΉ:π΄βΆβ β§ π΄ β β)) β πΉ β (β βpm
β)) |
29 | 27, 27, 28 | mpanl12 699 |
. . . 4
β’ ((πΉ:π΄βΆβ β§ π΄ β β) β πΉ β (β βpm
β)) |
30 | 29 | 3adant3 1129 |
. . 3
β’ ((πΉ:π΄βΆβ β§ π΄ β β β§ π΅ β β) β πΉ β (β βpm
β)) |
31 | | simp3 1135 |
. . 3
β’ ((πΉ:π΄βΆβ β§ π΄ β β β§ π΅ β β) β π΅ β β) |
32 | | eqid 2726 |
. . . . . 6
β’ (π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, π¦, (πΉβπ§))) = (π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, π¦, (πΉβπ§))) |
33 | 20, 17, 32 | limcvallem 25755 |
. . . . 5
β’ ((πΉ:π΄βΆβ β§ π΄ β β β§ π΅ β β) β ((π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, π¦, (πΉβπ§))) β ((π½ CnP πΎ)βπ΅) β π¦ β β)) |
34 | 33 | abssdv 4060 |
. . . 4
β’ ((πΉ:π΄βΆβ β§ π΄ β β β§ π΅ β β) β {π¦ β£ (π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, π¦, (πΉβπ§))) β ((π½ CnP πΎ)βπ΅)} β β) |
35 | 27 | ssex 5314 |
. . . 4
β’ ({π¦ β£ (π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, π¦, (πΉβπ§))) β ((π½ CnP πΎ)βπ΅)} β β β {π¦ β£ (π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, π¦, (πΉβπ§))) β ((π½ CnP πΎ)βπ΅)} β V) |
36 | 34, 35 | syl 17 |
. . 3
β’ ((πΉ:π΄βΆβ β§ π΄ β β β§ π΅ β β) β {π¦ β£ (π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, π¦, (πΉβπ§))) β ((π½ CnP πΎ)βπ΅)} β V) |
37 | 2, 26, 30, 31, 36 | ovmpod 7556 |
. 2
β’ ((πΉ:π΄βΆβ β§ π΄ β β β§ π΅ β β) β (πΉ limβ π΅) = {π¦ β£ (π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, π¦, (πΉβπ§))) β ((π½ CnP πΎ)βπ΅)}) |
38 | 37, 34 | eqsstrd 4015 |
. 2
β’ ((πΉ:π΄βΆβ β§ π΄ β β β§ π΅ β β) β (πΉ limβ π΅) β β) |
39 | 37, 38 | jca 511 |
1
β’ ((πΉ:π΄βΆβ β§ π΄ β β β§ π΅ β β) β ((πΉ limβ π΅) = {π¦ β£ (π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, π¦, (πΉβπ§))) β ((π½ CnP πΎ)βπ΅)} β§ (πΉ limβ π΅) β β)) |