MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  limcres Structured version   Visualization version   GIF version

Theorem limcres 25091
Description: If 𝐡 is an interior point of 𝐢 βˆͺ {𝐡} relative to the domain 𝐴, then a limit point of 𝐹 β†Ύ 𝐢 extends to a limit of 𝐹. (Contributed by Mario Carneiro, 27-Dec-2016.)
Hypotheses
Ref Expression
limcres.f (πœ‘ β†’ 𝐹:π΄βŸΆβ„‚)
limcres.c (πœ‘ β†’ 𝐢 βŠ† 𝐴)
limcres.a (πœ‘ β†’ 𝐴 βŠ† β„‚)
limcres.k 𝐾 = (TopOpenβ€˜β„‚fld)
limcres.j 𝐽 = (𝐾 β†Ύt (𝐴 βˆͺ {𝐡}))
limcres.i (πœ‘ β†’ 𝐡 ∈ ((intβ€˜π½)β€˜(𝐢 βˆͺ {𝐡})))
Assertion
Ref Expression
limcres (πœ‘ β†’ ((𝐹 β†Ύ 𝐢) limβ„‚ 𝐡) = (𝐹 limβ„‚ 𝐡))

Proof of Theorem limcres
Dummy variables 𝑧 π‘₯ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 limcrcl 25079 . . . . . 6 (π‘₯ ∈ ((𝐹 β†Ύ 𝐢) limβ„‚ 𝐡) β†’ ((𝐹 β†Ύ 𝐢):dom (𝐹 β†Ύ 𝐢)βŸΆβ„‚ ∧ dom (𝐹 β†Ύ 𝐢) βŠ† β„‚ ∧ 𝐡 ∈ β„‚))
21simp3d 1144 . . . . 5 (π‘₯ ∈ ((𝐹 β†Ύ 𝐢) limβ„‚ 𝐡) β†’ 𝐡 ∈ β„‚)
3 limccl 25080 . . . . . 6 ((𝐹 β†Ύ 𝐢) limβ„‚ 𝐡) βŠ† β„‚
43sseli 3922 . . . . 5 (π‘₯ ∈ ((𝐹 β†Ύ 𝐢) limβ„‚ 𝐡) β†’ π‘₯ ∈ β„‚)
52, 4jca 513 . . . 4 (π‘₯ ∈ ((𝐹 β†Ύ 𝐢) limβ„‚ 𝐡) β†’ (𝐡 ∈ β„‚ ∧ π‘₯ ∈ β„‚))
65a1i 11 . . 3 (πœ‘ β†’ (π‘₯ ∈ ((𝐹 β†Ύ 𝐢) limβ„‚ 𝐡) β†’ (𝐡 ∈ β„‚ ∧ π‘₯ ∈ β„‚)))
7 limcrcl 25079 . . . . . 6 (π‘₯ ∈ (𝐹 limβ„‚ 𝐡) β†’ (𝐹:dom πΉβŸΆβ„‚ ∧ dom 𝐹 βŠ† β„‚ ∧ 𝐡 ∈ β„‚))
87simp3d 1144 . . . . 5 (π‘₯ ∈ (𝐹 limβ„‚ 𝐡) β†’ 𝐡 ∈ β„‚)
9 limccl 25080 . . . . . 6 (𝐹 limβ„‚ 𝐡) βŠ† β„‚
109sseli 3922 . . . . 5 (π‘₯ ∈ (𝐹 limβ„‚ 𝐡) β†’ π‘₯ ∈ β„‚)
118, 10jca 513 . . . 4 (π‘₯ ∈ (𝐹 limβ„‚ 𝐡) β†’ (𝐡 ∈ β„‚ ∧ π‘₯ ∈ β„‚))
1211a1i 11 . . 3 (πœ‘ β†’ (π‘₯ ∈ (𝐹 limβ„‚ 𝐡) β†’ (𝐡 ∈ β„‚ ∧ π‘₯ ∈ β„‚)))
13 limcres.j . . . . . . . 8 𝐽 = (𝐾 β†Ύt (𝐴 βˆͺ {𝐡}))
14 limcres.k . . . . . . . . . 10 𝐾 = (TopOpenβ€˜β„‚fld)
1514cnfldtopon 23987 . . . . . . . . 9 𝐾 ∈ (TopOnβ€˜β„‚)
16 limcres.a . . . . . . . . . . 11 (πœ‘ β†’ 𝐴 βŠ† β„‚)
1716adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ (𝐡 ∈ β„‚ ∧ π‘₯ ∈ β„‚)) β†’ 𝐴 βŠ† β„‚)
18 simprl 769 . . . . . . . . . . 11 ((πœ‘ ∧ (𝐡 ∈ β„‚ ∧ π‘₯ ∈ β„‚)) β†’ 𝐡 ∈ β„‚)
1918snssd 4748 . . . . . . . . . 10 ((πœ‘ ∧ (𝐡 ∈ β„‚ ∧ π‘₯ ∈ β„‚)) β†’ {𝐡} βŠ† β„‚)
2017, 19unssd 4126 . . . . . . . . 9 ((πœ‘ ∧ (𝐡 ∈ β„‚ ∧ π‘₯ ∈ β„‚)) β†’ (𝐴 βˆͺ {𝐡}) βŠ† β„‚)
21 resttopon 22353 . . . . . . . . 9 ((𝐾 ∈ (TopOnβ€˜β„‚) ∧ (𝐴 βˆͺ {𝐡}) βŠ† β„‚) β†’ (𝐾 β†Ύt (𝐴 βˆͺ {𝐡})) ∈ (TopOnβ€˜(𝐴 βˆͺ {𝐡})))
2215, 20, 21sylancr 588 . . . . . . . 8 ((πœ‘ ∧ (𝐡 ∈ β„‚ ∧ π‘₯ ∈ β„‚)) β†’ (𝐾 β†Ύt (𝐴 βˆͺ {𝐡})) ∈ (TopOnβ€˜(𝐴 βˆͺ {𝐡})))
2313, 22eqeltrid 2841 . . . . . . 7 ((πœ‘ ∧ (𝐡 ∈ β„‚ ∧ π‘₯ ∈ β„‚)) β†’ 𝐽 ∈ (TopOnβ€˜(𝐴 βˆͺ {𝐡})))
24 topontop 22103 . . . . . . 7 (𝐽 ∈ (TopOnβ€˜(𝐴 βˆͺ {𝐡})) β†’ 𝐽 ∈ Top)
2523, 24syl 17 . . . . . 6 ((πœ‘ ∧ (𝐡 ∈ β„‚ ∧ π‘₯ ∈ β„‚)) β†’ 𝐽 ∈ Top)
26 limcres.c . . . . . . . . 9 (πœ‘ β†’ 𝐢 βŠ† 𝐴)
2726adantr 482 . . . . . . . 8 ((πœ‘ ∧ (𝐡 ∈ β„‚ ∧ π‘₯ ∈ β„‚)) β†’ 𝐢 βŠ† 𝐴)
28 unss1 4119 . . . . . . . 8 (𝐢 βŠ† 𝐴 β†’ (𝐢 βˆͺ {𝐡}) βŠ† (𝐴 βˆͺ {𝐡}))
2927, 28syl 17 . . . . . . 7 ((πœ‘ ∧ (𝐡 ∈ β„‚ ∧ π‘₯ ∈ β„‚)) β†’ (𝐢 βˆͺ {𝐡}) βŠ† (𝐴 βˆͺ {𝐡}))
30 toponuni 22104 . . . . . . . 8 (𝐽 ∈ (TopOnβ€˜(𝐴 βˆͺ {𝐡})) β†’ (𝐴 βˆͺ {𝐡}) = βˆͺ 𝐽)
3123, 30syl 17 . . . . . . 7 ((πœ‘ ∧ (𝐡 ∈ β„‚ ∧ π‘₯ ∈ β„‚)) β†’ (𝐴 βˆͺ {𝐡}) = βˆͺ 𝐽)
3229, 31sseqtrd 3966 . . . . . 6 ((πœ‘ ∧ (𝐡 ∈ β„‚ ∧ π‘₯ ∈ β„‚)) β†’ (𝐢 βˆͺ {𝐡}) βŠ† βˆͺ 𝐽)
33 limcres.i . . . . . . 7 (πœ‘ β†’ 𝐡 ∈ ((intβ€˜π½)β€˜(𝐢 βˆͺ {𝐡})))
3433adantr 482 . . . . . 6 ((πœ‘ ∧ (𝐡 ∈ β„‚ ∧ π‘₯ ∈ β„‚)) β†’ 𝐡 ∈ ((intβ€˜π½)β€˜(𝐢 βˆͺ {𝐡})))
35 elun 4089 . . . . . . . . 9 (𝑧 ∈ (𝐴 βˆͺ {𝐡}) ↔ (𝑧 ∈ 𝐴 ∨ 𝑧 ∈ {𝐡}))
36 simplrr 776 . . . . . . . . . . 11 (((πœ‘ ∧ (𝐡 ∈ β„‚ ∧ π‘₯ ∈ β„‚)) ∧ 𝑧 ∈ 𝐴) β†’ π‘₯ ∈ β„‚)
37 limcres.f . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐹:π΄βŸΆβ„‚)
3837adantr 482 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝐡 ∈ β„‚ ∧ π‘₯ ∈ β„‚)) β†’ 𝐹:π΄βŸΆβ„‚)
3938ffvelcdmda 6989 . . . . . . . . . . 11 (((πœ‘ ∧ (𝐡 ∈ β„‚ ∧ π‘₯ ∈ β„‚)) ∧ 𝑧 ∈ 𝐴) β†’ (πΉβ€˜π‘§) ∈ β„‚)
4036, 39ifcld 4511 . . . . . . . . . 10 (((πœ‘ ∧ (𝐡 ∈ β„‚ ∧ π‘₯ ∈ β„‚)) ∧ 𝑧 ∈ 𝐴) β†’ if(𝑧 = 𝐡, π‘₯, (πΉβ€˜π‘§)) ∈ β„‚)
41 elsni 4582 . . . . . . . . . . . . 13 (𝑧 ∈ {𝐡} β†’ 𝑧 = 𝐡)
4241adantl 483 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝐡 ∈ β„‚ ∧ π‘₯ ∈ β„‚)) ∧ 𝑧 ∈ {𝐡}) β†’ 𝑧 = 𝐡)
4342iftrued 4473 . . . . . . . . . . 11 (((πœ‘ ∧ (𝐡 ∈ β„‚ ∧ π‘₯ ∈ β„‚)) ∧ 𝑧 ∈ {𝐡}) β†’ if(𝑧 = 𝐡, π‘₯, (πΉβ€˜π‘§)) = π‘₯)
44 simplrr 776 . . . . . . . . . . 11 (((πœ‘ ∧ (𝐡 ∈ β„‚ ∧ π‘₯ ∈ β„‚)) ∧ 𝑧 ∈ {𝐡}) β†’ π‘₯ ∈ β„‚)
4543, 44eqeltrd 2837 . . . . . . . . . 10 (((πœ‘ ∧ (𝐡 ∈ β„‚ ∧ π‘₯ ∈ β„‚)) ∧ 𝑧 ∈ {𝐡}) β†’ if(𝑧 = 𝐡, π‘₯, (πΉβ€˜π‘§)) ∈ β„‚)
4640, 45jaodan 956 . . . . . . . . 9 (((πœ‘ ∧ (𝐡 ∈ β„‚ ∧ π‘₯ ∈ β„‚)) ∧ (𝑧 ∈ 𝐴 ∨ 𝑧 ∈ {𝐡})) β†’ if(𝑧 = 𝐡, π‘₯, (πΉβ€˜π‘§)) ∈ β„‚)
4735, 46sylan2b 595 . . . . . . . 8 (((πœ‘ ∧ (𝐡 ∈ β„‚ ∧ π‘₯ ∈ β„‚)) ∧ 𝑧 ∈ (𝐴 βˆͺ {𝐡})) β†’ if(𝑧 = 𝐡, π‘₯, (πΉβ€˜π‘§)) ∈ β„‚)
4847fmpttd 7017 . . . . . . 7 ((πœ‘ ∧ (𝐡 ∈ β„‚ ∧ π‘₯ ∈ β„‚)) β†’ (𝑧 ∈ (𝐴 βˆͺ {𝐡}) ↦ if(𝑧 = 𝐡, π‘₯, (πΉβ€˜π‘§))):(𝐴 βˆͺ {𝐡})βŸΆβ„‚)
4931feq2d 6612 . . . . . . 7 ((πœ‘ ∧ (𝐡 ∈ β„‚ ∧ π‘₯ ∈ β„‚)) β†’ ((𝑧 ∈ (𝐴 βˆͺ {𝐡}) ↦ if(𝑧 = 𝐡, π‘₯, (πΉβ€˜π‘§))):(𝐴 βˆͺ {𝐡})βŸΆβ„‚ ↔ (𝑧 ∈ (𝐴 βˆͺ {𝐡}) ↦ if(𝑧 = 𝐡, π‘₯, (πΉβ€˜π‘§))):βˆͺ π½βŸΆβ„‚))
5048, 49mpbid 232 . . . . . 6 ((πœ‘ ∧ (𝐡 ∈ β„‚ ∧ π‘₯ ∈ β„‚)) β†’ (𝑧 ∈ (𝐴 βˆͺ {𝐡}) ↦ if(𝑧 = 𝐡, π‘₯, (πΉβ€˜π‘§))):βˆͺ π½βŸΆβ„‚)
51 eqid 2736 . . . . . . 7 βˆͺ 𝐽 = βˆͺ 𝐽
5215toponunii 22106 . . . . . . 7 β„‚ = βˆͺ 𝐾
5351, 52cnprest 22481 . . . . . 6 (((𝐽 ∈ Top ∧ (𝐢 βˆͺ {𝐡}) βŠ† βˆͺ 𝐽) ∧ (𝐡 ∈ ((intβ€˜π½)β€˜(𝐢 βˆͺ {𝐡})) ∧ (𝑧 ∈ (𝐴 βˆͺ {𝐡}) ↦ if(𝑧 = 𝐡, π‘₯, (πΉβ€˜π‘§))):βˆͺ π½βŸΆβ„‚)) β†’ ((𝑧 ∈ (𝐴 βˆͺ {𝐡}) ↦ if(𝑧 = 𝐡, π‘₯, (πΉβ€˜π‘§))) ∈ ((𝐽 CnP 𝐾)β€˜π΅) ↔ ((𝑧 ∈ (𝐴 βˆͺ {𝐡}) ↦ if(𝑧 = 𝐡, π‘₯, (πΉβ€˜π‘§))) β†Ύ (𝐢 βˆͺ {𝐡})) ∈ (((𝐽 β†Ύt (𝐢 βˆͺ {𝐡})) CnP 𝐾)β€˜π΅)))
5425, 32, 34, 50, 53syl22anc 837 . . . . 5 ((πœ‘ ∧ (𝐡 ∈ β„‚ ∧ π‘₯ ∈ β„‚)) β†’ ((𝑧 ∈ (𝐴 βˆͺ {𝐡}) ↦ if(𝑧 = 𝐡, π‘₯, (πΉβ€˜π‘§))) ∈ ((𝐽 CnP 𝐾)β€˜π΅) ↔ ((𝑧 ∈ (𝐴 βˆͺ {𝐡}) ↦ if(𝑧 = 𝐡, π‘₯, (πΉβ€˜π‘§))) β†Ύ (𝐢 βˆͺ {𝐡})) ∈ (((𝐽 β†Ύt (𝐢 βˆͺ {𝐡})) CnP 𝐾)β€˜π΅)))
55 eqid 2736 . . . . . 6 (𝑧 ∈ (𝐴 βˆͺ {𝐡}) ↦ if(𝑧 = 𝐡, π‘₯, (πΉβ€˜π‘§))) = (𝑧 ∈ (𝐴 βˆͺ {𝐡}) ↦ if(𝑧 = 𝐡, π‘₯, (πΉβ€˜π‘§)))
5613, 14, 55, 38, 17, 18ellimc 25078 . . . . 5 ((πœ‘ ∧ (𝐡 ∈ β„‚ ∧ π‘₯ ∈ β„‚)) β†’ (π‘₯ ∈ (𝐹 limβ„‚ 𝐡) ↔ (𝑧 ∈ (𝐴 βˆͺ {𝐡}) ↦ if(𝑧 = 𝐡, π‘₯, (πΉβ€˜π‘§))) ∈ ((𝐽 CnP 𝐾)β€˜π΅)))
57 eqid 2736 . . . . . . 7 (𝐾 β†Ύt (𝐢 βˆͺ {𝐡})) = (𝐾 β†Ύt (𝐢 βˆͺ {𝐡}))
58 eqid 2736 . . . . . . 7 (𝑧 ∈ (𝐢 βˆͺ {𝐡}) ↦ if(𝑧 = 𝐡, π‘₯, ((𝐹 β†Ύ 𝐢)β€˜π‘§))) = (𝑧 ∈ (𝐢 βˆͺ {𝐡}) ↦ if(𝑧 = 𝐡, π‘₯, ((𝐹 β†Ύ 𝐢)β€˜π‘§)))
5938, 27fssresd 6667 . . . . . . 7 ((πœ‘ ∧ (𝐡 ∈ β„‚ ∧ π‘₯ ∈ β„‚)) β†’ (𝐹 β†Ύ 𝐢):πΆβŸΆβ„‚)
6027, 17sstrd 3936 . . . . . . 7 ((πœ‘ ∧ (𝐡 ∈ β„‚ ∧ π‘₯ ∈ β„‚)) β†’ 𝐢 βŠ† β„‚)
6157, 14, 58, 59, 60, 18ellimc 25078 . . . . . 6 ((πœ‘ ∧ (𝐡 ∈ β„‚ ∧ π‘₯ ∈ β„‚)) β†’ (π‘₯ ∈ ((𝐹 β†Ύ 𝐢) limβ„‚ 𝐡) ↔ (𝑧 ∈ (𝐢 βˆͺ {𝐡}) ↦ if(𝑧 = 𝐡, π‘₯, ((𝐹 β†Ύ 𝐢)β€˜π‘§))) ∈ (((𝐾 β†Ύt (𝐢 βˆͺ {𝐡})) CnP 𝐾)β€˜π΅)))
62 elun 4089 . . . . . . . . . . 11 (𝑧 ∈ (𝐢 βˆͺ {𝐡}) ↔ (𝑧 ∈ 𝐢 ∨ 𝑧 ∈ {𝐡}))
63 velsn 4581 . . . . . . . . . . . 12 (𝑧 ∈ {𝐡} ↔ 𝑧 = 𝐡)
6463orbi2i 911 . . . . . . . . . . 11 ((𝑧 ∈ 𝐢 ∨ 𝑧 ∈ {𝐡}) ↔ (𝑧 ∈ 𝐢 ∨ 𝑧 = 𝐡))
6562, 64bitri 276 . . . . . . . . . 10 (𝑧 ∈ (𝐢 βˆͺ {𝐡}) ↔ (𝑧 ∈ 𝐢 ∨ 𝑧 = 𝐡))
66 pm5.61 999 . . . . . . . . . . . 12 (((𝑧 ∈ 𝐢 ∨ 𝑧 = 𝐡) ∧ Β¬ 𝑧 = 𝐡) ↔ (𝑧 ∈ 𝐢 ∧ Β¬ 𝑧 = 𝐡))
67 fvres 6819 . . . . . . . . . . . . 13 (𝑧 ∈ 𝐢 β†’ ((𝐹 β†Ύ 𝐢)β€˜π‘§) = (πΉβ€˜π‘§))
6867adantr 482 . . . . . . . . . . . 12 ((𝑧 ∈ 𝐢 ∧ Β¬ 𝑧 = 𝐡) β†’ ((𝐹 β†Ύ 𝐢)β€˜π‘§) = (πΉβ€˜π‘§))
6966, 68sylbi 216 . . . . . . . . . . 11 (((𝑧 ∈ 𝐢 ∨ 𝑧 = 𝐡) ∧ Β¬ 𝑧 = 𝐡) β†’ ((𝐹 β†Ύ 𝐢)β€˜π‘§) = (πΉβ€˜π‘§))
7069ifeq2da 4497 . . . . . . . . . 10 ((𝑧 ∈ 𝐢 ∨ 𝑧 = 𝐡) β†’ if(𝑧 = 𝐡, π‘₯, ((𝐹 β†Ύ 𝐢)β€˜π‘§)) = if(𝑧 = 𝐡, π‘₯, (πΉβ€˜π‘§)))
7165, 70sylbi 216 . . . . . . . . 9 (𝑧 ∈ (𝐢 βˆͺ {𝐡}) β†’ if(𝑧 = 𝐡, π‘₯, ((𝐹 β†Ύ 𝐢)β€˜π‘§)) = if(𝑧 = 𝐡, π‘₯, (πΉβ€˜π‘§)))
7271mpteq2ia 5184 . . . . . . . 8 (𝑧 ∈ (𝐢 βˆͺ {𝐡}) ↦ if(𝑧 = 𝐡, π‘₯, ((𝐹 β†Ύ 𝐢)β€˜π‘§))) = (𝑧 ∈ (𝐢 βˆͺ {𝐡}) ↦ if(𝑧 = 𝐡, π‘₯, (πΉβ€˜π‘§)))
7329resmptd 5956 . . . . . . . 8 ((πœ‘ ∧ (𝐡 ∈ β„‚ ∧ π‘₯ ∈ β„‚)) β†’ ((𝑧 ∈ (𝐴 βˆͺ {𝐡}) ↦ if(𝑧 = 𝐡, π‘₯, (πΉβ€˜π‘§))) β†Ύ (𝐢 βˆͺ {𝐡})) = (𝑧 ∈ (𝐢 βˆͺ {𝐡}) ↦ if(𝑧 = 𝐡, π‘₯, (πΉβ€˜π‘§))))
7472, 73eqtr4id 2795 . . . . . . 7 ((πœ‘ ∧ (𝐡 ∈ β„‚ ∧ π‘₯ ∈ β„‚)) β†’ (𝑧 ∈ (𝐢 βˆͺ {𝐡}) ↦ if(𝑧 = 𝐡, π‘₯, ((𝐹 β†Ύ 𝐢)β€˜π‘§))) = ((𝑧 ∈ (𝐴 βˆͺ {𝐡}) ↦ if(𝑧 = 𝐡, π‘₯, (πΉβ€˜π‘§))) β†Ύ (𝐢 βˆͺ {𝐡})))
7513oveq1i 7313 . . . . . . . . . 10 (𝐽 β†Ύt (𝐢 βˆͺ {𝐡})) = ((𝐾 β†Ύt (𝐴 βˆͺ {𝐡})) β†Ύt (𝐢 βˆͺ {𝐡}))
76 cnex 10994 . . . . . . . . . . . . 13 β„‚ ∈ V
7776ssex 5254 . . . . . . . . . . . 12 ((𝐴 βˆͺ {𝐡}) βŠ† β„‚ β†’ (𝐴 βˆͺ {𝐡}) ∈ V)
7820, 77syl 17 . . . . . . . . . . 11 ((πœ‘ ∧ (𝐡 ∈ β„‚ ∧ π‘₯ ∈ β„‚)) β†’ (𝐴 βˆͺ {𝐡}) ∈ V)
79 restabs 22357 . . . . . . . . . . 11 ((𝐾 ∈ (TopOnβ€˜β„‚) ∧ (𝐢 βˆͺ {𝐡}) βŠ† (𝐴 βˆͺ {𝐡}) ∧ (𝐴 βˆͺ {𝐡}) ∈ V) β†’ ((𝐾 β†Ύt (𝐴 βˆͺ {𝐡})) β†Ύt (𝐢 βˆͺ {𝐡})) = (𝐾 β†Ύt (𝐢 βˆͺ {𝐡})))
8015, 29, 78, 79mp3an2i 1466 . . . . . . . . . 10 ((πœ‘ ∧ (𝐡 ∈ β„‚ ∧ π‘₯ ∈ β„‚)) β†’ ((𝐾 β†Ύt (𝐴 βˆͺ {𝐡})) β†Ύt (𝐢 βˆͺ {𝐡})) = (𝐾 β†Ύt (𝐢 βˆͺ {𝐡})))
8175, 80eqtr2id 2789 . . . . . . . . 9 ((πœ‘ ∧ (𝐡 ∈ β„‚ ∧ π‘₯ ∈ β„‚)) β†’ (𝐾 β†Ύt (𝐢 βˆͺ {𝐡})) = (𝐽 β†Ύt (𝐢 βˆͺ {𝐡})))
8281oveq1d 7318 . . . . . . . 8 ((πœ‘ ∧ (𝐡 ∈ β„‚ ∧ π‘₯ ∈ β„‚)) β†’ ((𝐾 β†Ύt (𝐢 βˆͺ {𝐡})) CnP 𝐾) = ((𝐽 β†Ύt (𝐢 βˆͺ {𝐡})) CnP 𝐾))
8382fveq1d 6802 . . . . . . 7 ((πœ‘ ∧ (𝐡 ∈ β„‚ ∧ π‘₯ ∈ β„‚)) β†’ (((𝐾 β†Ύt (𝐢 βˆͺ {𝐡})) CnP 𝐾)β€˜π΅) = (((𝐽 β†Ύt (𝐢 βˆͺ {𝐡})) CnP 𝐾)β€˜π΅))
8474, 83eleq12d 2831 . . . . . 6 ((πœ‘ ∧ (𝐡 ∈ β„‚ ∧ π‘₯ ∈ β„‚)) β†’ ((𝑧 ∈ (𝐢 βˆͺ {𝐡}) ↦ if(𝑧 = 𝐡, π‘₯, ((𝐹 β†Ύ 𝐢)β€˜π‘§))) ∈ (((𝐾 β†Ύt (𝐢 βˆͺ {𝐡})) CnP 𝐾)β€˜π΅) ↔ ((𝑧 ∈ (𝐴 βˆͺ {𝐡}) ↦ if(𝑧 = 𝐡, π‘₯, (πΉβ€˜π‘§))) β†Ύ (𝐢 βˆͺ {𝐡})) ∈ (((𝐽 β†Ύt (𝐢 βˆͺ {𝐡})) CnP 𝐾)β€˜π΅)))
8561, 84bitrd 280 . . . . 5 ((πœ‘ ∧ (𝐡 ∈ β„‚ ∧ π‘₯ ∈ β„‚)) β†’ (π‘₯ ∈ ((𝐹 β†Ύ 𝐢) limβ„‚ 𝐡) ↔ ((𝑧 ∈ (𝐴 βˆͺ {𝐡}) ↦ if(𝑧 = 𝐡, π‘₯, (πΉβ€˜π‘§))) β†Ύ (𝐢 βˆͺ {𝐡})) ∈ (((𝐽 β†Ύt (𝐢 βˆͺ {𝐡})) CnP 𝐾)β€˜π΅)))
8654, 56, 853bitr4rd 313 . . . 4 ((πœ‘ ∧ (𝐡 ∈ β„‚ ∧ π‘₯ ∈ β„‚)) β†’ (π‘₯ ∈ ((𝐹 β†Ύ 𝐢) limβ„‚ 𝐡) ↔ π‘₯ ∈ (𝐹 limβ„‚ 𝐡)))
8786ex 414 . . 3 (πœ‘ β†’ ((𝐡 ∈ β„‚ ∧ π‘₯ ∈ β„‚) β†’ (π‘₯ ∈ ((𝐹 β†Ύ 𝐢) limβ„‚ 𝐡) ↔ π‘₯ ∈ (𝐹 limβ„‚ 𝐡))))
886, 12, 87pm5.21ndd 382 . 2 (πœ‘ β†’ (π‘₯ ∈ ((𝐹 β†Ύ 𝐢) limβ„‚ 𝐡) ↔ π‘₯ ∈ (𝐹 limβ„‚ 𝐡)))
8988eqrdv 2734 1 (πœ‘ β†’ ((𝐹 β†Ύ 𝐢) limβ„‚ 𝐡) = (𝐹 limβ„‚ 𝐡))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∨ wo 845   = wceq 1539   ∈ wcel 2104  Vcvv 3437   βˆͺ cun 3890   βŠ† wss 3892  ifcif 4465  {csn 4565  βˆͺ cuni 4844   ↦ cmpt 5164  dom cdm 5596   β†Ύ cres 5598  βŸΆwf 6450  β€˜cfv 6454  (class class class)co 7303  β„‚cc 10911   β†Ύt crest 17172  TopOpenctopn 17173  β„‚fldccnfld 20638  Topctop 22083  TopOnctopon 22100  intcnt 22209   CnP ccnp 22417   limβ„‚ climc 25067
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2707  ax-rep 5218  ax-sep 5232  ax-nul 5239  ax-pow 5297  ax-pr 5361  ax-un 7616  ax-cnex 10969  ax-resscn 10970  ax-1cn 10971  ax-icn 10972  ax-addcl 10973  ax-addrcl 10974  ax-mulcl 10975  ax-mulrcl 10976  ax-mulcom 10977  ax-addass 10978  ax-mulass 10979  ax-distr 10980  ax-i2m1 10981  ax-1ne0 10982  ax-1rid 10983  ax-rnegex 10984  ax-rrecex 10985  ax-cnre 10986  ax-pre-lttri 10987  ax-pre-lttrn 10988  ax-pre-ltadd 10989  ax-pre-mulgt0 10990  ax-pre-sup 10991
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3or 1088  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3285  df-reu 3286  df-rab 3287  df-v 3439  df-sbc 3722  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-pss 3911  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4566  df-pr 4568  df-tp 4570  df-op 4572  df-uni 4845  df-int 4887  df-iun 4933  df-br 5082  df-opab 5144  df-mpt 5165  df-tr 5199  df-id 5496  df-eprel 5502  df-po 5510  df-so 5511  df-fr 5551  df-we 5553  df-xp 5602  df-rel 5603  df-cnv 5604  df-co 5605  df-dm 5606  df-rn 5607  df-res 5608  df-ima 5609  df-pred 6213  df-ord 6280  df-on 6281  df-lim 6282  df-suc 6283  df-iota 6406  df-fun 6456  df-fn 6457  df-f 6458  df-f1 6459  df-fo 6460  df-f1o 6461  df-fv 6462  df-riota 7260  df-ov 7306  df-oprab 7307  df-mpo 7308  df-om 7741  df-1st 7859  df-2nd 7860  df-frecs 8124  df-wrecs 8155  df-recs 8229  df-rdg 8268  df-1o 8324  df-er 8525  df-map 8644  df-pm 8645  df-en 8761  df-dom 8762  df-sdom 8763  df-fin 8764  df-fi 9210  df-sup 9241  df-inf 9242  df-pnf 11053  df-mnf 11054  df-xr 11055  df-ltxr 11056  df-le 11057  df-sub 11249  df-neg 11250  df-div 11675  df-nn 12016  df-2 12078  df-3 12079  df-4 12080  df-5 12081  df-6 12082  df-7 12083  df-8 12084  df-9 12085  df-n0 12276  df-z 12362  df-dec 12480  df-uz 12625  df-q 12731  df-rp 12773  df-xneg 12890  df-xadd 12891  df-xmul 12892  df-fz 13282  df-seq 13764  df-exp 13825  df-cj 14851  df-re 14852  df-im 14853  df-sqrt 14987  df-abs 14988  df-struct 16889  df-slot 16924  df-ndx 16936  df-base 16954  df-plusg 17016  df-mulr 17017  df-starv 17018  df-tset 17022  df-ple 17023  df-ds 17025  df-unif 17026  df-rest 17174  df-topn 17175  df-topgen 17195  df-psmet 20630  df-xmet 20631  df-met 20632  df-bl 20633  df-mopn 20634  df-cnfld 20639  df-top 22084  df-topon 22101  df-topsp 22123  df-bases 22137  df-ntr 22212  df-cnp 22420  df-xms 23514  df-ms 23515  df-limc 25071
This theorem is referenced by:  dvreslem  25114  dvaddbr  25143  dvmulbr  25144  lhop2  25220  lhop  25221  limciccioolb  43210  limcicciooub  43226  limcresiooub  43231  limcresioolb  43232  ioccncflimc  43474  icocncflimc  43478  dirkercncflem3  43694  fourierdlem32  43728  fourierdlem33  43729  fourierdlem48  43743  fourierdlem49  43744  fourierdlem62  43757  fouriersw  43820
  Copyright terms: Public domain W3C validator