lmcn2

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, 15-May-2014)

	Ref	Expression
Hypotheses	txlm.z	$⊢ Z = ℤ_{\geq M}$
	txlm.m	$⊢ φ \to M \in ℤ$
	txlm.j	$⊢ φ \to J \in TopOn (X)$
	txlm.k	$⊢ φ \to K \in TopOn (Y)$
	txlm.f	$⊢ φ \to F : Z ⟶ X$
	txlm.g	$⊢ φ \to G : Z ⟶ Y$
	lmcn2.fl	$⊢ φ \to F \underset{t}{⇝} (J) R$
	lmcn2.gl	$⊢ φ \to G \underset{t}{⇝} (K) S$
	lmcn2.o	$⊢ φ \to O \in ((J \times_{t} K) Cn N)$
	lmcn2.h	$⊢ H = (n \in Z ⟼ F (n) O G (n))$
Assertion	lmcn2	$⊢ φ \to H \underset{t}{⇝} (N) (R O S)$

Proof

Step	Hyp	Ref	Expression
1		txlm.z	$⊢ Z = ℤ_{\geq M}$
2		txlm.m	$⊢ φ \to M \in ℤ$
3		txlm.j	$⊢ φ \to J \in TopOn (X)$
4		txlm.k	$⊢ φ \to K \in TopOn (Y)$
5		txlm.f	$⊢ φ \to F : Z ⟶ X$
6		txlm.g	$⊢ φ \to G : Z ⟶ Y$
7		lmcn2.fl	$⊢ φ \to F \underset{t}{⇝} (J) R$
8		lmcn2.gl	$⊢ φ \to G \underset{t}{⇝} (K) S$
9		lmcn2.o	$⊢ φ \to O \in ((J \times_{t} K) Cn N)$
10		lmcn2.h	$⊢ H = (n \in Z ⟼ F (n) O G (n))$
11	5	ffvelrnda	$⊢ (φ \land n \in Z) \to F (n) \in X$
12	6	ffvelrnda	$⊢ (φ \land n \in Z) \to G (n) \in Y$
13	11 12	opelxpd	$⊢ (φ \land n \in Z) \to ⟨F (n), G (n)⟩ \in (X \times Y)$
14		eqidd	$⊢ φ \to (n \in Z ⟼ ⟨F (n), G (n)⟩) = (n \in Z ⟼ ⟨F (n), G (n)⟩)$
15		txtopon	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to J \times_{t} K \in TopOn (X \times Y)$
16	3 4 15	syl2anc	$⊢ φ \to J \times_{t} K \in TopOn (X \times Y)$
17		cntop2	$⊢ O \in ((J \times_{t} K) Cn N) \to N \in Top$
18	9 17	syl	$⊢ φ \to N \in Top$
19		toptopon2	$⊢ N \in Top \leftrightarrow N \in TopOn (⋃ N)$
20	18 19	sylib	$⊢ φ \to N \in TopOn (⋃ N)$
21		cnf2	$⊢ (J \times_{t} K \in TopOn (X \times Y) \land N \in TopOn (⋃ N) \land O \in ((J \times_{t} K) Cn N)) \to O : X \times Y ⟶ ⋃ N$
22	16 20 9 21	syl3anc	$⊢ φ \to O : X \times Y ⟶ ⋃ N$
23	22	feqmptd	$⊢ φ \to O = (x \in (X \times Y) ⟼ O (x))$
24		fveq2	$⊢ x = ⟨F (n), G (n)⟩ \to O (x) = O (⟨F (n), G (n)⟩)$
25		df-ov	$⊢ F (n) O G (n) = O (⟨F (n), G (n)⟩)$
26	24 25	eqtr4di	$⊢ x = ⟨F (n), G (n)⟩ \to O (x) = F (n) O G (n)$
27	13 14 23 26	fmptco	$⊢ φ \to O \circ (n \in Z ⟼ ⟨F (n), G (n)⟩) = (n \in Z ⟼ F (n) O G (n))$
28	27 10	eqtr4di	$⊢ φ \to O \circ (n \in Z ⟼ ⟨F (n), G (n)⟩) = H$
29		eqid	$⊢ (n \in Z ⟼ ⟨F (n), G (n)⟩) = (n \in Z ⟼ ⟨F (n), G (n)⟩)$
30	1 2 3 4 5 6 29	txlm	$⊢ φ \to ((F \underset{t}{⇝} (J) R \land G \underset{t}{⇝} (K) S) \leftrightarrow (n \in Z ⟼ ⟨F (n), G (n)⟩) \underset{t}{⇝} (J \times_{t} K) ⟨R, S⟩)$
31	7 8 30	mpbi2and	$⊢ φ \to (n \in Z ⟼ ⟨F (n), G (n)⟩) \underset{t}{⇝} (J \times_{t} K) ⟨R, S⟩$
32	31 9	lmcn	$⊢ φ \to (O \circ (n \in Z ⟼ ⟨F (n), G (n)⟩)) \underset{t}{⇝} (N) O (⟨R, S⟩)$
33	28 32	eqbrtrrd	$⊢ φ \to H \underset{t}{⇝} (N) O (⟨R, S⟩)$
34		df-ov	$⊢ R O S = O (⟨R, S⟩)$
35	33 34	breqtrrdi	$⊢ φ \to H \underset{t}{⇝} (N) (R O S)$

Metamath Proof Explorer

Theorem lmcn2

Proof