flfcnp2

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)

	Ref	Expression
Hypotheses	flfcnp2.j	$⊢ φ \to J \in TopOn (X)$
	flfcnp2.k	$⊢ φ \to K \in TopOn (Y)$
	flfcnp2.l	$⊢ φ \to L \in Fil (Z)$
	flfcnp2.a	$⊢ (φ \land x \in Z) \to A \in X$
	flfcnp2.b	$⊢ (φ \land x \in Z) \to B \in Y$
	flfcnp2.r	$⊢ φ \to R \in (J fLimf L) ((x \in Z ⟼ A))$
	flfcnp2.s	$⊢ φ \to S \in (K fLimf L) ((x \in Z ⟼ B))$
	flfcnp2.o	$⊢ φ \to O \in ((J \times_{t} K) CnP N) (⟨R, S⟩)$
Assertion	flfcnp2	$⊢ φ \to R O S \in (N fLimf L) ((x \in Z ⟼ A O B))$

Proof

Step	Hyp	Ref	Expression
1		flfcnp2.j	$⊢ φ \to J \in TopOn (X)$
2		flfcnp2.k	$⊢ φ \to K \in TopOn (Y)$
3		flfcnp2.l	$⊢ φ \to L \in Fil (Z)$
4		flfcnp2.a	$⊢ (φ \land x \in Z) \to A \in X$
5		flfcnp2.b	$⊢ (φ \land x \in Z) \to B \in Y$
6		flfcnp2.r	$⊢ φ \to R \in (J fLimf L) ((x \in Z ⟼ A))$
7		flfcnp2.s	$⊢ φ \to S \in (K fLimf L) ((x \in Z ⟼ B))$
8		flfcnp2.o	$⊢ φ \to O \in ((J \times_{t} K) CnP N) (⟨R, S⟩)$
9		df-ov	$⊢ R O S = O (⟨R, S⟩)$
10		txtopon	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to J \times_{t} K \in TopOn (X \times Y)$
11	1 2 10	syl2anc	$⊢ φ \to J \times_{t} K \in TopOn (X \times Y)$
12	4 5	opelxpd	$⊢ (φ \land x \in Z) \to ⟨A, B⟩ \in (X \times Y)$
13	12	fmpttd	$⊢ φ \to (x \in Z ⟼ ⟨A, B⟩) : Z ⟶ X \times Y$
14	4	fmpttd	$⊢ φ \to (x \in Z ⟼ A) : Z ⟶ X$
15	5	fmpttd	$⊢ φ \to (x \in Z ⟼ B) : Z ⟶ Y$
16		nfcv	$⊢ \underline{Ⅎ} y ⟨(x \in Z ⟼ A) (x), (x \in Z ⟼ B) (x)⟩$
17		nffvmpt1	$⊢ \underline{Ⅎ} x (x \in Z ⟼ A) (y)$
18		nffvmpt1	$⊢ \underline{Ⅎ} x (x \in Z ⟼ B) (y)$
19	17 18	nfop	$⊢ \underline{Ⅎ} x ⟨(x \in Z ⟼ A) (y), (x \in Z ⟼ B) (y)⟩$
20		fveq2	$⊢ x = y \to (x \in Z ⟼ A) (x) = (x \in Z ⟼ A) (y)$
21		fveq2	$⊢ x = y \to (x \in Z ⟼ B) (x) = (x \in Z ⟼ B) (y)$
22	20 21	opeq12d	$⊢ x = y \to ⟨(x \in Z ⟼ A) (x), (x \in Z ⟼ B) (x)⟩ = ⟨(x \in Z ⟼ A) (y), (x \in Z ⟼ B) (y)⟩$
23	16 19 22	cbvmpt	$⊢ (x \in Z ⟼ ⟨(x \in Z ⟼ A) (x), (x \in Z ⟼ B) (x)⟩) = (y \in Z ⟼ ⟨(x \in Z ⟼ A) (y), (x \in Z ⟼ B) (y)⟩)$
24	1 2 3 14 15 23	txflf	$⊢ φ \to (⟨R, S⟩ \in ((J \times_{t} K) fLimf L) ((x \in Z ⟼ ⟨(x \in Z ⟼ A) (x), (x \in Z ⟼ B) (x)⟩)) \leftrightarrow (R \in (J fLimf L) ((x \in Z ⟼ A)) \land S \in (K fLimf L) ((x \in Z ⟼ B))))$
25	6 7 24	mpbir2and	$⊢ φ \to ⟨R, S⟩ \in ((J \times_{t} K) fLimf L) ((x \in Z ⟼ ⟨(x \in Z ⟼ A) (x), (x \in Z ⟼ B) (x)⟩))$
26		simpr	$⊢ (φ \land x \in Z) \to x \in Z$
27		eqid	$⊢ (x \in Z ⟼ A) = (x \in Z ⟼ A)$
28	27	fvmpt2	$⊢ (x \in Z \land A \in X) \to (x \in Z ⟼ A) (x) = A$
29	26 4 28	syl2anc	$⊢ (φ \land x \in Z) \to (x \in Z ⟼ A) (x) = A$
30		eqid	$⊢ (x \in Z ⟼ B) = (x \in Z ⟼ B)$
31	30	fvmpt2	$⊢ (x \in Z \land B \in Y) \to (x \in Z ⟼ B) (x) = B$
32	26 5 31	syl2anc	$⊢ (φ \land x \in Z) \to (x \in Z ⟼ B) (x) = B$
33	29 32	opeq12d	$⊢ (φ \land x \in Z) \to ⟨(x \in Z ⟼ A) (x), (x \in Z ⟼ B) (x)⟩ = ⟨A, B⟩$
34	33	mpteq2dva	$⊢ φ \to (x \in Z ⟼ ⟨(x \in Z ⟼ A) (x), (x \in Z ⟼ B) (x)⟩) = (x \in Z ⟼ ⟨A, B⟩)$
35	34	fveq2d	$⊢ φ \to ((J \times_{t} K) fLimf L) ((x \in Z ⟼ ⟨(x \in Z ⟼ A) (x), (x \in Z ⟼ B) (x)⟩)) = ((J \times_{t} K) fLimf L) ((x \in Z ⟼ ⟨A, B⟩))$
36	25 35	eleqtrd	$⊢ φ \to ⟨R, S⟩ \in ((J \times_{t} K) fLimf L) ((x \in Z ⟼ ⟨A, B⟩))$
37		flfcnp	$⊢ ((J \times_{t} K \in TopOn (X \times Y) \land L \in Fil (Z) \land (x \in Z ⟼ ⟨A, B⟩) : Z ⟶ X \times Y) \land (⟨R, S⟩ \in ((J \times_{t} K) fLimf L) ((x \in Z ⟼ ⟨A, B⟩)) \land O \in ((J \times_{t} K) CnP N) (⟨R, S⟩))) \to O (⟨R, S⟩) \in (N fLimf L) (O \circ (x \in Z ⟼ ⟨A, B⟩))$
38	11 3 13 36 8 37	syl32anc	$⊢ φ \to O (⟨R, S⟩) \in (N fLimf L) (O \circ (x \in Z ⟼ ⟨A, B⟩))$
39		eqidd	$⊢ φ \to (x \in Z ⟼ ⟨A, B⟩) = (x \in Z ⟼ ⟨A, B⟩)$
40		cnptop2	$⊢ O \in ((J \times_{t} K) CnP N) (⟨R, S⟩) \to N \in Top$
41	8 40	syl	$⊢ φ \to N \in Top$
42		toptopon2	$⊢ N \in Top \leftrightarrow N \in TopOn (⋃ N)$
43	41 42	sylib	$⊢ φ \to N \in TopOn (⋃ N)$
44		cnpf2	$⊢ (J \times_{t} K \in TopOn (X \times Y) \land N \in TopOn (⋃ N) \land O \in ((J \times_{t} K) CnP N) (⟨R, S⟩)) \to O : X \times Y ⟶ ⋃ N$
45	11 43 8 44	syl3anc	$⊢ φ \to O : X \times Y ⟶ ⋃ N$
46	45	feqmptd	$⊢ φ \to O = (y \in (X \times Y) ⟼ O (y))$
47		fveq2	$⊢ y = ⟨A, B⟩ \to O (y) = O (⟨A, B⟩)$
48		df-ov	$⊢ A O B = O (⟨A, B⟩)$
49	47 48	eqtr4di	$⊢ y = ⟨A, B⟩ \to O (y) = A O B$
50	12 39 46 49	fmptco	$⊢ φ \to O \circ (x \in Z ⟼ ⟨A, B⟩) = (x \in Z ⟼ A O B)$
51	50	fveq2d	$⊢ φ \to (N fLimf L) (O \circ (x \in Z ⟼ ⟨A, B⟩)) = (N fLimf L) ((x \in Z ⟼ A O B))$
52	38 51	eleqtrd	$⊢ φ \to O (⟨R, S⟩) \in (N fLimf L) ((x \in Z ⟼ A O B))$
53	9 52	eqeltrid	$⊢ φ \to R O S \in (N fLimf L) ((x \in Z ⟼ A O B))$

Metamath Proof Explorer

Theorem flfcnp2

Proof