MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  limccnp2 Structured version   Visualization version   GIF version
Theorem limccnp2 25401
Description: The image of a convergent sequence under a continuous map is convergent to the image of the original point. Binary operation version. (Contributed by Mario Carneiro, 28-Dec-2016.)
Hypotheses
Ref Expression
limccnp2.r ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ 𝑅 ∈ 𝑋)
limccnp2.s ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ 𝑆 ∈ π‘Œ)
limccnp2.x (πœ‘ β†’ 𝑋 βŠ† β„‚)
limccnp2.y (πœ‘ β†’ π‘Œ βŠ† β„‚)
limccnp2.k 𝐾 = (TopOpenβ€˜β„‚fld)
limccnp2.j 𝐽 = ((𝐾 Γ—t 𝐾) β†Ύt (𝑋 Γ— π‘Œ))
limccnp2.c (πœ‘ β†’ 𝐢 ∈ ((π‘₯ ∈ 𝐴 ↦ 𝑅) limβ„‚ 𝐡))
limccnp2.d (πœ‘ β†’ 𝐷 ∈ ((π‘₯ ∈ 𝐴 ↦ 𝑆) limβ„‚ 𝐡))
limccnp2.h (πœ‘ β†’ 𝐻 ∈ ((𝐽 CnP 𝐾)β€˜βŸ¨πΆ, 𝐷⟩))
Assertion
Ref Expression
limccnp2 (πœ‘ β†’ (𝐢𝐻𝐷) ∈ ((π‘₯ ∈ 𝐴 ↦ (𝑅𝐻𝑆)) limβ„‚ 𝐡))
Distinct variable groups:   π‘₯,𝐡   π‘₯,𝐢   π‘₯,𝐷   π‘₯,𝐻   πœ‘,π‘₯   π‘₯,𝑋   π‘₯,𝐴   π‘₯,π‘Œ
Allowed substitution hints:   𝑅(π‘₯)   𝑆(π‘₯)   𝐽(π‘₯)   𝐾(π‘₯)
Proof of Theorem limccnp2
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 limccnp2.h . . . . . . . . . . 11 (πœ‘ β†’ 𝐻 ∈ ((𝐽 CnP 𝐾)β€˜βŸ¨πΆ, 𝐷⟩))
2 eqid 2733 . . . . . . . . . . . 12 βˆͺ 𝐽 = βˆͺ 𝐽
32cnprcl 22741 . . . . . . . . . . 11 (𝐻 ∈ ((𝐽 CnP 𝐾)β€˜βŸ¨πΆ, 𝐷⟩) β†’ ⟨𝐢, 𝐷⟩ ∈ βˆͺ 𝐽)
41, 3syl 17 . . . . . . . . . 10 (πœ‘ β†’ ⟨𝐢, 𝐷⟩ ∈ βˆͺ 𝐽)
5 limccnp2.j . . . . . . . . . . . 12 𝐽 = ((𝐾 Γ—t 𝐾) β†Ύt (𝑋 Γ— π‘Œ))
6 limccnp2.k . . . . . . . . . . . . . . 15 𝐾 = (TopOpenβ€˜β„‚fld)
76cnfldtopon 24291 . . . . . . . . . . . . . 14 𝐾 ∈ (TopOnβ€˜β„‚)
8 txtopon 23087 . . . . . . . . . . . . . 14 ((𝐾 ∈ (TopOnβ€˜β„‚) ∧ 𝐾 ∈ (TopOnβ€˜β„‚)) β†’ (𝐾 Γ—t 𝐾) ∈ (TopOnβ€˜(β„‚ Γ— β„‚)))
97, 7, 8mp2an 691 . . . . . . . . . . . . 13 (𝐾 Γ—t 𝐾) ∈ (TopOnβ€˜(β„‚ Γ— β„‚))
10 limccnp2.x . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝑋 βŠ† β„‚)
11 limccnp2.y . . . . . . . . . . . . . 14 (πœ‘ β†’ π‘Œ βŠ† β„‚)
12 xpss12 5691 . . . . . . . . . . . . . 14 ((𝑋 βŠ† β„‚ ∧ π‘Œ βŠ† β„‚) β†’ (𝑋 Γ— π‘Œ) βŠ† (β„‚ Γ— β„‚))
1310, 11, 12syl2anc 585 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑋 Γ— π‘Œ) βŠ† (β„‚ Γ— β„‚))
14 resttopon 22657 . . . . . . . . . . . . 13 (((𝐾 Γ—t 𝐾) ∈ (TopOnβ€˜(β„‚ Γ— β„‚)) ∧ (𝑋 Γ— π‘Œ) βŠ† (β„‚ Γ— β„‚)) β†’ ((𝐾 Γ—t 𝐾) β†Ύt (𝑋 Γ— π‘Œ)) ∈ (TopOnβ€˜(𝑋 Γ— π‘Œ)))
159, 13, 14sylancr 588 . . . . . . . . . . . 12 (πœ‘ β†’ ((𝐾 Γ—t 𝐾) β†Ύt (𝑋 Γ— π‘Œ)) ∈ (TopOnβ€˜(𝑋 Γ— π‘Œ)))
165, 15eqeltrid 2838 . . . . . . . . . . 11 (πœ‘ β†’ 𝐽 ∈ (TopOnβ€˜(𝑋 Γ— π‘Œ)))
17 toponuni 22408 . . . . . . . . . . 11 (𝐽 ∈ (TopOnβ€˜(𝑋 Γ— π‘Œ)) β†’ (𝑋 Γ— π‘Œ) = βˆͺ 𝐽)
1816, 17syl 17 . . . . . . . . . 10 (πœ‘ β†’ (𝑋 Γ— π‘Œ) = βˆͺ 𝐽)
194, 18eleqtrrd 2837 . . . . . . . . 9 (πœ‘ β†’ ⟨𝐢, 𝐷⟩ ∈ (𝑋 Γ— π‘Œ))
20 opelxp 5712 . . . . . . . . 9 (⟨𝐢, 𝐷⟩ ∈ (𝑋 Γ— π‘Œ) ↔ (𝐢 ∈ 𝑋 ∧ 𝐷 ∈ π‘Œ))
2119, 20sylib 217 . . . . . . . 8 (πœ‘ β†’ (𝐢 ∈ 𝑋 ∧ 𝐷 ∈ π‘Œ))
2221simpld 496 . . . . . . 7 (πœ‘ β†’ 𝐢 ∈ 𝑋)
2322ad2antrr 725 . . . . . 6 (((πœ‘ ∧ π‘₯ ∈ (𝐴 βˆͺ {𝐡})) ∧ π‘₯ = 𝐡) β†’ 𝐢 ∈ 𝑋)
24 simpll 766 . . . . . . 7 (((πœ‘ ∧ π‘₯ ∈ (𝐴 βˆͺ {𝐡})) ∧ Β¬ π‘₯ = 𝐡) β†’ πœ‘)
25 simpr 486 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ (𝐴 βˆͺ {𝐡})) β†’ π‘₯ ∈ (𝐴 βˆͺ {𝐡}))
26 elun 4148 . . . . . . . . . . . 12 (π‘₯ ∈ (𝐴 βˆͺ {𝐡}) ↔ (π‘₯ ∈ 𝐴 ∨ π‘₯ ∈ {𝐡}))
2725, 26sylib 217 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ (𝐴 βˆͺ {𝐡})) β†’ (π‘₯ ∈ 𝐴 ∨ π‘₯ ∈ {𝐡}))
2827ord 863 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ (𝐴 βˆͺ {𝐡})) β†’ (Β¬ π‘₯ ∈ 𝐴 β†’ π‘₯ ∈ {𝐡}))
29 elsni 4645 . . . . . . . . . 10 (π‘₯ ∈ {𝐡} β†’ π‘₯ = 𝐡)
3028, 29syl6 35 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ (𝐴 βˆͺ {𝐡})) β†’ (Β¬ π‘₯ ∈ 𝐴 β†’ π‘₯ = 𝐡))
3130con1d 145 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ (𝐴 βˆͺ {𝐡})) β†’ (Β¬ π‘₯ = 𝐡 β†’ π‘₯ ∈ 𝐴))
3231imp 408 . . . . . . 7 (((πœ‘ ∧ π‘₯ ∈ (𝐴 βˆͺ {𝐡})) ∧ Β¬ π‘₯ = 𝐡) β†’ π‘₯ ∈ 𝐴)
33 limccnp2.r . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ 𝑅 ∈ 𝑋)
3424, 32, 33syl2anc 585 . . . . . 6 (((πœ‘ ∧ π‘₯ ∈ (𝐴 βˆͺ {𝐡})) ∧ Β¬ π‘₯ = 𝐡) β†’ 𝑅 ∈ 𝑋)
3523, 34ifclda 4563 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ (𝐴 βˆͺ {𝐡})) β†’ if(π‘₯ = 𝐡, 𝐢, 𝑅) ∈ 𝑋)
3621simprd 497 . . . . . . 7 (πœ‘ β†’ 𝐷 ∈ π‘Œ)
3736ad2antrr 725 . . . . . 6 (((πœ‘ ∧ π‘₯ ∈ (𝐴 βˆͺ {𝐡})) ∧ π‘₯ = 𝐡) β†’ 𝐷 ∈ π‘Œ)
38 limccnp2.s . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ 𝑆 ∈ π‘Œ)
3924, 32, 38syl2anc 585 . . . . . 6 (((πœ‘ ∧ π‘₯ ∈ (𝐴 βˆͺ {𝐡})) ∧ Β¬ π‘₯ = 𝐡) β†’ 𝑆 ∈ π‘Œ)
4037, 39ifclda 4563 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ (𝐴 βˆͺ {𝐡})) β†’ if(π‘₯ = 𝐡, 𝐷, 𝑆) ∈ π‘Œ)
4135, 40opelxpd 5714 . . . 4 ((πœ‘ ∧ π‘₯ ∈ (𝐴 βˆͺ {𝐡})) β†’ ⟨if(π‘₯ = 𝐡, 𝐢, 𝑅), if(π‘₯ = 𝐡, 𝐷, 𝑆)⟩ ∈ (𝑋 Γ— π‘Œ))
42 eqidd 2734 . . . 4 (πœ‘ β†’ (π‘₯ ∈ (𝐴 βˆͺ {𝐡}) ↦ ⟨if(π‘₯ = 𝐡, 𝐢, 𝑅), if(π‘₯ = 𝐡, 𝐷, 𝑆)⟩) = (π‘₯ ∈ (𝐴 βˆͺ {𝐡}) ↦ ⟨if(π‘₯ = 𝐡, 𝐢, 𝑅), if(π‘₯ = 𝐡, 𝐷, 𝑆)⟩))
437a1i 11 . . . . . 6 (πœ‘ β†’ 𝐾 ∈ (TopOnβ€˜β„‚))
44 cnpf2 22746 . . . . . 6 ((𝐽 ∈ (TopOnβ€˜(𝑋 Γ— π‘Œ)) ∧ 𝐾 ∈ (TopOnβ€˜β„‚) ∧ 𝐻 ∈ ((𝐽 CnP 𝐾)β€˜βŸ¨πΆ, 𝐷⟩)) β†’ 𝐻:(𝑋 Γ— π‘Œ)βŸΆβ„‚)
4516, 43, 1, 44syl3anc 1372 . . . . 5 (πœ‘ β†’ 𝐻:(𝑋 Γ— π‘Œ)βŸΆβ„‚)
4645feqmptd 6958 . . . 4 (πœ‘ β†’ 𝐻 = (𝑦 ∈ (𝑋 Γ— π‘Œ) ↦ (π»β€˜π‘¦)))
47 fveq2 6889 . . . . 5 (𝑦 = ⟨if(π‘₯ = 𝐡, 𝐢, 𝑅), if(π‘₯ = 𝐡, 𝐷, 𝑆)⟩ β†’ (π»β€˜π‘¦) = (π»β€˜βŸ¨if(π‘₯ = 𝐡, 𝐢, 𝑅), if(π‘₯ = 𝐡, 𝐷, 𝑆)⟩))
48 df-ov 7409 . . . . . 6 (if(π‘₯ = 𝐡, 𝐢, 𝑅)𝐻if(π‘₯ = 𝐡, 𝐷, 𝑆)) = (π»β€˜βŸ¨if(π‘₯ = 𝐡, 𝐢, 𝑅), if(π‘₯ = 𝐡, 𝐷, 𝑆)⟩)
49 ovif12 7505 . . . . . 6 (if(π‘₯ = 𝐡, 𝐢, 𝑅)𝐻if(π‘₯ = 𝐡, 𝐷, 𝑆)) = if(π‘₯ = 𝐡, (𝐢𝐻𝐷), (𝑅𝐻𝑆))
5048, 49eqtr3i 2763 . . . . 5 (π»β€˜βŸ¨if(π‘₯ = 𝐡, 𝐢, 𝑅), if(π‘₯ = 𝐡, 𝐷, 𝑆)⟩) = if(π‘₯ = 𝐡, (𝐢𝐻𝐷), (𝑅𝐻𝑆))
5147, 50eqtrdi 2789 . . . 4 (𝑦 = ⟨if(π‘₯ = 𝐡, 𝐢, 𝑅), if(π‘₯ = 𝐡, 𝐷, 𝑆)⟩ β†’ (π»β€˜π‘¦) = if(π‘₯ = 𝐡, (𝐢𝐻𝐷), (𝑅𝐻𝑆)))
5241, 42, 46, 51fmptco 7124 . . 3 (πœ‘ β†’ (𝐻 ∘ (π‘₯ ∈ (𝐴 βˆͺ {𝐡}) ↦ ⟨if(π‘₯ = 𝐡, 𝐢, 𝑅), if(π‘₯ = 𝐡, 𝐷, 𝑆)⟩)) = (π‘₯ ∈ (𝐴 βˆͺ {𝐡}) ↦ if(π‘₯ = 𝐡, (𝐢𝐻𝐷), (𝑅𝐻𝑆))))
53 eqid 2733 . . . . . . . . . . 11 (π‘₯ ∈ 𝐴 ↦ 𝑅) = (π‘₯ ∈ 𝐴 ↦ 𝑅)
5453, 33dmmptd 6693 . . . . . . . . . 10 (πœ‘ β†’ dom (π‘₯ ∈ 𝐴 ↦ 𝑅) = 𝐴)
55 limccnp2.c . . . . . . . . . . . 12 (πœ‘ β†’ 𝐢 ∈ ((π‘₯ ∈ 𝐴 ↦ 𝑅) limβ„‚ 𝐡))
56 limcrcl 25383 . . . . . . . . . . . 12 (𝐢 ∈ ((π‘₯ ∈ 𝐴 ↦ 𝑅) limβ„‚ 𝐡) β†’ ((π‘₯ ∈ 𝐴 ↦ 𝑅):dom (π‘₯ ∈ 𝐴 ↦ 𝑅)βŸΆβ„‚ ∧ dom (π‘₯ ∈ 𝐴 ↦ 𝑅) βŠ† β„‚ ∧ 𝐡 ∈ β„‚))
5755, 56syl 17 . . . . . . . . . . 11 (πœ‘ β†’ ((π‘₯ ∈ 𝐴 ↦ 𝑅):dom (π‘₯ ∈ 𝐴 ↦ 𝑅)βŸΆβ„‚ ∧ dom (π‘₯ ∈ 𝐴 ↦ 𝑅) βŠ† β„‚ ∧ 𝐡 ∈ β„‚))
5857simp2d 1144 . . . . . . . . . 10 (πœ‘ β†’ dom (π‘₯ ∈ 𝐴 ↦ 𝑅) βŠ† β„‚)
5954, 58eqsstrrd 4021 . . . . . . . . 9 (πœ‘ β†’ 𝐴 βŠ† β„‚)
6057simp3d 1145 . . . . . . . . . 10 (πœ‘ β†’ 𝐡 ∈ β„‚)
6160snssd 4812 . . . . . . . . 9 (πœ‘ β†’ {𝐡} βŠ† β„‚)
6259, 61unssd 4186 . . . . . . . 8 (πœ‘ β†’ (𝐴 βˆͺ {𝐡}) βŠ† β„‚)
63 resttopon 22657 . . . . . . . 8 ((𝐾 ∈ (TopOnβ€˜β„‚) ∧ (𝐴 βˆͺ {𝐡}) βŠ† β„‚) β†’ (𝐾 β†Ύt (𝐴 βˆͺ {𝐡})) ∈ (TopOnβ€˜(𝐴 βˆͺ {𝐡})))
647, 62, 63sylancr 588 . . . . . . 7 (πœ‘ β†’ (𝐾 β†Ύt (𝐴 βˆͺ {𝐡})) ∈ (TopOnβ€˜(𝐴 βˆͺ {𝐡})))
65 ssun2 4173 . . . . . . . 8 {𝐡} βŠ† (𝐴 βˆͺ {𝐡})
66 snssg 4787 . . . . . . . . 9 (𝐡 ∈ β„‚ β†’ (𝐡 ∈ (𝐴 βˆͺ {𝐡}) ↔ {𝐡} βŠ† (𝐴 βˆͺ {𝐡})))
6760, 66syl 17 . . . . . . . 8 (πœ‘ β†’ (𝐡 ∈ (𝐴 βˆͺ {𝐡}) ↔ {𝐡} βŠ† (𝐴 βˆͺ {𝐡})))
6865, 67mpbiri 258 . . . . . . 7 (πœ‘ β†’ 𝐡 ∈ (𝐴 βˆͺ {𝐡}))
6910adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ 𝑋 βŠ† β„‚)
7069, 33sseldd 3983 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ 𝑅 ∈ β„‚)
71 eqid 2733 . . . . . . . . 9 (𝐾 β†Ύt (𝐴 βˆͺ {𝐡})) = (𝐾 β†Ύt (𝐴 βˆͺ {𝐡}))
7259, 60, 70, 71, 6limcmpt 25392 . . . . . . . 8 (πœ‘ β†’ (𝐢 ∈ ((π‘₯ ∈ 𝐴 ↦ 𝑅) limβ„‚ 𝐡) ↔ (π‘₯ ∈ (𝐴 βˆͺ {𝐡}) ↦ if(π‘₯ = 𝐡, 𝐢, 𝑅)) ∈ (((𝐾 β†Ύt (𝐴 βˆͺ {𝐡})) CnP 𝐾)β€˜π΅)))
7355, 72mpbid 231 . . . . . . 7 (πœ‘ β†’ (π‘₯ ∈ (𝐴 βˆͺ {𝐡}) ↦ if(π‘₯ = 𝐡, 𝐢, 𝑅)) ∈ (((𝐾 β†Ύt (𝐴 βˆͺ {𝐡})) CnP 𝐾)β€˜π΅))
74 limccnp2.d . . . . . . . 8 (πœ‘ β†’ 𝐷 ∈ ((π‘₯ ∈ 𝐴 ↦ 𝑆) limβ„‚ 𝐡))
7511adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ π‘Œ βŠ† β„‚)
7675, 38sseldd 3983 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ 𝑆 ∈ β„‚)
7759, 60, 76, 71, 6limcmpt 25392 . . . . . . . 8 (πœ‘ β†’ (𝐷 ∈ ((π‘₯ ∈ 𝐴 ↦ 𝑆) limβ„‚ 𝐡) ↔ (π‘₯ ∈ (𝐴 βˆͺ {𝐡}) ↦ if(π‘₯ = 𝐡, 𝐷, 𝑆)) ∈ (((𝐾 β†Ύt (𝐴 βˆͺ {𝐡})) CnP 𝐾)β€˜π΅)))
7874, 77mpbid 231 . . . . . . 7 (πœ‘ β†’ (π‘₯ ∈ (𝐴 βˆͺ {𝐡}) ↦ if(π‘₯ = 𝐡, 𝐷, 𝑆)) ∈ (((𝐾 β†Ύt (𝐴 βˆͺ {𝐡})) CnP 𝐾)β€˜π΅))
7964, 43, 43, 68, 73, 78txcnp 23116 . . . . . 6 (πœ‘ β†’ (π‘₯ ∈ (𝐴 βˆͺ {𝐡}) ↦ ⟨if(π‘₯ = 𝐡, 𝐢, 𝑅), if(π‘₯ = 𝐡, 𝐷, 𝑆)⟩) ∈ (((𝐾 β†Ύt (𝐴 βˆͺ {𝐡})) CnP (𝐾 Γ—t 𝐾))β€˜π΅))
809topontopi 22409 . . . . . . . 8 (𝐾 Γ—t 𝐾) ∈ Top
8180a1i 11 . . . . . . 7 (πœ‘ β†’ (𝐾 Γ—t 𝐾) ∈ Top)
8241fmpttd 7112 . . . . . . . 8 (πœ‘ β†’ (π‘₯ ∈ (𝐴 βˆͺ {𝐡}) ↦ ⟨if(π‘₯ = 𝐡, 𝐢, 𝑅), if(π‘₯ = 𝐡, 𝐷, 𝑆)⟩):(𝐴 βˆͺ {𝐡})⟢(𝑋 Γ— π‘Œ))
83 toponuni 22408 . . . . . . . . . 10 ((𝐾 β†Ύt (𝐴 βˆͺ {𝐡})) ∈ (TopOnβ€˜(𝐴 βˆͺ {𝐡})) β†’ (𝐴 βˆͺ {𝐡}) = βˆͺ (𝐾 β†Ύt (𝐴 βˆͺ {𝐡})))
8464, 83syl 17 . . . . . . . . 9 (πœ‘ β†’ (𝐴 βˆͺ {𝐡}) = βˆͺ (𝐾 β†Ύt (𝐴 βˆͺ {𝐡})))
8584feq2d 6701 . . . . . . . 8 (πœ‘ β†’ ((π‘₯ ∈ (𝐴 βˆͺ {𝐡}) ↦ ⟨if(π‘₯ = 𝐡, 𝐢, 𝑅), if(π‘₯ = 𝐡, 𝐷, 𝑆)⟩):(𝐴 βˆͺ {𝐡})⟢(𝑋 Γ— π‘Œ) ↔ (π‘₯ ∈ (𝐴 βˆͺ {𝐡}) ↦ ⟨if(π‘₯ = 𝐡, 𝐢, 𝑅), if(π‘₯ = 𝐡, 𝐷, 𝑆)⟩):βˆͺ (𝐾 β†Ύt (𝐴 βˆͺ {𝐡}))⟢(𝑋 Γ— π‘Œ)))
8682, 85mpbid 231 . . . . . . 7 (πœ‘ β†’ (π‘₯ ∈ (𝐴 βˆͺ {𝐡}) ↦ ⟨if(π‘₯ = 𝐡, 𝐢, 𝑅), if(π‘₯ = 𝐡, 𝐷, 𝑆)⟩):βˆͺ (𝐾 β†Ύt (𝐴 βˆͺ {𝐡}))⟢(𝑋 Γ— π‘Œ))
87 eqid 2733 . . . . . . . 8 βˆͺ (𝐾 β†Ύt (𝐴 βˆͺ {𝐡})) = βˆͺ (𝐾 β†Ύt (𝐴 βˆͺ {𝐡}))
889toponunii 22410 . . . . . . . 8 (β„‚ Γ— β„‚) = βˆͺ (𝐾 Γ—t 𝐾)
8987, 88cnprest2 22786 . . . . . . 7 (((𝐾 Γ—t 𝐾) ∈ Top ∧ (π‘₯ ∈ (𝐴 βˆͺ {𝐡}) ↦ ⟨if(π‘₯ = 𝐡, 𝐢, 𝑅), if(π‘₯ = 𝐡, 𝐷, 𝑆)⟩):βˆͺ (𝐾 β†Ύt (𝐴 βˆͺ {𝐡}))⟢(𝑋 Γ— π‘Œ) ∧ (𝑋 Γ— π‘Œ) βŠ† (β„‚ Γ— β„‚)) β†’ ((π‘₯ ∈ (𝐴 βˆͺ {𝐡}) ↦ ⟨if(π‘₯ = 𝐡, 𝐢, 𝑅), if(π‘₯ = 𝐡, 𝐷, 𝑆)⟩) ∈ (((𝐾 β†Ύt (𝐴 βˆͺ {𝐡})) CnP (𝐾 Γ—t 𝐾))β€˜π΅) ↔ (π‘₯ ∈ (𝐴 βˆͺ {𝐡}) ↦ ⟨if(π‘₯ = 𝐡, 𝐢, 𝑅), if(π‘₯ = 𝐡, 𝐷, 𝑆)⟩) ∈ (((𝐾 β†Ύt (𝐴 βˆͺ {𝐡})) CnP ((𝐾 Γ—t 𝐾) β†Ύt (𝑋 Γ— π‘Œ)))β€˜π΅)))
9081, 86, 13, 89syl3anc 1372 . . . . . 6 (πœ‘ β†’ ((π‘₯ ∈ (𝐴 βˆͺ {𝐡}) ↦ ⟨if(π‘₯ = 𝐡, 𝐢, 𝑅), if(π‘₯ = 𝐡, 𝐷, 𝑆)⟩) ∈ (((𝐾 β†Ύt (𝐴 βˆͺ {𝐡})) CnP (𝐾 Γ—t 𝐾))β€˜π΅) ↔ (π‘₯ ∈ (𝐴 βˆͺ {𝐡}) ↦ ⟨if(π‘₯ = 𝐡, 𝐢, 𝑅), if(π‘₯ = 𝐡, 𝐷, 𝑆)⟩) ∈ (((𝐾 β†Ύt (𝐴 βˆͺ {𝐡})) CnP ((𝐾 Γ—t 𝐾) β†Ύt (𝑋 Γ— π‘Œ)))β€˜π΅)))
9179, 90mpbid 231 . . . . 5 (πœ‘ β†’ (π‘₯ ∈ (𝐴 βˆͺ {𝐡}) ↦ ⟨if(π‘₯ = 𝐡, 𝐢, 𝑅), if(π‘₯ = 𝐡, 𝐷, 𝑆)⟩) ∈ (((𝐾 β†Ύt (𝐴 βˆͺ {𝐡})) CnP ((𝐾 Γ—t 𝐾) β†Ύt (𝑋 Γ— π‘Œ)))β€˜π΅))
925oveq2i 7417 . . . . . 6 ((𝐾 β†Ύt (𝐴 βˆͺ {𝐡})) CnP 𝐽) = ((𝐾 β†Ύt (𝐴 βˆͺ {𝐡})) CnP ((𝐾 Γ—t 𝐾) β†Ύt (𝑋 Γ— π‘Œ)))
9392fveq1i 6890 . . . . 5 (((𝐾 β†Ύt (𝐴 βˆͺ {𝐡})) CnP 𝐽)β€˜π΅) = (((𝐾 β†Ύt (𝐴 βˆͺ {𝐡})) CnP ((𝐾 Γ—t 𝐾) β†Ύt (𝑋 Γ— π‘Œ)))β€˜π΅)
9491, 93eleqtrrdi 2845 . . . 4 (πœ‘ β†’ (π‘₯ ∈ (𝐴 βˆͺ {𝐡}) ↦ ⟨if(π‘₯ = 𝐡, 𝐢, 𝑅), if(π‘₯ = 𝐡, 𝐷, 𝑆)⟩) ∈ (((𝐾 β†Ύt (𝐴 βˆͺ {𝐡})) CnP 𝐽)β€˜π΅))
95 iftrue 4534 . . . . . . . . 9 (π‘₯ = 𝐡 β†’ if(π‘₯ = 𝐡, 𝐢, 𝑅) = 𝐢)
96 iftrue 4534 . . . . . . . . 9 (π‘₯ = 𝐡 β†’ if(π‘₯ = 𝐡, 𝐷, 𝑆) = 𝐷)
9795, 96opeq12d 4881 . . . . . . . 8 (π‘₯ = 𝐡 β†’ ⟨if(π‘₯ = 𝐡, 𝐢, 𝑅), if(π‘₯ = 𝐡, 𝐷, 𝑆)⟩ = ⟨𝐢, 𝐷⟩)
98 eqid 2733 . . . . . . . 8 (π‘₯ ∈ (𝐴 βˆͺ {𝐡}) ↦ ⟨if(π‘₯ = 𝐡, 𝐢, 𝑅), if(π‘₯ = 𝐡, 𝐷, 𝑆)⟩) = (π‘₯ ∈ (𝐴 βˆͺ {𝐡}) ↦ ⟨if(π‘₯ = 𝐡, 𝐢, 𝑅), if(π‘₯ = 𝐡, 𝐷, 𝑆)⟩)
99 opex 5464 . . . . . . . 8 ⟨𝐢, 𝐷⟩ ∈ V
10097, 98, 99fvmpt 6996 . . . . . . 7 (𝐡 ∈ (𝐴 βˆͺ {𝐡}) β†’ ((π‘₯ ∈ (𝐴 βˆͺ {𝐡}) ↦ ⟨if(π‘₯ = 𝐡, 𝐢, 𝑅), if(π‘₯ = 𝐡, 𝐷, 𝑆)⟩)β€˜π΅) = ⟨𝐢, 𝐷⟩)
10168, 100syl 17 . . . . . 6 (πœ‘ β†’ ((π‘₯ ∈ (𝐴 βˆͺ {𝐡}) ↦ ⟨if(π‘₯ = 𝐡, 𝐢, 𝑅), if(π‘₯ = 𝐡, 𝐷, 𝑆)⟩)β€˜π΅) = ⟨𝐢, 𝐷⟩)
102101fveq2d 6893 . . . . 5 (πœ‘ β†’ ((𝐽 CnP 𝐾)β€˜((π‘₯ ∈ (𝐴 βˆͺ {𝐡}) ↦ ⟨if(π‘₯ = 𝐡, 𝐢, 𝑅), if(π‘₯ = 𝐡, 𝐷, 𝑆)⟩)β€˜π΅)) = ((𝐽 CnP 𝐾)β€˜βŸ¨πΆ, 𝐷⟩))
1031, 102eleqtrrd 2837 . . . 4 (πœ‘ β†’ 𝐻 ∈ ((𝐽 CnP 𝐾)β€˜((π‘₯ ∈ (𝐴 βˆͺ {𝐡}) ↦ ⟨if(π‘₯ = 𝐡, 𝐢, 𝑅), if(π‘₯ = 𝐡, 𝐷, 𝑆)⟩)β€˜π΅)))
104 cnpco 22763 . . . 4 (((π‘₯ ∈ (𝐴 βˆͺ {𝐡}) ↦ ⟨if(π‘₯ = 𝐡, 𝐢, 𝑅), if(π‘₯ = 𝐡, 𝐷, 𝑆)⟩) ∈ (((𝐾 β†Ύt (𝐴 βˆͺ {𝐡})) CnP 𝐽)β€˜π΅) ∧ 𝐻 ∈ ((𝐽 CnP 𝐾)β€˜((π‘₯ ∈ (𝐴 βˆͺ {𝐡}) ↦ ⟨if(π‘₯ = 𝐡, 𝐢, 𝑅), if(π‘₯ = 𝐡, 𝐷, 𝑆)⟩)β€˜π΅))) β†’ (𝐻 ∘ (π‘₯ ∈ (𝐴 βˆͺ {𝐡}) ↦ ⟨if(π‘₯ = 𝐡, 𝐢, 𝑅), if(π‘₯ = 𝐡, 𝐷, 𝑆)⟩)) ∈ (((𝐾 β†Ύt (𝐴 βˆͺ {𝐡})) CnP 𝐾)β€˜π΅))
10594, 103, 104syl2anc 585 . . 3 (πœ‘ β†’ (𝐻 ∘ (π‘₯ ∈ (𝐴 βˆͺ {𝐡}) ↦ ⟨if(π‘₯ = 𝐡, 𝐢, 𝑅), if(π‘₯ = 𝐡, 𝐷, 𝑆)⟩)) ∈ (((𝐾 β†Ύt (𝐴 βˆͺ {𝐡})) CnP 𝐾)β€˜π΅))
10652, 105eqeltrrd 2835 . 2 (πœ‘ β†’ (π‘₯ ∈ (𝐴 βˆͺ {𝐡}) ↦ if(π‘₯ = 𝐡, (𝐢𝐻𝐷), (𝑅𝐻𝑆))) ∈ (((𝐾 β†Ύt (𝐴 βˆͺ {𝐡})) CnP 𝐾)β€˜π΅))
10745adantr 482 . . . 4 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ 𝐻:(𝑋 Γ— π‘Œ)βŸΆβ„‚)
108107, 33, 38fovcdmd 7576 . . 3 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ (𝑅𝐻𝑆) ∈ β„‚)
10959, 60, 108, 71, 6limcmpt 25392 . 2 (πœ‘ β†’ ((𝐢𝐻𝐷) ∈ ((π‘₯ ∈ 𝐴 ↦ (𝑅𝐻𝑆)) limβ„‚ 𝐡) ↔ (π‘₯ ∈ (𝐴 βˆͺ {𝐡}) ↦ if(π‘₯ = 𝐡, (𝐢𝐻𝐷), (𝑅𝐻𝑆))) ∈ (((𝐾 β†Ύt (𝐴 βˆͺ {𝐡})) CnP 𝐾)β€˜π΅)))
110106, 109mpbird 257 1 (πœ‘ β†’ (𝐢𝐻𝐷) ∈ ((π‘₯ ∈ 𝐴 ↦ (𝑅𝐻𝑆)) limβ„‚ 𝐡))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∨ wo 846   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107   βˆͺ cun 3946   βŠ† wss 3948  ifcif 4528  {csn 4628  βŸ¨cop 4634  βˆͺ cuni 4908   ↦ cmpt 5231   Γ— cxp 5674  dom cdm 5676   ∘ ccom 5680  βŸΆwf 6537  β€˜cfv 6541  (class class class)co 7406  β„‚cc 11105   β†Ύt crest 17363  TopOpenctopn 17364  β„‚fldccnfld 20937  Topctop 22387  TopOnctopon 22404   CnP ccnp 22721   Γ—t ctx 23056   limβ„‚ climc 25371
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722  ax-cnex 11163  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-addrcl 11168  ax-mulcl 11169  ax-mulrcl 11170  ax-mulcom 11171  ax-addass 11172  ax-mulass 11173  ax-distr 11174  ax-i2m1 11175  ax-1ne0 11176  ax-1rid 11177  ax-rnegex 11178  ax-rrecex 11179  ax-cnre 11180  ax-pre-lttri 11181  ax-pre-lttrn 11182  ax-pre-ltadd 11183  ax-pre-mulgt0 11184  ax-pre-sup 11185
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-tp 4633  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6298  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-riota 7362  df-ov 7409  df-oprab 7410  df-mpo 7411  df-om 7853  df-1st 7972  df-2nd 7973  df-frecs 8263  df-wrecs 8294  df-recs 8368  df-rdg 8407  df-1o 8463  df-er 8700  df-map 8819  df-pm 8820  df-en 8937  df-dom 8938  df-sdom 8939  df-fin 8940  df-fi 9403  df-sup 9434  df-inf 9435  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11443  df-neg 11444  df-div 11869  df-nn 12210  df-2 12272  df-3 12273  df-4 12274  df-5 12275  df-6 12276  df-7 12277  df-8 12278  df-9 12279  df-n0 12470  df-z 12556  df-dec 12675  df-uz 12820  df-q 12930  df-rp 12972  df-xneg 13089  df-xadd 13090  df-xmul 13091  df-fz 13482  df-seq 13964  df-exp 14025  df-cj 15043  df-re 15044  df-im 15045  df-sqrt 15179  df-abs 15180  df-struct 17077  df-slot 17112  df-ndx 17124  df-base 17142  df-plusg 17207  df-mulr 17208  df-starv 17209  df-tset 17213  df-ple 17214  df-ds 17216  df-unif 17217  df-rest 17365  df-topn 17366  df-topgen 17386  df-psmet 20929  df-xmet 20930  df-met 20931  df-bl 20932  df-mopn 20933  df-cnfld 20938  df-top 22388  df-topon 22405  df-topsp 22427  df-bases 22441  df-cnp 22724  df-tx 23058  df-xms 23818  df-ms 23819  df-limc 25375
This theorem is referenced by:  dvcnp2  25429  dvaddbr  25447  dvmulbr  25448  dvcobr  25455  lhop1lem  25522  taylthlem2  25878  gg-dvcnp2  35163  gg-dvmulbr  35164  gg-dvcobr  35165
  Copyright terms: Public domain W3C validator