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

Theorem flfcnp2 22181
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, 19-Sep-2015.)
Hypotheses
Ref Expression
flfcnp2.j (𝜑𝐽 ∈ (TopOn‘𝑋))
flfcnp2.k (𝜑𝐾 ∈ (TopOn‘𝑌))
flfcnp2.l (𝜑𝐿 ∈ (Fil‘𝑍))
flfcnp2.a ((𝜑𝑥𝑍) → 𝐴𝑋)
flfcnp2.b ((𝜑𝑥𝑍) → 𝐵𝑌)
flfcnp2.r (𝜑𝑅 ∈ ((𝐽 fLimf 𝐿)‘(𝑥𝑍𝐴)))
flfcnp2.s (𝜑𝑆 ∈ ((𝐾 fLimf 𝐿)‘(𝑥𝑍𝐵)))
flfcnp2.o (𝜑𝑂 ∈ (((𝐽 ×t 𝐾) CnP 𝑁)‘⟨𝑅, 𝑆⟩))
Assertion
Ref Expression
flfcnp2 (𝜑 → (𝑅𝑂𝑆) ∈ ((𝑁 fLimf 𝐿)‘(𝑥𝑍 ↦ (𝐴𝑂𝐵))))
Distinct variable groups:   𝑥,𝑂   𝜑,𝑥   𝑥,𝑍   𝑥,𝑋   𝑥,𝑌
Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)   𝑅(𝑥)   𝑆(𝑥)   𝐽(𝑥)   𝐾(𝑥)   𝐿(𝑥)   𝑁(𝑥)

