Step | Hyp | Ref
| Expression |
1 | | limcrcl 25079 |
. . . . . 6
β’ (π₯ β ((πΉ βΎ πΆ) limβ π΅) β ((πΉ βΎ πΆ):dom (πΉ βΎ πΆ)βΆβ β§ dom (πΉ βΎ πΆ) β β β§ π΅ β β)) |
2 | 1 | simp3d 1144 |
. . . . 5
β’ (π₯ β ((πΉ βΎ πΆ) limβ π΅) β π΅ β β) |
3 | | limccl 25080 |
. . . . . 6
β’ ((πΉ βΎ πΆ) limβ π΅) β β |
4 | 3 | sseli 3922 |
. . . . 5
β’ (π₯ β ((πΉ βΎ πΆ) limβ π΅) β π₯ β β) |
5 | 2, 4 | jca 513 |
. . . 4
β’ (π₯ β ((πΉ βΎ πΆ) limβ π΅) β (π΅ β β β§ π₯ β β)) |
6 | 5 | a1i 11 |
. . 3
β’ (π β (π₯ β ((πΉ βΎ πΆ) limβ π΅) β (π΅ β β β§ π₯ β β))) |
7 | | limcrcl 25079 |
. . . . . 6
β’ (π₯ β (πΉ limβ π΅) β (πΉ:dom πΉβΆβ β§ dom πΉ β β β§ π΅ β β)) |
8 | 7 | simp3d 1144 |
. . . . 5
β’ (π₯ β (πΉ limβ π΅) β π΅ β β) |
9 | | limccl 25080 |
. . . . . 6
β’ (πΉ limβ π΅) β
β |
10 | 9 | sseli 3922 |
. . . . 5
β’ (π₯ β (πΉ limβ π΅) β π₯ β β) |
11 | 8, 10 | jca 513 |
. . . 4
β’ (π₯ β (πΉ limβ π΅) β (π΅ β β β§ π₯ β β)) |
12 | 11 | a1i 11 |
. . 3
β’ (π β (π₯ β (πΉ limβ π΅) β (π΅ β β β§ π₯ β β))) |
13 | | limcres.j |
. . . . . . . 8
β’ π½ = (πΎ βΎt (π΄ βͺ {π΅})) |
14 | | limcres.k |
. . . . . . . . . 10
β’ πΎ =
(TopOpenββfld) |
15 | 14 | cnfldtopon 23987 |
. . . . . . . . 9
β’ πΎ β
(TopOnββ) |
16 | | limcres.a |
. . . . . . . . . . 11
β’ (π β π΄ β β) |
17 | 16 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ (π΅ β β β§ π₯ β β)) β π΄ β β) |
18 | | simprl 769 |
. . . . . . . . . . 11
β’ ((π β§ (π΅ β β β§ π₯ β β)) β π΅ β β) |
19 | 18 | snssd 4748 |
. . . . . . . . . 10
β’ ((π β§ (π΅ β β β§ π₯ β β)) β {π΅} β β) |
20 | 17, 19 | unssd 4126 |
. . . . . . . . 9
β’ ((π β§ (π΅ β β β§ π₯ β β)) β (π΄ βͺ {π΅}) β β) |
21 | | resttopon 22353 |
. . . . . . . . 9
β’ ((πΎ β (TopOnββ)
β§ (π΄ βͺ {π΅}) β β) β
(πΎ βΎt
(π΄ βͺ {π΅})) β (TopOnβ(π΄ βͺ {π΅}))) |
22 | 15, 20, 21 | sylancr 588 |
. . . . . . . 8
β’ ((π β§ (π΅ β β β§ π₯ β β)) β (πΎ βΎt (π΄ βͺ {π΅})) β (TopOnβ(π΄ βͺ {π΅}))) |
23 | 13, 22 | eqeltrid 2841 |
. . . . . . 7
β’ ((π β§ (π΅ β β β§ π₯ β β)) β π½ β (TopOnβ(π΄ βͺ {π΅}))) |
24 | | topontop 22103 |
. . . . . . 7
β’ (π½ β (TopOnβ(π΄ βͺ {π΅})) β π½ β Top) |
25 | 23, 24 | syl 17 |
. . . . . 6
β’ ((π β§ (π΅ β β β§ π₯ β β)) β π½ β Top) |
26 | | limcres.c |
. . . . . . . . 9
β’ (π β πΆ β π΄) |
27 | 26 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π΅ β β β§ π₯ β β)) β πΆ β π΄) |
28 | | unss1 4119 |
. . . . . . . 8
β’ (πΆ β π΄ β (πΆ βͺ {π΅}) β (π΄ βͺ {π΅})) |
29 | 27, 28 | syl 17 |
. . . . . . 7
β’ ((π β§ (π΅ β β β§ π₯ β β)) β (πΆ βͺ {π΅}) β (π΄ βͺ {π΅})) |
30 | | toponuni 22104 |
. . . . . . . 8
β’ (π½ β (TopOnβ(π΄ βͺ {π΅})) β (π΄ βͺ {π΅}) = βͺ π½) |
31 | 23, 30 | syl 17 |
. . . . . . 7
β’ ((π β§ (π΅ β β β§ π₯ β β)) β (π΄ βͺ {π΅}) = βͺ π½) |
32 | 29, 31 | sseqtrd 3966 |
. . . . . 6
β’ ((π β§ (π΅ β β β§ π₯ β β)) β (πΆ βͺ {π΅}) β βͺ
π½) |
33 | | limcres.i |
. . . . . . 7
β’ (π β π΅ β ((intβπ½)β(πΆ βͺ {π΅}))) |
34 | 33 | adantr 482 |
. . . . . 6
β’ ((π β§ (π΅ β β β§ π₯ β β)) β π΅ β ((intβπ½)β(πΆ βͺ {π΅}))) |
35 | | elun 4089 |
. . . . . . . . 9
β’ (π§ β (π΄ βͺ {π΅}) β (π§ β π΄ β¨ π§ β {π΅})) |
36 | | simplrr 776 |
. . . . . . . . . . 11
β’ (((π β§ (π΅ β β β§ π₯ β β)) β§ π§ β π΄) β π₯ β β) |
37 | | limcres.f |
. . . . . . . . . . . . 13
β’ (π β πΉ:π΄βΆβ) |
38 | 37 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ (π΅ β β β§ π₯ β β)) β πΉ:π΄βΆβ) |
39 | 38 | ffvelcdmda 6989 |
. . . . . . . . . . 11
β’ (((π β§ (π΅ β β β§ π₯ β β)) β§ π§ β π΄) β (πΉβπ§) β β) |
40 | 36, 39 | ifcld 4511 |
. . . . . . . . . 10
β’ (((π β§ (π΅ β β β§ π₯ β β)) β§ π§ β π΄) β if(π§ = π΅, π₯, (πΉβπ§)) β β) |
41 | | elsni 4582 |
. . . . . . . . . . . . 13
β’ (π§ β {π΅} β π§ = π΅) |
42 | 41 | adantl 483 |
. . . . . . . . . . . 12
β’ (((π β§ (π΅ β β β§ π₯ β β)) β§ π§ β {π΅}) β π§ = π΅) |
43 | 42 | iftrued 4473 |
. . . . . . . . . . 11
β’ (((π β§ (π΅ β β β§ π₯ β β)) β§ π§ β {π΅}) β if(π§ = π΅, π₯, (πΉβπ§)) = π₯) |
44 | | simplrr 776 |
. . . . . . . . . . 11
β’ (((π β§ (π΅ β β β§ π₯ β β)) β§ π§ β {π΅}) β π₯ β β) |
45 | 43, 44 | eqeltrd 2837 |
. . . . . . . . . 10
β’ (((π β§ (π΅ β β β§ π₯ β β)) β§ π§ β {π΅}) β if(π§ = π΅, π₯, (πΉβπ§)) β β) |
46 | 40, 45 | jaodan 956 |
. . . . . . . . 9
β’ (((π β§ (π΅ β β β§ π₯ β β)) β§ (π§ β π΄ β¨ π§ β {π΅})) β if(π§ = π΅, π₯, (πΉβπ§)) β β) |
47 | 35, 46 | sylan2b 595 |
. . . . . . . 8
β’ (((π β§ (π΅ β β β§ π₯ β β)) β§ π§ β (π΄ βͺ {π΅})) β if(π§ = π΅, π₯, (πΉβπ§)) β β) |
48 | 47 | fmpttd 7017 |
. . . . . . 7
β’ ((π β§ (π΅ β β β§ π₯ β β)) β (π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, π₯, (πΉβπ§))):(π΄ βͺ {π΅})βΆβ) |
49 | 31 | feq2d 6612 |
. . . . . . 7
β’ ((π β§ (π΅ β β β§ π₯ β β)) β ((π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, π₯, (πΉβπ§))):(π΄ βͺ {π΅})βΆβ β (π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, π₯, (πΉβπ§))):βͺ π½βΆβ)) |
50 | 48, 49 | mpbid 232 |
. . . . . 6
β’ ((π β§ (π΅ β β β§ π₯ β β)) β (π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, π₯, (πΉβπ§))):βͺ π½βΆβ) |
51 | | eqid 2736 |
. . . . . . 7
β’ βͺ π½ =
βͺ π½ |
52 | 15 | toponunii 22106 |
. . . . . . 7
β’ β =
βͺ πΎ |
53 | 51, 52 | cnprest 22481 |
. . . . . 6
β’ (((π½ β Top β§ (πΆ βͺ {π΅}) β βͺ
π½) β§ (π΅ β ((intβπ½)β(πΆ βͺ {π΅})) β§ (π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, π₯, (πΉβπ§))):βͺ π½βΆβ)) β ((π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, π₯, (πΉβπ§))) β ((π½ CnP πΎ)βπ΅) β ((π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, π₯, (πΉβπ§))) βΎ (πΆ βͺ {π΅})) β (((π½ βΎt (πΆ βͺ {π΅})) CnP πΎ)βπ΅))) |
54 | 25, 32, 34, 50, 53 | syl22anc 837 |
. . . . 5
β’ ((π β§ (π΅ β β β§ π₯ β β)) β ((π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, π₯, (πΉβπ§))) β ((π½ CnP πΎ)βπ΅) β ((π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, π₯, (πΉβπ§))) βΎ (πΆ βͺ {π΅})) β (((π½ βΎt (πΆ βͺ {π΅})) CnP πΎ)βπ΅))) |
55 | | eqid 2736 |
. . . . . 6
β’ (π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, π₯, (πΉβπ§))) = (π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, π₯, (πΉβπ§))) |
56 | 13, 14, 55, 38, 17, 18 | ellimc 25078 |
. . . . 5
β’ ((π β§ (π΅ β β β§ π₯ β β)) β (π₯ β (πΉ limβ π΅) β (π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, π₯, (πΉβπ§))) β ((π½ CnP πΎ)βπ΅))) |
57 | | eqid 2736 |
. . . . . . 7
β’ (πΎ βΎt (πΆ βͺ {π΅})) = (πΎ βΎt (πΆ βͺ {π΅})) |
58 | | eqid 2736 |
. . . . . . 7
β’ (π§ β (πΆ βͺ {π΅}) β¦ if(π§ = π΅, π₯, ((πΉ βΎ πΆ)βπ§))) = (π§ β (πΆ βͺ {π΅}) β¦ if(π§ = π΅, π₯, ((πΉ βΎ πΆ)βπ§))) |
59 | 38, 27 | fssresd 6667 |
. . . . . . 7
β’ ((π β§ (π΅ β β β§ π₯ β β)) β (πΉ βΎ πΆ):πΆβΆβ) |
60 | 27, 17 | sstrd 3936 |
. . . . . . 7
β’ ((π β§ (π΅ β β β§ π₯ β β)) β πΆ β β) |
61 | 57, 14, 58, 59, 60, 18 | ellimc 25078 |
. . . . . 6
β’ ((π β§ (π΅ β β β§ π₯ β β)) β (π₯ β ((πΉ βΎ πΆ) limβ π΅) β (π§ β (πΆ βͺ {π΅}) β¦ if(π§ = π΅, π₯, ((πΉ βΎ πΆ)βπ§))) β (((πΎ βΎt (πΆ βͺ {π΅})) CnP πΎ)βπ΅))) |
62 | | elun 4089 |
. . . . . . . . . . 11
β’ (π§ β (πΆ βͺ {π΅}) β (π§ β πΆ β¨ π§ β {π΅})) |
63 | | velsn 4581 |
. . . . . . . . . . . 12
β’ (π§ β {π΅} β π§ = π΅) |
64 | 63 | orbi2i 911 |
. . . . . . . . . . 11
β’ ((π§ β πΆ β¨ π§ β {π΅}) β (π§ β πΆ β¨ π§ = π΅)) |
65 | 62, 64 | bitri 276 |
. . . . . . . . . 10
β’ (π§ β (πΆ βͺ {π΅}) β (π§ β πΆ β¨ π§ = π΅)) |
66 | | pm5.61 999 |
. . . . . . . . . . . 12
β’ (((π§ β πΆ β¨ π§ = π΅) β§ Β¬ π§ = π΅) β (π§ β πΆ β§ Β¬ π§ = π΅)) |
67 | | fvres 6819 |
. . . . . . . . . . . . 13
β’ (π§ β πΆ β ((πΉ βΎ πΆ)βπ§) = (πΉβπ§)) |
68 | 67 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π§ β πΆ β§ Β¬ π§ = π΅) β ((πΉ βΎ πΆ)βπ§) = (πΉβπ§)) |
69 | 66, 68 | sylbi 216 |
. . . . . . . . . . 11
β’ (((π§ β πΆ β¨ π§ = π΅) β§ Β¬ π§ = π΅) β ((πΉ βΎ πΆ)βπ§) = (πΉβπ§)) |
70 | 69 | ifeq2da 4497 |
. . . . . . . . . 10
β’ ((π§ β πΆ β¨ π§ = π΅) β if(π§ = π΅, π₯, ((πΉ βΎ πΆ)βπ§)) = if(π§ = π΅, π₯, (πΉβπ§))) |
71 | 65, 70 | sylbi 216 |
. . . . . . . . 9
β’ (π§ β (πΆ βͺ {π΅}) β if(π§ = π΅, π₯, ((πΉ βΎ πΆ)βπ§)) = if(π§ = π΅, π₯, (πΉβπ§))) |
72 | 71 | mpteq2ia 5184 |
. . . . . . . 8
β’ (π§ β (πΆ βͺ {π΅}) β¦ if(π§ = π΅, π₯, ((πΉ βΎ πΆ)βπ§))) = (π§ β (πΆ βͺ {π΅}) β¦ if(π§ = π΅, π₯, (πΉβπ§))) |
73 | 29 | resmptd 5956 |
. . . . . . . 8
β’ ((π β§ (π΅ β β β§ π₯ β β)) β ((π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, π₯, (πΉβπ§))) βΎ (πΆ βͺ {π΅})) = (π§ β (πΆ βͺ {π΅}) β¦ if(π§ = π΅, π₯, (πΉβπ§)))) |
74 | 72, 73 | eqtr4id 2795 |
. . . . . . 7
β’ ((π β§ (π΅ β β β§ π₯ β β)) β (π§ β (πΆ βͺ {π΅}) β¦ if(π§ = π΅, π₯, ((πΉ βΎ πΆ)βπ§))) = ((π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, π₯, (πΉβπ§))) βΎ (πΆ βͺ {π΅}))) |
75 | 13 | oveq1i 7313 |
. . . . . . . . . 10
β’ (π½ βΎt (πΆ βͺ {π΅})) = ((πΎ βΎt (π΄ βͺ {π΅})) βΎt (πΆ βͺ {π΅})) |
76 | | cnex 10994 |
. . . . . . . . . . . . 13
β’ β
β V |
77 | 76 | ssex 5254 |
. . . . . . . . . . . 12
β’ ((π΄ βͺ {π΅}) β β β (π΄ βͺ {π΅}) β V) |
78 | 20, 77 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ (π΅ β β β§ π₯ β β)) β (π΄ βͺ {π΅}) β V) |
79 | | restabs 22357 |
. . . . . . . . . . 11
β’ ((πΎ β (TopOnββ)
β§ (πΆ βͺ {π΅}) β (π΄ βͺ {π΅}) β§ (π΄ βͺ {π΅}) β V) β ((πΎ βΎt (π΄ βͺ {π΅})) βΎt (πΆ βͺ {π΅})) = (πΎ βΎt (πΆ βͺ {π΅}))) |
80 | 15, 29, 78, 79 | mp3an2i 1466 |
. . . . . . . . . 10
β’ ((π β§ (π΅ β β β§ π₯ β β)) β ((πΎ βΎt (π΄ βͺ {π΅})) βΎt (πΆ βͺ {π΅})) = (πΎ βΎt (πΆ βͺ {π΅}))) |
81 | 75, 80 | eqtr2id 2789 |
. . . . . . . . 9
β’ ((π β§ (π΅ β β β§ π₯ β β)) β (πΎ βΎt (πΆ βͺ {π΅})) = (π½ βΎt (πΆ βͺ {π΅}))) |
82 | 81 | oveq1d 7318 |
. . . . . . . 8
β’ ((π β§ (π΅ β β β§ π₯ β β)) β ((πΎ βΎt (πΆ βͺ {π΅})) CnP πΎ) = ((π½ βΎt (πΆ βͺ {π΅})) CnP πΎ)) |
83 | 82 | fveq1d 6802 |
. . . . . . 7
β’ ((π β§ (π΅ β β β§ π₯ β β)) β (((πΎ βΎt (πΆ βͺ {π΅})) CnP πΎ)βπ΅) = (((π½ βΎt (πΆ βͺ {π΅})) CnP πΎ)βπ΅)) |
84 | 74, 83 | eleq12d 2831 |
. . . . . 6
β’ ((π β§ (π΅ β β β§ π₯ β β)) β ((π§ β (πΆ βͺ {π΅}) β¦ if(π§ = π΅, π₯, ((πΉ βΎ πΆ)βπ§))) β (((πΎ βΎt (πΆ βͺ {π΅})) CnP πΎ)βπ΅) β ((π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, π₯, (πΉβπ§))) βΎ (πΆ βͺ {π΅})) β (((π½ βΎt (πΆ βͺ {π΅})) CnP πΎ)βπ΅))) |
85 | 61, 84 | bitrd 280 |
. . . . 5
β’ ((π β§ (π΅ β β β§ π₯ β β)) β (π₯ β ((πΉ βΎ πΆ) limβ π΅) β ((π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, π₯, (πΉβπ§))) βΎ (πΆ βͺ {π΅})) β (((π½ βΎt (πΆ βͺ {π΅})) CnP πΎ)βπ΅))) |
86 | 54, 56, 85 | 3bitr4rd 313 |
. . . 4
β’ ((π β§ (π΅ β β β§ π₯ β β)) β (π₯ β ((πΉ βΎ πΆ) limβ π΅) β π₯ β (πΉ limβ π΅))) |
87 | 86 | ex 414 |
. . 3
β’ (π β ((π΅ β β β§ π₯ β β) β (π₯ β ((πΉ βΎ πΆ) limβ π΅) β π₯ β (πΉ limβ π΅)))) |
88 | 6, 12, 87 | pm5.21ndd 382 |
. 2
β’ (π β (π₯ β ((πΉ βΎ πΆ) limβ π΅) β π₯ β (πΉ limβ π΅))) |
89 | 88 | eqrdv 2734 |
1
β’ (π β ((πΉ βΎ πΆ) limβ π΅) = (πΉ limβ π΅)) |