Theorem flfcnp2 21621

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.

Step	Hyp	Ref	Expression
1		df-ov 6552	. 2 ⊢ (𝑅𝑂𝑆) = (𝑂‘⟨𝑅, 𝑆⟩)
2		flfcnp2.j	. . . . 5 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))
3		flfcnp2.k	. . . . 5 ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌))
4		txtopon 21204	. . . . 5 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)))
5	2, 3, 4	syl2anc 691	. . . 4 ⊢ (𝜑 → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)))
6		flfcnp2.l	. . . 4 ⊢ (𝜑 → 𝐿 ∈ (Fil‘𝑍))
7		flfcnp2.a	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐴 ∈ 𝑋)
8		flfcnp2.b	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐵 ∈ 𝑌)
9		opelxpi 5072	. . . . . 6 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → ⟨𝐴, 𝐵⟩ ∈ (𝑋 × 𝑌))
10	7, 8, 9	syl2anc 691	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → ⟨𝐴, 𝐵⟩ ∈ (𝑋 × 𝑌))
11		eqid 2610	. . . . 5 ⊢ (𝑥 ∈ 𝑍 ↦ ⟨𝐴, 𝐵⟩) = (𝑥 ∈ 𝑍 ↦ ⟨𝐴, 𝐵⟩)
12	10, 11	fmptd 6292	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝑍 ↦ ⟨𝐴, 𝐵⟩):𝑍⟶(𝑋 × 𝑌))
13		flfcnp2.r	. . . . . 6 ⊢ (𝜑 → 𝑅 ∈ ((𝐽 fLimf 𝐿)‘(𝑥 ∈ 𝑍 ↦ 𝐴)))
14		flfcnp2.s	. . . . . 6 ⊢ (𝜑 → 𝑆 ∈ ((𝐾 fLimf 𝐿)‘(𝑥 ∈ 𝑍 ↦ 𝐵)))
15		eqid 2610	. . . . . . . 8 ⊢ (𝑥 ∈ 𝑍 ↦ 𝐴) = (𝑥 ∈ 𝑍 ↦ 𝐴)
16	7, 15	fmptd 6292	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝑍 ↦ 𝐴):𝑍⟶𝑋)
17		eqid 2610	. . . . . . . 8 ⊢ (𝑥 ∈ 𝑍 ↦ 𝐵) = (𝑥 ∈ 𝑍 ↦ 𝐵)
18	8, 17	fmptd 6292	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝑍 ↦ 𝐵):𝑍⟶𝑌)
19		nfcv 2751	. . . . . . . 8 ⊢ Ⅎ𝑦⟨((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑥), ((𝑥 ∈ 𝑍 ↦ 𝐵)‘𝑥)⟩
20		nffvmpt1 6111	. . . . . . . . 9 ⊢ Ⅎ𝑥((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑦)
21		nffvmpt1 6111	. . . . . . . . 9 ⊢ Ⅎ𝑥((𝑥 ∈ 𝑍 ↦ 𝐵)‘𝑦)
22	20, 21	nfop 4356	. . . . . . . 8 ⊢ Ⅎ𝑥⟨((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑦), ((𝑥 ∈ 𝑍 ↦ 𝐵)‘𝑦)⟩
23		fveq2 6103	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑥) = ((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑦))
24		fveq2 6103	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝑍 ↦ 𝐵)‘𝑥) = ((𝑥 ∈ 𝑍 ↦ 𝐵)‘𝑦))
25	23, 24	opeq12d 4348	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → ⟨((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑥), ((𝑥 ∈ 𝑍 ↦ 𝐵)‘𝑥)⟩ = ⟨((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑦), ((𝑥 ∈ 𝑍 ↦ 𝐵)‘𝑦)⟩)
26	19, 22, 25	cbvmpt 4677	. . . . . . 7 ⊢ (𝑥 ∈ 𝑍 ↦ ⟨((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑥), ((𝑥 ∈ 𝑍 ↦ 𝐵)‘𝑥)⟩) = (𝑦 ∈ 𝑍 ↦ ⟨((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑦), ((𝑥 ∈ 𝑍 ↦ 𝐵)‘𝑦)⟩)
27	2, 3, 6, 16, 18, 26	txflf 21620	. . . . . 6 ⊢ (𝜑 → (⟨𝑅, 𝑆⟩ ∈ (((𝐽 ×t 𝐾) fLimf 𝐿)‘(𝑥 ∈ 𝑍 ↦ ⟨((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑥), ((𝑥 ∈ 𝑍 ↦ 𝐵)‘𝑥)⟩)) ↔ (𝑅 ∈ ((𝐽 fLimf 𝐿)‘(𝑥 ∈ 𝑍 ↦ 𝐴)) ∧ 𝑆 ∈ ((𝐾 fLimf 𝐿)‘(𝑥 ∈ 𝑍 ↦ 𝐵)))))
28	13, 14, 27	mpbir2and 959	. . . . 5 ⊢ (𝜑 → ⟨𝑅, 𝑆⟩ ∈ (((𝐽 ×t 𝐾) fLimf 𝐿)‘(𝑥 ∈ 𝑍 ↦ ⟨((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑥), ((𝑥 ∈ 𝑍 ↦ 𝐵)‘𝑥)⟩)))
29		simpr 476	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝑥 ∈ 𝑍)
30	15	fvmpt2 6200	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋) → ((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑥) = 𝐴)
31	29, 7, 30	syl2anc 691	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → ((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑥) = 𝐴)
32	17	fvmpt2 6200	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝑍 ∧ 𝐵 ∈ 𝑌) → ((𝑥 ∈ 𝑍 ↦ 𝐵)‘𝑥) = 𝐵)
33	29, 8, 32	syl2anc 691	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → ((𝑥 ∈ 𝑍 ↦ 𝐵)‘𝑥) = 𝐵)
34	31, 33	opeq12d 4348	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → ⟨((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑥), ((𝑥 ∈ 𝑍 ↦ 𝐵)‘𝑥)⟩ = ⟨𝐴, 𝐵⟩)
35	34	mpteq2dva 4672	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝑍 ↦ ⟨((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑥), ((𝑥 ∈ 𝑍 ↦ 𝐵)‘𝑥)⟩) = (𝑥 ∈ 𝑍 ↦ ⟨𝐴, 𝐵⟩))
36	35	fveq2d 6107	. . . . 5 ⊢ (𝜑 → (((𝐽 ×t 𝐾) fLimf 𝐿)‘(𝑥 ∈ 𝑍 ↦ ⟨((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑥), ((𝑥 ∈ 𝑍 ↦ 𝐵)‘𝑥)⟩)) = (((𝐽 ×t 𝐾) fLimf 𝐿)‘(𝑥 ∈ 𝑍 ↦ ⟨𝐴, 𝐵⟩)))
37	28, 36	eleqtrd 2690	. . . 4 ⊢ (𝜑 → ⟨𝑅, 𝑆⟩ ∈ (((𝐽 ×t 𝐾) fLimf 𝐿)‘(𝑥 ∈ 𝑍 ↦ ⟨𝐴, 𝐵⟩)))
38		flfcnp2.o	. . . 4 ⊢ (𝜑 → 𝑂 ∈ (((𝐽 ×t 𝐾) CnP 𝑁)‘⟨𝑅, 𝑆⟩))
39		flfcnp 21618	. . . 4 ⊢ ((((𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)) ∧ 𝐿 ∈ (Fil‘𝑍) ∧ (𝑥 ∈ 𝑍 ↦ ⟨𝐴, 𝐵⟩):𝑍⟶(𝑋 × 𝑌)) ∧ (⟨𝑅, 𝑆⟩ ∈ (((𝐽 ×t 𝐾) fLimf 𝐿)‘(𝑥 ∈ 𝑍 ↦ ⟨𝐴, 𝐵⟩)) ∧ 𝑂 ∈ (((𝐽 ×t 𝐾) CnP 𝑁)‘⟨𝑅, 𝑆⟩))) → (𝑂‘⟨𝑅, 𝑆⟩) ∈ ((𝑁 fLimf 𝐿)‘(𝑂 ∘ (𝑥 ∈ 𝑍 ↦ ⟨𝐴, 𝐵⟩))))
40	5, 6, 12, 37, 38, 39	syl32anc 1326	. . 3 ⊢ (𝜑 → (𝑂‘⟨𝑅, 𝑆⟩) ∈ ((𝑁 fLimf 𝐿)‘(𝑂 ∘ (𝑥 ∈ 𝑍 ↦ ⟨𝐴, 𝐵⟩))))
41		eqidd 2611	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ 𝑍 ↦ ⟨𝐴, 𝐵⟩) = (𝑥 ∈ 𝑍 ↦ ⟨𝐴, 𝐵⟩))
42		cnptop2 20857	. . . . . . . . 9 ⊢ (𝑂 ∈ (((𝐽 ×t 𝐾) CnP 𝑁)‘⟨𝑅, 𝑆⟩) → 𝑁 ∈ Top)
43	38, 42	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ Top)
44		eqid 2610	. . . . . . . . 9 ⊢ ∪ 𝑁 = ∪ 𝑁
45	44	toptopon 20548	. . . . . . . 8 ⊢ (𝑁 ∈ Top ↔ 𝑁 ∈ (TopOn‘∪ 𝑁))
46	43, 45	sylib 207	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ (TopOn‘∪ 𝑁))
47		cnpf2 20864	. . . . . . 7 ⊢ (((𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)) ∧ 𝑁 ∈ (TopOn‘∪ 𝑁) ∧ 𝑂 ∈ (((𝐽 ×t 𝐾) CnP 𝑁)‘⟨𝑅, 𝑆⟩)) → 𝑂:(𝑋 × 𝑌)⟶∪ 𝑁)
48	5, 46, 38, 47	syl3anc 1318	. . . . . 6 ⊢ (𝜑 → 𝑂:(𝑋 × 𝑌)⟶∪ 𝑁)
49	48	feqmptd 6159	. . . . 5 ⊢ (𝜑 → 𝑂 = (𝑦 ∈ (𝑋 × 𝑌) ↦ (𝑂‘𝑦)))
50		fveq2 6103	. . . . . 6 ⊢ (𝑦 = ⟨𝐴, 𝐵⟩ → (𝑂‘𝑦) = (𝑂‘⟨𝐴, 𝐵⟩))
51		df-ov 6552	. . . . . 6 ⊢ (𝐴𝑂𝐵) = (𝑂‘⟨𝐴, 𝐵⟩)
52	50, 51	syl6eqr 2662	. . . . 5 ⊢ (𝑦 = ⟨𝐴, 𝐵⟩ → (𝑂‘𝑦) = (𝐴𝑂𝐵))
53	10, 41, 49, 52	fmptco 6303	. . . 4 ⊢ (𝜑 → (𝑂 ∘ (𝑥 ∈ 𝑍 ↦ ⟨𝐴, 𝐵⟩)) = (𝑥 ∈ 𝑍 ↦ (𝐴𝑂𝐵)))
54	53	fveq2d 6107	. . 3 ⊢ (𝜑 → ((𝑁 fLimf 𝐿)‘(𝑂 ∘ (𝑥 ∈ 𝑍 ↦ ⟨𝐴, 𝐵⟩))) = ((𝑁 fLimf 𝐿)‘(𝑥 ∈ 𝑍 ↦ (𝐴𝑂𝐵))))
55	40, 54	eleqtrd 2690	. 2 ⊢ (𝜑 → (𝑂‘⟨𝑅, 𝑆⟩) ∈ ((𝑁 fLimf 𝐿)‘(𝑥 ∈ 𝑍 ↦ (𝐴𝑂𝐵))))
56	1, 55	syl5eqel 2692	1 ⊢ (𝜑 → (𝑅𝑂𝑆) ∈ ((𝑁 fLimf 𝐿)‘(𝑥 ∈ 𝑍 ↦ (𝐴𝑂𝐵))))

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1475   ∈ wcel 1977  ⟨cop 4131  ∪ cuni 4372   ↦ cmpt 4643   × cxp 5036   ∘ ccom 5042  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549  Topctop 20517  TopOnctopon 20518   CnP ccnp 20839   ×_t ctx 21173  Filcfil 21459   fLimf cflf 21549

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-1st 7059  df-2nd 7060  df-map 7746  df-topgen 15927  df-fbas 19564  df-fg 19565  df-top 20521  df-bases 20522  df-topon 20523  df-ntr 20634  df-nei 20712  df-cnp 20842  df-tx 21175  df-fil 21460  df-fm 21552  df-flim 21553  df-flf 21554

This theorem is referenced by:  tsmsadd  21760