Proof of Theorem flfcnp2
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 df-ov 6908 . 2 (𝑅𝑂𝑆) = (𝑂‘⟨𝑅, 𝑆⟩)
2 flfcnp2.j . . . . 5 (𝜑𝐽 ∈ (TopOn‘𝑋))
3 flfcnp2.k . . . . 5 (𝜑𝐾 ∈ (TopOn‘𝑌))
4 txtopon 21765 . . . . 5 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)))
52, 3, 4syl2anc 579 . . . 4 (𝜑 → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)))
6 flfcnp2.l . . . 4 (𝜑𝐿 ∈ (Fil‘𝑍))
7 flfcnp2.a . . . . . 6 ((𝜑𝑥𝑍) → 𝐴𝑋)
8 flfcnp2.b . . . . . 6 ((𝜑𝑥𝑍) → 𝐵𝑌)
9 opelxpi 5379 . . . . . 6 ((𝐴𝑋𝐵𝑌) → ⟨𝐴, 𝐵⟩ ∈ (𝑋 × 𝑌))
107, 8, 9syl2anc 579 . . . . 5 ((𝜑𝑥𝑍) → ⟨𝐴, 𝐵⟩ ∈ (𝑋 × 𝑌))
1110fmpttd 6634 . . . 4 (𝜑 → (𝑥𝑍 ↦ ⟨𝐴, 𝐵⟩):𝑍⟶(𝑋 × 𝑌))
12 flfcnp2.r . . . . . 6 (𝜑𝑅 ∈ ((𝐽 fLimf 𝐿)‘(𝑥𝑍𝐴)))
13 flfcnp2.s . . . . . 6 (𝜑𝑆 ∈ ((𝐾 fLimf 𝐿)‘(𝑥𝑍𝐵)))
147fmpttd 6634 . . . . . . 7 (𝜑 → (𝑥𝑍𝐴):𝑍𝑋)
158fmpttd 6634 . . . . . . 7 (𝜑 → (𝑥𝑍𝐵):𝑍𝑌)
16 nfcv 2969 . . . . . . . 8 𝑦⟨((𝑥𝑍𝐴)‘𝑥), ((𝑥𝑍𝐵)‘𝑥)⟩
17 nffvmpt1 6444 . . . . . . . . 9 𝑥((𝑥𝑍𝐴)‘𝑦)
18 nffvmpt1 6444 . . . . . . . . 9 𝑥((𝑥𝑍𝐵)‘𝑦)
1917, 18nfop 4639 . . . . . . . 8 𝑥⟨((𝑥𝑍𝐴)‘𝑦), ((𝑥𝑍𝐵)‘𝑦)⟩
20 fveq2 6433 . . . . . . . . 9 (𝑥 = 𝑦 → ((𝑥𝑍𝐴)‘𝑥) = ((𝑥𝑍𝐴)‘𝑦))
21 fveq2 6433 . . . . . . . . 9 (𝑥 = 𝑦 → ((𝑥𝑍𝐵)‘𝑥) = ((𝑥𝑍𝐵)‘𝑦))
2220, 21opeq12d 4631 . . . . . . . 8 (𝑥 = 𝑦 → ⟨((𝑥𝑍𝐴)‘𝑥), ((𝑥𝑍𝐵)‘𝑥)⟩ = ⟨((𝑥𝑍𝐴)‘𝑦), ((𝑥𝑍𝐵)‘𝑦)⟩)
2316, 19, 22cbvmpt 4972 . . . . . . 7 (𝑥𝑍 ↦ ⟨((𝑥𝑍𝐴)‘𝑥), ((𝑥𝑍𝐵)‘𝑥)⟩) = (𝑦𝑍 ↦ ⟨((𝑥𝑍𝐴)‘𝑦), ((𝑥𝑍𝐵)‘𝑦)⟩)
242, 3, 6, 14, 15, 23txflf 22180 . . . . . 6 (𝜑 → (⟨𝑅, 𝑆⟩ ∈ (((𝐽 ×t 𝐾) fLimf 𝐿)‘(𝑥𝑍 ↦ ⟨((𝑥𝑍𝐴)‘𝑥), ((𝑥𝑍𝐵)‘𝑥)⟩)) ↔ (𝑅 ∈ ((𝐽 fLimf 𝐿)‘(𝑥𝑍𝐴)) ∧ 𝑆 ∈ ((𝐾 fLimf 𝐿)‘(𝑥𝑍𝐵)))))
2512, 13, 24mpbir2and 704 . . . . 5 (𝜑 → ⟨𝑅, 𝑆⟩ ∈ (((𝐽 ×t 𝐾) fLimf 𝐿)‘(𝑥𝑍 ↦ ⟨((𝑥𝑍𝐴)‘𝑥), ((𝑥𝑍𝐵)‘𝑥)⟩)))
26 simpr 479 . . . . . . . . 9 ((𝜑𝑥𝑍) → 𝑥𝑍)
27 eqid 2825 . . . . . . . . . 10 (𝑥𝑍𝐴) = (𝑥𝑍𝐴)
2827fvmpt2 6538 . . . . . . . . 9 ((𝑥𝑍𝐴𝑋) → ((𝑥𝑍𝐴)‘𝑥) = 𝐴)
2926, 7, 28syl2anc 579 . . . . . . . 8 ((𝜑𝑥𝑍) → ((𝑥𝑍𝐴)‘𝑥) = 𝐴)
30 eqid 2825 . . . . . . . . . 10 (𝑥𝑍𝐵) = (𝑥𝑍𝐵)
3130fvmpt2 6538 . . . . . . . . 9 ((𝑥𝑍𝐵𝑌) → ((𝑥𝑍𝐵)‘𝑥) = 𝐵)
3226, 8, 31syl2anc 579 . . . . . . . 8 ((𝜑𝑥𝑍) → ((𝑥𝑍𝐵)‘𝑥) = 𝐵)
3329, 32opeq12d 4631 . . . . . . 7 ((𝜑𝑥𝑍) → ⟨((𝑥𝑍𝐴)‘𝑥), ((𝑥𝑍𝐵)‘𝑥)⟩ = ⟨𝐴, 𝐵⟩)
3433mpteq2dva 4967 . . . . . 6 (𝜑 → (𝑥𝑍 ↦ ⟨((𝑥𝑍𝐴)‘𝑥), ((𝑥𝑍𝐵)‘𝑥)⟩) = (𝑥𝑍 ↦ ⟨𝐴, 𝐵⟩))
3534fveq2d 6437 . . . . 5 (𝜑 → (((𝐽 ×t 𝐾) fLimf 𝐿)‘(𝑥𝑍 ↦ ⟨((𝑥𝑍𝐴)‘𝑥), ((𝑥𝑍𝐵)‘𝑥)⟩)) = (((𝐽 ×t 𝐾) fLimf 𝐿)‘(𝑥𝑍 ↦ ⟨𝐴, 𝐵⟩)))
3625, 35eleqtrd 2908 . . . 4 (𝜑 → ⟨𝑅, 𝑆⟩ ∈ (((𝐽 ×t 𝐾) fLimf 𝐿)‘(𝑥𝑍 ↦ ⟨𝐴, 𝐵⟩)))
37 flfcnp2.o . . . 4 (𝜑𝑂 ∈ (((𝐽 ×t 𝐾) CnP 𝑁)‘⟨𝑅, 𝑆⟩))
38 flfcnp 22178 . . . 4 ((((𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)) ∧ 𝐿 ∈ (Fil‘𝑍) ∧ (𝑥𝑍 ↦ ⟨𝐴, 𝐵⟩):𝑍⟶(𝑋 × 𝑌)) ∧ (⟨𝑅, 𝑆⟩ ∈ (((𝐽 ×t 𝐾) fLimf 𝐿)‘(𝑥𝑍 ↦ ⟨𝐴, 𝐵⟩)) ∧ 𝑂 ∈ (((𝐽 ×t 𝐾) CnP 𝑁)‘⟨𝑅, 𝑆⟩))) → (𝑂‘⟨𝑅, 𝑆⟩) ∈ ((𝑁 fLimf 𝐿)‘(𝑂 ∘ (𝑥𝑍 ↦ ⟨𝐴, 𝐵⟩))))
395, 6, 11, 36, 37, 38syl32anc 1501 . . 3 (𝜑 → (𝑂‘⟨𝑅, 𝑆⟩) ∈ ((𝑁 fLimf 𝐿)‘(𝑂 ∘ (𝑥𝑍 ↦ ⟨𝐴, 𝐵⟩))))
40 eqidd 2826 . . . . 5 (𝜑 → (𝑥𝑍 ↦ ⟨𝐴, 𝐵⟩) = (𝑥𝑍 ↦ ⟨𝐴, 𝐵⟩))
41 cnptop2 21418 . . . . . . . . 9 (𝑂 ∈ (((𝐽 ×t 𝐾) CnP 𝑁)‘⟨𝑅, 𝑆⟩) → 𝑁 ∈ Top)
4237, 41syl 17 . . . . . . . 8 (𝜑𝑁 ∈ Top)
43 eqid 2825 . . . . . . . . 9 𝑁 = 𝑁
4443toptopon 21092 . . . . . . . 8 (𝑁 ∈ Top ↔ 𝑁 ∈ (TopOn‘ 𝑁))
4542, 44sylib 210 . . . . . . 7 (𝜑𝑁 ∈ (TopOn‘ 𝑁))
46 cnpf2 21425 . . . . . . 7 (((𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)) ∧ 𝑁 ∈ (TopOn‘ 𝑁) ∧ 𝑂 ∈ (((𝐽 ×t 𝐾) CnP 𝑁)‘⟨𝑅, 𝑆⟩)) → 𝑂:(𝑋 × 𝑌)⟶ 𝑁)
475, 45, 37, 46syl3anc 1494 . . . . . 6 (𝜑𝑂:(𝑋 × 𝑌)⟶ 𝑁)
4847feqmptd 6496 . . . . 5 (𝜑𝑂 = (𝑦 ∈ (𝑋 × 𝑌) ↦ (𝑂𝑦)))
49 fveq2 6433 . . . . . 6 (𝑦 = ⟨𝐴, 𝐵⟩ → (𝑂𝑦) = (𝑂‘⟨𝐴, 𝐵⟩))
50 df-ov 6908 . . . . . 6 (𝐴𝑂𝐵) = (𝑂‘⟨𝐴, 𝐵⟩)
5149, 50syl6eqr 2879 . . . . 5 (𝑦 = ⟨𝐴, 𝐵⟩ → (𝑂𝑦) = (𝐴𝑂𝐵))
5210, 40, 48, 51fmptco 6646 . . . 4 (𝜑 → (𝑂 ∘ (𝑥𝑍 ↦ ⟨𝐴, 𝐵⟩)) = (𝑥𝑍 ↦ (𝐴𝑂𝐵)))
5352fveq2d 6437 . . 3 (𝜑 → ((𝑁 fLimf 𝐿)‘(𝑂 ∘ (𝑥𝑍 ↦ ⟨𝐴, 𝐵⟩))) = ((𝑁 fLimf 𝐿)‘(𝑥𝑍 ↦ (𝐴𝑂𝐵))))
5439, 53eleqtrd 2908 . 2 (𝜑 → (𝑂‘⟨𝑅, 𝑆⟩) ∈ ((𝑁 fLimf 𝐿)‘(𝑥𝑍 ↦ (𝐴𝑂𝐵))))
551, 54syl5eqel 2910 1 (𝜑 → (𝑅𝑂𝑆) ∈ ((𝑁 fLimf 𝐿)‘(𝑥𝑍 ↦ (𝐴𝑂𝐵))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 386   = wceq 1656  wcel 2164  cop 4403   cuni 4658  cmpt 4952   × cxp 5340  ccom 5346  wf 6119  cfv 6123  (class class class)co 6905  Topctop 21068  TopOnctopon 21085   CnP ccnp 21400   ×t ctx 21734  Filcfil 22019   fLimf cflf 22109
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-8 2166  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803  ax-rep 4994  ax-sep 5005  ax-nul 5013  ax-pow 5065  ax-pr 5127  ax-un 7209
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-nel 3103  df-ral 3122  df-rex 3123  df-reu 3124  df-rab 3126  df-v 3416  df-sbc 3663  df-csb 3758  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4145  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-op 4404  df-uni 4659  df-iun 4742  df-br 4874  df-opab 4936  df-mpt 4953  df-id 5250  df-xp 5348  df-rel 5349  df-cnv 5350  df-co 5351  df-dm 5352  df-rn 5353  df-res 5354  df-ima 5355  df-iota 6086  df-fun 6125  df-fn 6126  df-f 6127  df-f1 6128  df-fo 6129  df-f1o 6130  df-fv 6131  df-ov 6908  df-oprab 6909  df-mpt2 6910  df-1st 7428  df-2nd 7429  df-map 8124  df-topgen 16457  df-fbas 20103  df-fg 20104  df-top 21069  df-topon 21086  df-bases 21121  df-ntr 21195  df-nei 21273  df-cnp 21403  df-tx 21736  df-fil 22020  df-fm 22112  df-flim 22113  df-flf 22114
This theorem is referenced by:  tsmsadd  22320
  Copyright terms: Public domain W3C validator