Step | Hyp | Ref
| Expression |
1 | | limcco.r |
. . . . . . . . 9
β’ ((π β§ (π₯ β π΄ β§ π
β πΆ)) β π
β π΅) |
2 | 1 | expr 458 |
. . . . . . . 8
β’ ((π β§ π₯ β π΄) β (π
β πΆ β π
β π΅)) |
3 | 2 | necon1bd 2962 |
. . . . . . 7
β’ ((π β§ π₯ β π΄) β (Β¬ π
β π΅ β π
= πΆ)) |
4 | | limccl 25242 |
. . . . . . . . . 10
β’ ((π₯ β π΄ β¦ π
) limβ π) β β |
5 | | limcco.c |
. . . . . . . . . 10
β’ (π β πΆ β ((π₯ β π΄ β¦ π
) limβ π)) |
6 | 4, 5 | sselid 3943 |
. . . . . . . . 9
β’ (π β πΆ β β) |
7 | 6 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π₯ β π΄) β πΆ β β) |
8 | | elsn2g 4625 |
. . . . . . . 8
β’ (πΆ β β β (π
β {πΆ} β π
= πΆ)) |
9 | 7, 8 | syl 17 |
. . . . . . 7
β’ ((π β§ π₯ β π΄) β (π
β {πΆ} β π
= πΆ)) |
10 | 3, 9 | sylibrd 259 |
. . . . . 6
β’ ((π β§ π₯ β π΄) β (Β¬ π
β π΅ β π
β {πΆ})) |
11 | 10 | orrd 862 |
. . . . 5
β’ ((π β§ π₯ β π΄) β (π
β π΅ β¨ π
β {πΆ})) |
12 | | elun 4109 |
. . . . 5
β’ (π
β (π΅ βͺ {πΆ}) β (π
β π΅ β¨ π
β {πΆ})) |
13 | 11, 12 | sylibr 233 |
. . . 4
β’ ((π β§ π₯ β π΄) β π
β (π΅ βͺ {πΆ})) |
14 | 13 | fmpttd 7064 |
. . 3
β’ (π β (π₯ β π΄ β¦ π
):π΄βΆ(π΅ βͺ {πΆ})) |
15 | | eqid 2737 |
. . . . . 6
β’ (π¦ β π΅ β¦ π) = (π¦ β π΅ β¦ π) |
16 | | limcco.s |
. . . . . 6
β’ ((π β§ π¦ β π΅) β π β β) |
17 | 15, 16 | dmmptd 6647 |
. . . . 5
β’ (π β dom (π¦ β π΅ β¦ π) = π΅) |
18 | | limcco.d |
. . . . . . 7
β’ (π β π· β ((π¦ β π΅ β¦ π) limβ πΆ)) |
19 | | limcrcl 25241 |
. . . . . . 7
β’ (π· β ((π¦ β π΅ β¦ π) limβ πΆ) β ((π¦ β π΅ β¦ π):dom (π¦ β π΅ β¦ π)βΆβ β§ dom (π¦ β π΅ β¦ π) β β β§ πΆ β β)) |
20 | 18, 19 | syl 17 |
. . . . . 6
β’ (π β ((π¦ β π΅ β¦ π):dom (π¦ β π΅ β¦ π)βΆβ β§ dom (π¦ β π΅ β¦ π) β β β§ πΆ β β)) |
21 | 20 | simp2d 1144 |
. . . . 5
β’ (π β dom (π¦ β π΅ β¦ π) β β) |
22 | 17, 21 | eqsstrrd 3984 |
. . . 4
β’ (π β π΅ β β) |
23 | 6 | snssd 4770 |
. . . 4
β’ (π β {πΆ} β β) |
24 | 22, 23 | unssd 4147 |
. . 3
β’ (π β (π΅ βͺ {πΆ}) β β) |
25 | | eqid 2737 |
. . 3
β’
(TopOpenββfld) =
(TopOpenββfld) |
26 | | eqid 2737 |
. . 3
β’
((TopOpenββfld) βΎt (π΅ βͺ {πΆ})) = ((TopOpenββfld)
βΎt (π΅
βͺ {πΆ})) |
27 | 22, 6, 16, 26, 25 | limcmpt 25250 |
. . . 4
β’ (π β (π· β ((π¦ β π΅ β¦ π) limβ πΆ) β (π¦ β (π΅ βͺ {πΆ}) β¦ if(π¦ = πΆ, π·, π)) β
((((TopOpenββfld) βΎt (π΅ βͺ {πΆ})) CnP
(TopOpenββfld))βπΆ))) |
28 | 18, 27 | mpbid 231 |
. . 3
β’ (π β (π¦ β (π΅ βͺ {πΆ}) β¦ if(π¦ = πΆ, π·, π)) β
((((TopOpenββfld) βΎt (π΅ βͺ {πΆ})) CnP
(TopOpenββfld))βπΆ)) |
29 | 14, 24, 25, 26, 5, 28 | limccnp 25258 |
. 2
β’ (π β ((π¦ β (π΅ βͺ {πΆ}) β¦ if(π¦ = πΆ, π·, π))βπΆ) β (((π¦ β (π΅ βͺ {πΆ}) β¦ if(π¦ = πΆ, π·, π)) β (π₯ β π΄ β¦ π
)) limβ π)) |
30 | | eqid 2737 |
. . 3
β’ (π¦ β (π΅ βͺ {πΆ}) β¦ if(π¦ = πΆ, π·, π)) = (π¦ β (π΅ βͺ {πΆ}) β¦ if(π¦ = πΆ, π·, π)) |
31 | | iftrue 4493 |
. . 3
β’ (π¦ = πΆ β if(π¦ = πΆ, π·, π) = π·) |
32 | | ssun2 4134 |
. . . 4
β’ {πΆ} β (π΅ βͺ {πΆ}) |
33 | | snssg 4745 |
. . . . 5
β’ (πΆ β ((π₯ β π΄ β¦ π
) limβ π) β (πΆ β (π΅ βͺ {πΆ}) β {πΆ} β (π΅ βͺ {πΆ}))) |
34 | 5, 33 | syl 17 |
. . . 4
β’ (π β (πΆ β (π΅ βͺ {πΆ}) β {πΆ} β (π΅ βͺ {πΆ}))) |
35 | 32, 34 | mpbiri 258 |
. . 3
β’ (π β πΆ β (π΅ βͺ {πΆ})) |
36 | 30, 31, 35, 18 | fvmptd3 6972 |
. 2
β’ (π β ((π¦ β (π΅ βͺ {πΆ}) β¦ if(π¦ = πΆ, π·, π))βπΆ) = π·) |
37 | | eqidd 2738 |
. . . . 5
β’ (π β (π₯ β π΄ β¦ π
) = (π₯ β π΄ β¦ π
)) |
38 | | eqidd 2738 |
. . . . 5
β’ (π β (π¦ β (π΅ βͺ {πΆ}) β¦ if(π¦ = πΆ, π·, π)) = (π¦ β (π΅ βͺ {πΆ}) β¦ if(π¦ = πΆ, π·, π))) |
39 | | eqeq1 2741 |
. . . . . 6
β’ (π¦ = π
β (π¦ = πΆ β π
= πΆ)) |
40 | | limcco.1 |
. . . . . 6
β’ (π¦ = π
β π = π) |
41 | 39, 40 | ifbieq2d 4513 |
. . . . 5
β’ (π¦ = π
β if(π¦ = πΆ, π·, π) = if(π
= πΆ, π·, π)) |
42 | 13, 37, 38, 41 | fmptco 7076 |
. . . 4
β’ (π β ((π¦ β (π΅ βͺ {πΆ}) β¦ if(π¦ = πΆ, π·, π)) β (π₯ β π΄ β¦ π
)) = (π₯ β π΄ β¦ if(π
= πΆ, π·, π))) |
43 | | limcco.2 |
. . . . . . . 8
β’ ((π β§ (π₯ β π΄ β§ π
= πΆ)) β π = π·) |
44 | 43 | anassrs 469 |
. . . . . . 7
β’ (((π β§ π₯ β π΄) β§ π
= πΆ) β π = π·) |
45 | 44 | ifeq1da 4518 |
. . . . . 6
β’ ((π β§ π₯ β π΄) β if(π
= πΆ, π, π) = if(π
= πΆ, π·, π)) |
46 | | ifid 4527 |
. . . . . 6
β’ if(π
= πΆ, π, π) = π |
47 | 45, 46 | eqtr3di 2792 |
. . . . 5
β’ ((π β§ π₯ β π΄) β if(π
= πΆ, π·, π) = π) |
48 | 47 | mpteq2dva 5206 |
. . . 4
β’ (π β (π₯ β π΄ β¦ if(π
= πΆ, π·, π)) = (π₯ β π΄ β¦ π)) |
49 | 42, 48 | eqtrd 2777 |
. . 3
β’ (π β ((π¦ β (π΅ βͺ {πΆ}) β¦ if(π¦ = πΆ, π·, π)) β (π₯ β π΄ β¦ π
)) = (π₯ β π΄ β¦ π)) |
50 | 49 | oveq1d 7373 |
. 2
β’ (π β (((π¦ β (π΅ βͺ {πΆ}) β¦ if(π¦ = πΆ, π·, π)) β (π₯ β π΄ β¦ π
)) limβ π) = ((π₯ β π΄ β¦ π) limβ π)) |
51 | 29, 36, 50 | 3eltr3d 2852 |
1
β’ (π β π· β ((π₯ β π΄ β¦ π) limβ π)) |