cmetcaulem

	Ref	Expression
Hypotheses	cmetcau.1	$⊢ J = MetOpen (D)$
	cmetcau.3	$⊢ φ \to D \in CMet (X)$
	cmetcau.4	$⊢ φ \to P \in X$
	cmetcau.5	$⊢ φ \to F \in Cau (D)$
	cmetcau.6	$⊢ G = (x \in ℕ ⟼ if (x \in dom F, F (x), P))$
Assertion	cmetcaulem	$⊢ φ \to F \in dom \underset{t}{⇝} (J)$

Proof

Step	Hyp	Ref	Expression
1		cmetcau.1	$⊢ J = MetOpen (D)$
2		cmetcau.3	$⊢ φ \to D \in CMet (X)$
3		cmetcau.4	$⊢ φ \to P \in X$
4		cmetcau.5	$⊢ φ \to F \in Cau (D)$
5		cmetcau.6	$⊢ G = (x \in ℕ ⟼ if (x \in dom F, F (x), P))$
6		cmetmet	$⊢ D \in CMet (X) \to D \in Met (X)$
7	2 6	syl	$⊢ φ \to D \in Met (X)$
8		metxmet	$⊢ D \in Met (X) \to D \in ∞Met (X)$
9	7 8	syl	$⊢ φ \to D \in ∞Met (X)$
10	1	mopntopon	$⊢ D \in ∞Met (X) \to J \in TopOn (X)$
11	9 10	syl	$⊢ φ \to J \in TopOn (X)$
12		1z	$⊢ 1 \in ℤ$
13		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
14	13	uzfbas	$⊢ 1 \in ℤ \to ℤ_{\geq} [ℕ] \in fBas (ℕ)$
15	12 14	mp1i	$⊢ φ \to ℤ_{\geq} [ℕ] \in fBas (ℕ)$
16		fgcl	$⊢ ℤ_{\geq} [ℕ] \in fBas (ℕ) \to ℕ filGen ℤ_{\geq} [ℕ] \in Fil (ℕ)$
17	15 16	syl	$⊢ φ \to ℕ filGen ℤ_{\geq} [ℕ] \in Fil (ℕ)$
18		elfvdm	$⊢ D \in CMet (X) \to X \in dom CMet$
19	2 18	syl	$⊢ φ \to X \in dom CMet$
20		cnex	$⊢ ℂ \in V$
21	20	a1i	$⊢ φ \to ℂ \in V$
22		caufpm	$⊢ (D \in ∞Met (X) \land F \in Cau (D)) \to F \in (X ↑_{𝑝𝑚} ℂ)$
23	9 4 22	syl2anc	$⊢ φ \to F \in (X ↑_{𝑝𝑚} ℂ)$
24		elpm2g	$⊢ (X \in dom CMet \land ℂ \in V) \to (F \in (X ↑_{𝑝𝑚} ℂ) \leftrightarrow (F : dom F ⟶ X \land dom F \subseteq ℂ))$
25	24	simprbda	$⊢ ((X \in dom CMet \land ℂ \in V) \land F \in (X ↑_{𝑝𝑚} ℂ)) \to F : dom F ⟶ X$
26	19 21 23 25	syl21anc	$⊢ φ \to F : dom F ⟶ X$
27	26	adantr	$⊢ (φ \land x \in ℕ) \to F : dom F ⟶ X$
28	27	ffvelcdmda	$⊢ ((φ \land x \in ℕ) \land x \in dom F) \to F (x) \in X$
29	3	ad2antrr	$⊢ ((φ \land x \in ℕ) \land \neg x \in dom F) \to P \in X$
30	28 29	ifclda	$⊢ (φ \land x \in ℕ) \to if (x \in dom F, F (x), P) \in X$
31	30 5	fmptd	$⊢ φ \to G : ℕ ⟶ X$
32		flfval	$⊢ (J \in TopOn (X) \land ℕ filGen ℤ_{\geq} [ℕ] \in Fil (ℕ) \land G : ℕ ⟶ X) \to (J fLimf (ℕ filGen ℤ_{\geq} [ℕ])) (G) = J fLim (X FilMap G) (ℕ filGen ℤ_{\geq} [ℕ])$
33	11 17 31 32	syl3anc	$⊢ φ \to (J fLimf (ℕ filGen ℤ_{\geq} [ℕ])) (G) = J fLim (X FilMap G) (ℕ filGen ℤ_{\geq} [ℕ])$
34		eqid	$⊢ ℕ filGen ℤ_{\geq} [ℕ] = ℕ filGen ℤ_{\geq} [ℕ]$
35	34	fmfg	$⊢ (X \in dom CMet \land ℤ_{\geq} [ℕ] \in fBas (ℕ) \land G : ℕ ⟶ X) \to (X FilMap G) (ℤ_{\geq} [ℕ]) = (X FilMap G) (ℕ filGen ℤ_{\geq} [ℕ])$
36	19 15 31 35	syl3anc	$⊢ φ \to (X FilMap G) (ℤ_{\geq} [ℕ]) = (X FilMap G) (ℕ filGen ℤ_{\geq} [ℕ])$
37	36	oveq2d	$⊢ φ \to J fLim (X FilMap G) (ℤ_{\geq} [ℕ]) = J fLim (X FilMap G) (ℕ filGen ℤ_{\geq} [ℕ])$
38	33 37	eqtr4d	$⊢ φ \to (J fLimf (ℕ filGen ℤ_{\geq} [ℕ])) (G) = J fLim (X FilMap G) (ℤ_{\geq} [ℕ])$
39		biidd	$⊢ z = 1 \to (\exists j \in ℕ \forall k \in ℤ_{\geq j} k \in dom F \leftrightarrow \exists j \in ℕ \forall k \in ℤ_{\geq j} k \in dom F)$
40		1zzd	$⊢ φ \to 1 \in ℤ$
41	13 9 40	iscau3	$⊢ φ \to (F \in Cau (D) \leftrightarrow (F \in (X ↑_{𝑝𝑚} ℂ) \land \forall z \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land \forall w \in ℤ_{\geq k} F (k) D F (w) < z)))$
42	41	simplbda	$⊢ (φ \land F \in Cau (D)) \to \forall z \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land \forall w \in ℤ_{\geq k} F (k) D F (w) < z)$
43	4 42	mpdan	$⊢ φ \to \forall z \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land \forall w \in ℤ_{\geq k} F (k) D F (w) < z)$
44		simp1	$⊢ (k \in dom F \land F (k) \in X \land \forall w \in ℤ_{\geq k} F (k) D F (w) < z) \to k \in dom F$
45	44	ralimi	$⊢ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land \forall w \in ℤ_{\geq k} F (k) D F (w) < z) \to \forall k \in ℤ_{\geq j} k \in dom F$
46	45	reximi	$⊢ \exists j \in ℕ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land \forall w \in ℤ_{\geq k} F (k) D F (w) < z) \to \exists j \in ℕ \forall k \in ℤ_{\geq j} k \in dom F$
47	46	ralimi	$⊢ \forall z \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land \forall w \in ℤ_{\geq k} F (k) D F (w) < z) \to \forall z \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} k \in dom F$
48	43 47	syl	$⊢ φ \to \forall z \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} k \in dom F$
49		1rp	$⊢ 1 \in ℝ^{+}$
50	49	a1i	$⊢ φ \to 1 \in ℝ^{+}$
51	39 48 50	rspcdva	$⊢ φ \to \exists j \in ℕ \forall k \in ℤ_{\geq j} k \in dom F$
52		dfss3	$⊢ ℤ_{\geq j} \subseteq dom F \leftrightarrow \forall k \in ℤ_{\geq j} k \in dom F$
53		nnsscn	$⊢ ℕ \subseteq ℂ$
54	31 53	jctir	$⊢ φ \to (G : ℕ ⟶ X \land ℕ \subseteq ℂ)$
55		elpm2r	$⊢ ((X \in dom CMet \land ℂ \in V) \land (G : ℕ ⟶ X \land ℕ \subseteq ℂ)) \to G \in (X ↑_{𝑝𝑚} ℂ)$
56	19 21 54 55	syl21anc	$⊢ φ \to G \in (X ↑_{𝑝𝑚} ℂ)$
57	56	adantr	$⊢ (φ \land (j \in ℕ \land ℤ_{\geq j} \subseteq dom F)) \to G \in (X ↑_{𝑝𝑚} ℂ)$
58		eqid	$⊢ ℤ_{\geq j} = ℤ_{\geq j}$
59	9	adantr	$⊢ (φ \land (j \in ℕ \land ℤ_{\geq j} \subseteq dom F)) \to D \in ∞Met (X)$
60		nnz	$⊢ j \in ℕ \to j \in ℤ$
61	60	ad2antrl	$⊢ (φ \land (j \in ℕ \land ℤ_{\geq j} \subseteq dom F)) \to j \in ℤ$
62		eqidd	$⊢ ((φ \land (j \in ℕ \land ℤ_{\geq j} \subseteq dom F)) \land k \in ℤ_{\geq j}) \to F (k) = F (k)$
63		eqidd	$⊢ ((φ \land (j \in ℕ \land ℤ_{\geq j} \subseteq dom F)) \land m \in ℤ_{\geq j}) \to F (m) = F (m)$
64	58 59 61 62 63	iscau4	$⊢ (φ \land (j \in ℕ \land ℤ_{\geq j} \subseteq dom F)) \to (F \in Cau (D) \leftrightarrow (F \in (X ↑_{𝑝𝑚} ℂ) \land \forall z \in ℝ^{+} \exists m \in ℤ_{\geq j} \forall k \in ℤ_{\geq m} (k \in dom F \land F (k) \in X \land F (k) D F (m) < z)))$
65	64	simplbda	$⊢ ((φ \land (j \in ℕ \land ℤ_{\geq j} \subseteq dom F)) \land F \in Cau (D)) \to \forall z \in ℝ^{+} \exists m \in ℤ_{\geq j} \forall k \in ℤ_{\geq m} (k \in dom F \land F (k) \in X \land F (k) D F (m) < z)$
66	4 65	mpidan	$⊢ (φ \land (j \in ℕ \land ℤ_{\geq j} \subseteq dom F)) \to \forall z \in ℝ^{+} \exists m \in ℤ_{\geq j} \forall k \in ℤ_{\geq m} (k \in dom F \land F (k) \in X \land F (k) D F (m) < z)$
67		simprl	$⊢ (φ \land (j \in ℕ \land ℤ_{\geq j} \subseteq dom F)) \to j \in ℕ$
68		eluznn	$⊢ (j \in ℕ \land m \in ℤ_{\geq j}) \to m \in ℕ$
69	67 68	sylan	$⊢ ((φ \land (j \in ℕ \land ℤ_{\geq j} \subseteq dom F)) \land m \in ℤ_{\geq j}) \to m \in ℕ$
70		eluznn	$⊢ (m \in ℕ \land k \in ℤ_{\geq m}) \to k \in ℕ$
71	5 30	dmmptd	$⊢ φ \to dom G = ℕ$
72	71	adantr	$⊢ (φ \land (j \in ℕ \land ℤ_{\geq j} \subseteq dom F)) \to dom G = ℕ$
73	72	eleq2d	$⊢ (φ \land (j \in ℕ \land ℤ_{\geq j} \subseteq dom F)) \to (k \in dom G \leftrightarrow k \in ℕ)$
74	73	biimpar	$⊢ ((φ \land (j \in ℕ \land ℤ_{\geq j} \subseteq dom F)) \land k \in ℕ) \to k \in dom G$
75	74	a1d	$⊢ ((φ \land (j \in ℕ \land ℤ_{\geq j} \subseteq dom F)) \land k \in ℕ) \to (k \in dom F \to k \in dom G)$
76		idd	$⊢ ((φ \land (j \in ℕ \land ℤ_{\geq j} \subseteq dom F)) \land k \in ℕ) \to (F (k) \in X \to F (k) \in X)$
77		idd	$⊢ ((φ \land (j \in ℕ \land ℤ_{\geq j} \subseteq dom F)) \land k \in ℕ) \to (F (k) D F (m) < z \to F (k) D F (m) < z)$
78	75 76 77	3anim123d	$⊢ ((φ \land (j \in ℕ \land ℤ_{\geq j} \subseteq dom F)) \land k \in ℕ) \to ((k \in dom F \land F (k) \in X \land F (k) D F (m) < z) \to (k \in dom G \land F (k) \in X \land F (k) D F (m) < z))$
79	70 78	sylan2	$⊢ ((φ \land (j \in ℕ \land ℤ_{\geq j} \subseteq dom F)) \land (m \in ℕ \land k \in ℤ_{\geq m})) \to ((k \in dom F \land F (k) \in X \land F (k) D F (m) < z) \to (k \in dom G \land F (k) \in X \land F (k) D F (m) < z))$
80	79	anassrs	$⊢ (((φ \land (j \in ℕ \land ℤ_{\geq j} \subseteq dom F)) \land m \in ℕ) \land k \in ℤ_{\geq m}) \to ((k \in dom F \land F (k) \in X \land F (k) D F (m) < z) \to (k \in dom G \land F (k) \in X \land F (k) D F (m) < z))$
81	80	ralimdva	$⊢ ((φ \land (j \in ℕ \land ℤ_{\geq j} \subseteq dom F)) \land m \in ℕ) \to (\forall k \in ℤ_{\geq m} (k \in dom F \land F (k) \in X \land F (k) D F (m) < z) \to \forall k \in ℤ_{\geq m} (k \in dom G \land F (k) \in X \land F (k) D F (m) < z))$
82	69 81	syldan	$⊢ ((φ \land (j \in ℕ \land ℤ_{\geq j} \subseteq dom F)) \land m \in ℤ_{\geq j}) \to (\forall k \in ℤ_{\geq m} (k \in dom F \land F (k) \in X \land F (k) D F (m) < z) \to \forall k \in ℤ_{\geq m} (k \in dom G \land F (k) \in X \land F (k) D F (m) < z))$
83	82	reximdva	$⊢ (φ \land (j \in ℕ \land ℤ_{\geq j} \subseteq dom F)) \to (\exists m \in ℤ_{\geq j} \forall k \in ℤ_{\geq m} (k \in dom F \land F (k) \in X \land F (k) D F (m) < z) \to \exists m \in ℤ_{\geq j} \forall k \in ℤ_{\geq m} (k \in dom G \land F (k) \in X \land F (k) D F (m) < z))$
84	83	ralimdv	$⊢ (φ \land (j \in ℕ \land ℤ_{\geq j} \subseteq dom F)) \to (\forall z \in ℝ^{+} \exists m \in ℤ_{\geq j} \forall k \in ℤ_{\geq m} (k \in dom F \land F (k) \in X \land F (k) D F (m) < z) \to \forall z \in ℝ^{+} \exists m \in ℤ_{\geq j} \forall k \in ℤ_{\geq m} (k \in dom G \land F (k) \in X \land F (k) D F (m) < z))$
85	66 84	mpd	$⊢ (φ \land (j \in ℕ \land ℤ_{\geq j} \subseteq dom F)) \to \forall z \in ℝ^{+} \exists m \in ℤ_{\geq j} \forall k \in ℤ_{\geq m} (k \in dom G \land F (k) \in X \land F (k) D F (m) < z)$
86		eluznn	$⊢ (j \in ℕ \land k \in ℤ_{\geq j}) \to k \in ℕ$
87	67 86	sylan	$⊢ ((φ \land (j \in ℕ \land ℤ_{\geq j} \subseteq dom F)) \land k \in ℤ_{\geq j}) \to k \in ℕ$
88		simprr	$⊢ (φ \land (j \in ℕ \land ℤ_{\geq j} \subseteq dom F)) \to ℤ_{\geq j} \subseteq dom F$
89	88	sselda	$⊢ ((φ \land (j \in ℕ \land ℤ_{\geq j} \subseteq dom F)) \land k \in ℤ_{\geq j}) \to k \in dom F$
90		iftrue	$⊢ k \in dom F \to if (k \in dom F, F (k), P) = F (k)$
91	90	adantl	$⊢ (k \in ℕ \land k \in dom F) \to if (k \in dom F, F (k), P) = F (k)$
92		fvex	$⊢ F (k) \in V$
93	91 92	eqeltrdi	$⊢ (k \in ℕ \land k \in dom F) \to if (k \in dom F, F (k), P) \in V$
94		eleq1w	$⊢ x = k \to (x \in dom F \leftrightarrow k \in dom F)$
95		fveq2	$⊢ x = k \to F (x) = F (k)$
96	94 95	ifbieq1d	$⊢ x = k \to if (x \in dom F, F (x), P) = if (k \in dom F, F (k), P)$
97	96 5	fvmptg	$⊢ (k \in ℕ \land if (k \in dom F, F (k), P) \in V) \to G (k) = if (k \in dom F, F (k), P)$
98	93 97	syldan	$⊢ (k \in ℕ \land k \in dom F) \to G (k) = if (k \in dom F, F (k), P)$
99	98 91	eqtrd	$⊢ (k \in ℕ \land k \in dom F) \to G (k) = F (k)$
100	87 89 99	syl2anc	$⊢ ((φ \land (j \in ℕ \land ℤ_{\geq j} \subseteq dom F)) \land k \in ℤ_{\geq j}) \to G (k) = F (k)$
101	88	sselda	$⊢ ((φ \land (j \in ℕ \land ℤ_{\geq j} \subseteq dom F)) \land m \in ℤ_{\geq j}) \to m \in dom F$
102	69 101	elind	$⊢ ((φ \land (j \in ℕ \land ℤ_{\geq j} \subseteq dom F)) \land m \in ℤ_{\geq j}) \to m \in (ℕ \cap dom F)$
103		fveq2	$⊢ k = m \to G (k) = G (m)$
104		fveq2	$⊢ k = m \to F (k) = F (m)$
105	103 104	eqeq12d	$⊢ k = m \to (G (k) = F (k) \leftrightarrow G (m) = F (m))$
106		elin	$⊢ k \in (ℕ \cap dom F) \leftrightarrow (k \in ℕ \land k \in dom F)$
107	106 99	sylbi	$⊢ k \in (ℕ \cap dom F) \to G (k) = F (k)$
108	105 107	vtoclga	$⊢ m \in (ℕ \cap dom F) \to G (m) = F (m)$
109	102 108	syl	$⊢ ((φ \land (j \in ℕ \land ℤ_{\geq j} \subseteq dom F)) \land m \in ℤ_{\geq j}) \to G (m) = F (m)$
110	58 59 61 100 109	iscau4	$⊢ (φ \land (j \in ℕ \land ℤ_{\geq j} \subseteq dom F)) \to (G \in Cau (D) \leftrightarrow (G \in (X ↑_{𝑝𝑚} ℂ) \land \forall z \in ℝ^{+} \exists m \in ℤ_{\geq j} \forall k \in ℤ_{\geq m} (k \in dom G \land F (k) \in X \land F (k) D F (m) < z)))$
111	57 85 110	mpbir2and	$⊢ (φ \land (j \in ℕ \land ℤ_{\geq j} \subseteq dom F)) \to G \in Cau (D)$
112	111	expr	$⊢ (φ \land j \in ℕ) \to (ℤ_{\geq j} \subseteq dom F \to G \in Cau (D))$
113	52 112	biimtrrid	$⊢ (φ \land j \in ℕ) \to (\forall k \in ℤ_{\geq j} k \in dom F \to G \in Cau (D))$
114	113	rexlimdva	$⊢ φ \to (\exists j \in ℕ \forall k \in ℤ_{\geq j} k \in dom F \to G \in Cau (D))$
115	51 114	mpd	$⊢ φ \to G \in Cau (D)$
116		eqid	$⊢ (X FilMap G) (ℤ_{\geq} [ℕ]) = (X FilMap G) (ℤ_{\geq} [ℕ])$
117	13 116	caucfil	$⊢ (D \in ∞Met (X) \land 1 \in ℤ \land G : ℕ ⟶ X) \to (G \in Cau (D) \leftrightarrow (X FilMap G) (ℤ_{\geq} [ℕ]) \in CauFil (D))$
118	9 40 31 117	syl3anc	$⊢ φ \to (G \in Cau (D) \leftrightarrow (X FilMap G) (ℤ_{\geq} [ℕ]) \in CauFil (D))$
119	115 118	mpbid	$⊢ φ \to (X FilMap G) (ℤ_{\geq} [ℕ]) \in CauFil (D)$
120	1	cmetcvg	$⊢ (D \in CMet (X) \land (X FilMap G) (ℤ_{\geq} [ℕ]) \in CauFil (D)) \to J fLim (X FilMap G) (ℤ_{\geq} [ℕ]) \neq \emptyset$
121	2 119 120	syl2anc	$⊢ φ \to J fLim (X FilMap G) (ℤ_{\geq} [ℕ]) \neq \emptyset$
122	38 121	eqnetrd	$⊢ φ \to (J fLimf (ℕ filGen ℤ_{\geq} [ℕ])) (G) \neq \emptyset$
123		n0	$⊢ (J fLimf (ℕ filGen ℤ_{\geq} [ℕ])) (G) \neq \emptyset \leftrightarrow \exists y y \in (J fLimf (ℕ filGen ℤ_{\geq} [ℕ])) (G)$
124	122 123	sylib	$⊢ φ \to \exists y y \in (J fLimf (ℕ filGen ℤ_{\geq} [ℕ])) (G)$
125	13 34	lmflf	$⊢ (J \in TopOn (X) \land 1 \in ℤ \land G : ℕ ⟶ X) \to (G \underset{t}{⇝} (J) y \leftrightarrow y \in (J fLimf (ℕ filGen ℤ_{\geq} [ℕ])) (G))$
126	11 40 31 125	syl3anc	$⊢ φ \to (G \underset{t}{⇝} (J) y \leftrightarrow y \in (J fLimf (ℕ filGen ℤ_{\geq} [ℕ])) (G))$
127	23	adantr	$⊢ (φ \land G \underset{t}{⇝} (J) y) \to F \in (X ↑_{𝑝𝑚} ℂ)$
128		lmcl	$⊢ (J \in TopOn (X) \land G \underset{t}{⇝} (J) y) \to y \in X$
129	11 128	sylan	$⊢ (φ \land G \underset{t}{⇝} (J) y) \to y \in X$
130	1 9 13 40	lmmbr3	$⊢ φ \to (G \underset{t}{⇝} (J) y \leftrightarrow (G \in (X ↑_{𝑝𝑚} ℂ) \land y \in X \land \forall z \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} (k \in dom G \land G (k) \in X \land G (k) D y < z)))$
131	130	biimpa	$⊢ (φ \land G \underset{t}{⇝} (J) y) \to (G \in (X ↑_{𝑝𝑚} ℂ) \land y \in X \land \forall z \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} (k \in dom G \land G (k) \in X \land G (k) D y < z))$
132	131	simp3d	$⊢ (φ \land G \underset{t}{⇝} (J) y) \to \forall z \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} (k \in dom G \land G (k) \in X \land G (k) D y < z)$
133		r19.26	$⊢ \forall z \in ℝ^{+} (\exists j \in ℕ \forall k \in ℤ_{\geq j} k \in dom F \land \exists j \in ℕ \forall k \in ℤ_{\geq j} (k \in dom G \land G (k) \in X \land G (k) D y < z)) \leftrightarrow (\forall z \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} k \in dom F \land \forall z \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} (k \in dom G \land G (k) \in X \land G (k) D y < z))$
134	13	rexanuz2	$⊢ \exists j \in ℕ \forall k \in ℤ_{\geq j} (k \in dom F \land (k \in dom G \land G (k) \in X \land G (k) D y < z)) \leftrightarrow (\exists j \in ℕ \forall k \in ℤ_{\geq j} k \in dom F \land \exists j \in ℕ \forall k \in ℤ_{\geq j} (k \in dom G \land G (k) \in X \land G (k) D y < z))$
135		simprl	$⊢ ((φ \land k \in ℕ) \land (k \in dom F \land (k \in dom G \land G (k) \in X \land G (k) D y < z))) \to k \in dom F$
136	99	ad2ant2lr	$⊢ ((φ \land k \in ℕ) \land (k \in dom F \land (k \in dom G \land G (k) \in X \land G (k) D y < z))) \to G (k) = F (k)$
137		simprr2	$⊢ ((φ \land k \in ℕ) \land (k \in dom F \land (k \in dom G \land G (k) \in X \land G (k) D y < z))) \to G (k) \in X$
138	136 137	eqeltrrd	$⊢ ((φ \land k \in ℕ) \land (k \in dom F \land (k \in dom G \land G (k) \in X \land G (k) D y < z))) \to F (k) \in X$
139	136	oveq1d	$⊢ ((φ \land k \in ℕ) \land (k \in dom F \land (k \in dom G \land G (k) \in X \land G (k) D y < z))) \to G (k) D y = F (k) D y$
140		simprr3	$⊢ ((φ \land k \in ℕ) \land (k \in dom F \land (k \in dom G \land G (k) \in X \land G (k) D y < z))) \to G (k) D y < z$
141	139 140	eqbrtrrd	$⊢ ((φ \land k \in ℕ) \land (k \in dom F \land (k \in dom G \land G (k) \in X \land G (k) D y < z))) \to F (k) D y < z$
142	135 138 141	3jca	$⊢ ((φ \land k \in ℕ) \land (k \in dom F \land (k \in dom G \land G (k) \in X \land G (k) D y < z))) \to (k \in dom F \land F (k) \in X \land F (k) D y < z)$
143	142	ex	$⊢ (φ \land k \in ℕ) \to ((k \in dom F \land (k \in dom G \land G (k) \in X \land G (k) D y < z)) \to (k \in dom F \land F (k) \in X \land F (k) D y < z))$
144	86 143	sylan2	$⊢ (φ \land (j \in ℕ \land k \in ℤ_{\geq j})) \to ((k \in dom F \land (k \in dom G \land G (k) \in X \land G (k) D y < z)) \to (k \in dom F \land F (k) \in X \land F (k) D y < z))$
145	144	anassrs	$⊢ ((φ \land j \in ℕ) \land k \in ℤ_{\geq j}) \to ((k \in dom F \land (k \in dom G \land G (k) \in X \land G (k) D y < z)) \to (k \in dom F \land F (k) \in X \land F (k) D y < z))$
146	145	ralimdva	$⊢ (φ \land j \in ℕ) \to (\forall k \in ℤ_{\geq j} (k \in dom F \land (k \in dom G \land G (k) \in X \land G (k) D y < z)) \to \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D y < z))$
147	146	reximdva	$⊢ φ \to (\exists j \in ℕ \forall k \in ℤ_{\geq j} (k \in dom F \land (k \in dom G \land G (k) \in X \land G (k) D y < z)) \to \exists j \in ℕ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D y < z))$
148	134 147	biimtrrid	$⊢ φ \to ((\exists j \in ℕ \forall k \in ℤ_{\geq j} k \in dom F \land \exists j \in ℕ \forall k \in ℤ_{\geq j} (k \in dom G \land G (k) \in X \land G (k) D y < z)) \to \exists j \in ℕ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D y < z))$
149	148	ralimdv	$⊢ φ \to (\forall z \in ℝ^{+} (\exists j \in ℕ \forall k \in ℤ_{\geq j} k \in dom F \land \exists j \in ℕ \forall k \in ℤ_{\geq j} (k \in dom G \land G (k) \in X \land G (k) D y < z)) \to \forall z \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D y < z))$
150	133 149	biimtrrid	$⊢ φ \to ((\forall z \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} k \in dom F \land \forall z \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} (k \in dom G \land G (k) \in X \land G (k) D y < z)) \to \forall z \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D y < z))$
151	48 150	mpand	$⊢ φ \to (\forall z \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} (k \in dom G \land G (k) \in X \land G (k) D y < z) \to \forall z \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D y < z))$
152	151	adantr	$⊢ (φ \land G \underset{t}{⇝} (J) y) \to (\forall z \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} (k \in dom G \land G (k) \in X \land G (k) D y < z) \to \forall z \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D y < z))$
153	132 152	mpd	$⊢ (φ \land G \underset{t}{⇝} (J) y) \to \forall z \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D y < z)$
154	9	adantr	$⊢ (φ \land G \underset{t}{⇝} (J) y) \to D \in ∞Met (X)$
155		1zzd	$⊢ (φ \land G \underset{t}{⇝} (J) y) \to 1 \in ℤ$
156	1 154 13 155	lmmbr3	$⊢ (φ \land G \underset{t}{⇝} (J) y) \to (F \underset{t}{⇝} (J) y \leftrightarrow (F \in (X ↑_{𝑝𝑚} ℂ) \land y \in X \land \forall z \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D y < z)))$
157	127 129 153 156	mpbir3and	$⊢ (φ \land G \underset{t}{⇝} (J) y) \to F \underset{t}{⇝} (J) y$
158		lmrel	$⊢ Rel \underset{t}{⇝} (J)$
159	158	releldmi	$⊢ F \underset{t}{⇝} (J) y \to F \in dom \underset{t}{⇝} (J)$
160	157 159	syl	$⊢ (φ \land G \underset{t}{⇝} (J) y) \to F \in dom \underset{t}{⇝} (J)$
161	160	ex	$⊢ φ \to (G \underset{t}{⇝} (J) y \to F \in dom \underset{t}{⇝} (J))$
162	126 161	sylbird	$⊢ φ \to (y \in (J fLimf (ℕ filGen ℤ_{\geq} [ℕ])) (G) \to F \in dom \underset{t}{⇝} (J))$
163	162	exlimdv	$⊢ φ \to (\exists y y \in (J fLimf (ℕ filGen ℤ_{\geq} [ℕ])) (G) \to F \in dom \underset{t}{⇝} (J))$
164	124 163	mpd	$⊢ φ \to F \in dom \underset{t}{⇝} (J)$

Metamath Proof Explorer

Theorem cmetcaulem

Proof