lmcnp

Description: The image of a convergent sequence under a continuous map is convergent to the image of the original point. (Contributed by Mario Carneiro, 3-May-2014)

	Ref	Expression
Hypotheses	lmcnp.3	$⊢ φ \to F \underset{t}{⇝} (J) P$
	lmcnp.4	$⊢ φ \to G \in (J CnP K) (P)$
Assertion	lmcnp	$⊢ φ \to (G \circ F) \underset{t}{⇝} (K) G (P)$

Proof

Step	Hyp	Ref	Expression
1		lmcnp.3	$⊢ φ \to F \underset{t}{⇝} (J) P$
2		lmcnp.4	$⊢ φ \to G \in (J CnP K) (P)$
3		eqid	$⊢ ⋃ J = ⋃ J$
4		eqid	$⊢ ⋃ K = ⋃ K$
5	3 4	cnpf	$⊢ G \in (J CnP K) (P) \to G : ⋃ J ⟶ ⋃ K$
6	2 5	syl	$⊢ φ \to G : ⋃ J ⟶ ⋃ K$
7		cnptop1	$⊢ G \in (J CnP K) (P) \to J \in Top$
8	2 7	syl	$⊢ φ \to J \in Top$
9		toptopon2	$⊢ J \in Top \leftrightarrow J \in TopOn (⋃ J)$
10	8 9	sylib	$⊢ φ \to J \in TopOn (⋃ J)$
11		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
12		1zzd	$⊢ φ \to 1 \in ℤ$
13	10 11 12	lmbr2	$⊢ φ \to (F \underset{t}{⇝} (J) P \leftrightarrow (F \in (⋃ J ↑_{𝑝𝑚} ℂ) \land P \in ⋃ J \land \forall v \in J (P \in v \to \exists j \in ℕ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in v))))$
14	1 13	mpbid	$⊢ φ \to (F \in (⋃ J ↑_{𝑝𝑚} ℂ) \land P \in ⋃ J \land \forall v \in J (P \in v \to \exists j \in ℕ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in v)))$
15	14	simp1d	$⊢ φ \to F \in (⋃ J ↑_{𝑝𝑚} ℂ)$
16	8	uniexd	$⊢ φ \to ⋃ J \in V$
17		cnex	$⊢ ℂ \in V$
18		elpm2g	$⊢ (⋃ J \in V \land ℂ \in V) \to (F \in (⋃ J ↑_{𝑝𝑚} ℂ) \leftrightarrow (F : dom F ⟶ ⋃ J \land dom F \subseteq ℂ))$
19	16 17 18	sylancl	$⊢ φ \to (F \in (⋃ J ↑_{𝑝𝑚} ℂ) \leftrightarrow (F : dom F ⟶ ⋃ J \land dom F \subseteq ℂ))$
20	15 19	mpbid	$⊢ φ \to (F : dom F ⟶ ⋃ J \land dom F \subseteq ℂ)$
21	20	simpld	$⊢ φ \to F : dom F ⟶ ⋃ J$
22		fco	$⊢ (G : ⋃ J ⟶ ⋃ K \land F : dom F ⟶ ⋃ J) \to (G \circ F) : dom F ⟶ ⋃ K$
23	6 21 22	syl2anc	$⊢ φ \to (G \circ F) : dom F ⟶ ⋃ K$
24	23	ffdmd	$⊢ φ \to (G \circ F) : dom (G \circ F) ⟶ ⋃ K$
25	23	fdmd	$⊢ φ \to dom (G \circ F) = dom F$
26	20	simprd	$⊢ φ \to dom F \subseteq ℂ$
27	25 26	eqsstrd	$⊢ φ \to dom (G \circ F) \subseteq ℂ$
28		cnptop2	$⊢ G \in (J CnP K) (P) \to K \in Top$
29	2 28	syl	$⊢ φ \to K \in Top$
30	29	uniexd	$⊢ φ \to ⋃ K \in V$
31		elpm2g	$⊢ (⋃ K \in V \land ℂ \in V) \to (G \circ F \in (⋃ K ↑_{𝑝𝑚} ℂ) \leftrightarrow ((G \circ F) : dom (G \circ F) ⟶ ⋃ K \land dom (G \circ F) \subseteq ℂ))$
32	30 17 31	sylancl	$⊢ φ \to (G \circ F \in (⋃ K ↑_{𝑝𝑚} ℂ) \leftrightarrow ((G \circ F) : dom (G \circ F) ⟶ ⋃ K \land dom (G \circ F) \subseteq ℂ))$
33	24 27 32	mpbir2and	$⊢ φ \to G \circ F \in (⋃ K ↑_{𝑝𝑚} ℂ)$
34	14	simp2d	$⊢ φ \to P \in ⋃ J$
35	6 34	ffvelcdmd	$⊢ φ \to G (P) \in ⋃ K$
36	14	simp3d	$⊢ φ \to \forall v \in J (P \in v \to \exists j \in ℕ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in v))$
37	36	adantr	$⊢ (φ \land (u \in K \land G (P) \in u)) \to \forall v \in J (P \in v \to \exists j \in ℕ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in v))$
38		cnpimaex	$⊢ (G \in (J CnP K) (P) \land u \in K \land G (P) \in u) \to \exists v \in J (P \in v \land G [v] \subseteq u)$
39	38	3expb	$⊢ (G \in (J CnP K) (P) \land (u \in K \land G (P) \in u)) \to \exists v \in J (P \in v \land G [v] \subseteq u)$
40	2 39	sylan	$⊢ (φ \land (u \in K \land G (P) \in u)) \to \exists v \in J (P \in v \land G [v] \subseteq u)$
41		r19.29	$⊢ (\forall v \in J (P \in v \to \exists j \in ℕ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in v)) \land \exists v \in J (P \in v \land G [v] \subseteq u)) \to \exists v \in J ((P \in v \to \exists j \in ℕ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in v)) \land (P \in v \land G [v] \subseteq u))$
42		pm3.45	$⊢ (P \in v \to \exists j \in ℕ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in v)) \to ((P \in v \land G [v] \subseteq u) \to (\exists j \in ℕ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in v) \land G [v] \subseteq u))$
43	42	imp	$⊢ ((P \in v \to \exists j \in ℕ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in v)) \land (P \in v \land G [v] \subseteq u)) \to (\exists j \in ℕ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in v) \land G [v] \subseteq u)$
44	43	reximi	$⊢ \exists v \in J ((P \in v \to \exists j \in ℕ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in v)) \land (P \in v \land G [v] \subseteq u)) \to \exists v \in J (\exists j \in ℕ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in v) \land G [v] \subseteq u)$
45	41 44	syl	$⊢ (\forall v \in J (P \in v \to \exists j \in ℕ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in v)) \land \exists v \in J (P \in v \land G [v] \subseteq u)) \to \exists v \in J (\exists j \in ℕ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in v) \land G [v] \subseteq u)$
46	6	ad3antrrr	$⊢ (((φ \land (u \in K \land G (P) \in u)) \land (v \in J \land G [v] \subseteq u)) \land k \in dom F) \to G : ⋃ J ⟶ ⋃ K$
47	46	ffnd	$⊢ (((φ \land (u \in K \land G (P) \in u)) \land (v \in J \land G [v] \subseteq u)) \land k \in dom F) \to G Fn ⋃ J$
48		simplrl	$⊢ (((φ \land (u \in K \land G (P) \in u)) \land (v \in J \land G [v] \subseteq u)) \land k \in dom F) \to v \in J$
49		elssuni	$⊢ v \in J \to v \subseteq ⋃ J$
50	48 49	syl	$⊢ (((φ \land (u \in K \land G (P) \in u)) \land (v \in J \land G [v] \subseteq u)) \land k \in dom F) \to v \subseteq ⋃ J$
51		fnfvima	$⊢ (G Fn ⋃ J \land v \subseteq ⋃ J \land F (k) \in v) \to G (F (k)) \in G [v]$
52	51	3expia	$⊢ (G Fn ⋃ J \land v \subseteq ⋃ J) \to (F (k) \in v \to G (F (k)) \in G [v])$
53	47 50 52	syl2anc	$⊢ (((φ \land (u \in K \land G (P) \in u)) \land (v \in J \land G [v] \subseteq u)) \land k \in dom F) \to (F (k) \in v \to G (F (k)) \in G [v])$
54	21	ad2antrr	$⊢ ((φ \land (u \in K \land G (P) \in u)) \land (v \in J \land G [v] \subseteq u)) \to F : dom F ⟶ ⋃ J$
55		fvco3	$⊢ (F : dom F ⟶ ⋃ J \land k \in dom F) \to (G \circ F) (k) = G (F (k))$
56	54 55	sylan	$⊢ (((φ \land (u \in K \land G (P) \in u)) \land (v \in J \land G [v] \subseteq u)) \land k \in dom F) \to (G \circ F) (k) = G (F (k))$
57	56	eleq1d	$⊢ (((φ \land (u \in K \land G (P) \in u)) \land (v \in J \land G [v] \subseteq u)) \land k \in dom F) \to ((G \circ F) (k) \in G [v] \leftrightarrow G (F (k)) \in G [v])$
58	53 57	sylibrd	$⊢ (((φ \land (u \in K \land G (P) \in u)) \land (v \in J \land G [v] \subseteq u)) \land k \in dom F) \to (F (k) \in v \to (G \circ F) (k) \in G [v])$
59		simplrr	$⊢ (((φ \land (u \in K \land G (P) \in u)) \land (v \in J \land G [v] \subseteq u)) \land k \in dom F) \to G [v] \subseteq u$
60	59	sseld	$⊢ (((φ \land (u \in K \land G (P) \in u)) \land (v \in J \land G [v] \subseteq u)) \land k \in dom F) \to ((G \circ F) (k) \in G [v] \to (G \circ F) (k) \in u)$
61	58 60	syld	$⊢ (((φ \land (u \in K \land G (P) \in u)) \land (v \in J \land G [v] \subseteq u)) \land k \in dom F) \to (F (k) \in v \to (G \circ F) (k) \in u)$
62		simpr	$⊢ (((φ \land (u \in K \land G (P) \in u)) \land (v \in J \land G [v] \subseteq u)) \land k \in dom F) \to k \in dom F$
63	25	ad3antrrr	$⊢ (((φ \land (u \in K \land G (P) \in u)) \land (v \in J \land G [v] \subseteq u)) \land k \in dom F) \to dom (G \circ F) = dom F$
64	62 63	eleqtrrd	$⊢ (((φ \land (u \in K \land G (P) \in u)) \land (v \in J \land G [v] \subseteq u)) \land k \in dom F) \to k \in dom (G \circ F)$
65	61 64	jctild	$⊢ (((φ \land (u \in K \land G (P) \in u)) \land (v \in J \land G [v] \subseteq u)) \land k \in dom F) \to (F (k) \in v \to (k \in dom (G \circ F) \land (G \circ F) (k) \in u))$
66	65	expimpd	$⊢ ((φ \land (u \in K \land G (P) \in u)) \land (v \in J \land G [v] \subseteq u)) \to ((k \in dom F \land F (k) \in v) \to (k \in dom (G \circ F) \land (G \circ F) (k) \in u))$
67	66	ralimdv	$⊢ ((φ \land (u \in K \land G (P) \in u)) \land (v \in J \land G [v] \subseteq u)) \to (\forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in v) \to \forall k \in ℤ_{\geq j} (k \in dom (G \circ F) \land (G \circ F) (k) \in u))$
68	67	reximdv	$⊢ ((φ \land (u \in K \land G (P) \in u)) \land (v \in J \land G [v] \subseteq u)) \to (\exists j \in ℕ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in v) \to \exists j \in ℕ \forall k \in ℤ_{\geq j} (k \in dom (G \circ F) \land (G \circ F) (k) \in u))$
69	68	expr	$⊢ ((φ \land (u \in K \land G (P) \in u)) \land v \in J) \to (G [v] \subseteq u \to (\exists j \in ℕ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in v) \to \exists j \in ℕ \forall k \in ℤ_{\geq j} (k \in dom (G \circ F) \land (G \circ F) (k) \in u)))$
70	69	impcomd	$⊢ ((φ \land (u \in K \land G (P) \in u)) \land v \in J) \to ((\exists j \in ℕ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in v) \land G [v] \subseteq u) \to \exists j \in ℕ \forall k \in ℤ_{\geq j} (k \in dom (G \circ F) \land (G \circ F) (k) \in u))$
71	70	rexlimdva	$⊢ (φ \land (u \in K \land G (P) \in u)) \to (\exists v \in J (\exists j \in ℕ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in v) \land G [v] \subseteq u) \to \exists j \in ℕ \forall k \in ℤ_{\geq j} (k \in dom (G \circ F) \land (G \circ F) (k) \in u))$
72	45 71	syl5	$⊢ (φ \land (u \in K \land G (P) \in u)) \to ((\forall v \in J (P \in v \to \exists j \in ℕ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in v)) \land \exists v \in J (P \in v \land G [v] \subseteq u)) \to \exists j \in ℕ \forall k \in ℤ_{\geq j} (k \in dom (G \circ F) \land (G \circ F) (k) \in u))$
73	37 40 72	mp2and	$⊢ (φ \land (u \in K \land G (P) \in u)) \to \exists j \in ℕ \forall k \in ℤ_{\geq j} (k \in dom (G \circ F) \land (G \circ F) (k) \in u)$
74	73	expr	$⊢ (φ \land u \in K) \to (G (P) \in u \to \exists j \in ℕ \forall k \in ℤ_{\geq j} (k \in dom (G \circ F) \land (G \circ F) (k) \in u))$
75	74	ralrimiva	$⊢ φ \to \forall u \in K (G (P) \in u \to \exists j \in ℕ \forall k \in ℤ_{\geq j} (k \in dom (G \circ F) \land (G \circ F) (k) \in u))$
76		toptopon2	$⊢ K \in Top \leftrightarrow K \in TopOn (⋃ K)$
77	29 76	sylib	$⊢ φ \to K \in TopOn (⋃ K)$
78	77 11 12	lmbr2	$⊢ φ \to ((G \circ F) \underset{t}{⇝} (K) G (P) \leftrightarrow (G \circ F \in (⋃ K ↑_{𝑝𝑚} ℂ) \land G (P) \in ⋃ K \land \forall u \in K (G (P) \in u \to \exists j \in ℕ \forall k \in ℤ_{\geq j} (k \in dom (G \circ F) \land (G \circ F) (k) \in u))))$
79	33 35 75 78	mpbir3and	$⊢ φ \to (G \circ F) \underset{t}{⇝} (K) G (P)$

Metamath Proof Explorer

Theorem lmcnp

Proof