iscmet3lem2

	Ref	Expression
Hypotheses	iscmet3.1	$⊢ Z = ℤ_{\geq M}$
	iscmet3.2	$⊢ J = MetOpen (D)$
	iscmet3.3	$⊢ φ \to M \in ℤ$
	iscmet3.4	$⊢ φ \to D \in Met (X)$
	iscmet3.6	$⊢ φ \to F : Z ⟶ X$
	iscmet3.9	$⊢ φ \to \forall k \in ℤ \forall u \in S (k) \forall v \in S (k) u D v < {(\frac{1}{2})}^{k}$
	iscmet3.10	$⊢ φ \to \forall k \in Z \forall n \in (M \dots k) F (k) \in S (n)$
	iscmet3.7	$⊢ φ \to G \in Fil (X)$
	iscmet3.8	$⊢ φ \to S : ℤ ⟶ G$
	iscmet3.5	$⊢ φ \to F \in dom \underset{t}{⇝} (J)$
Assertion	iscmet3lem2	$⊢ φ \to J fLim G \neq \emptyset$

Proof

Step	Hyp	Ref	Expression
1		iscmet3.1	$⊢ Z = ℤ_{\geq M}$
2		iscmet3.2	$⊢ J = MetOpen (D)$
3		iscmet3.3	$⊢ φ \to M \in ℤ$
4		iscmet3.4	$⊢ φ \to D \in Met (X)$
5		iscmet3.6	$⊢ φ \to F : Z ⟶ X$
6		iscmet3.9	$⊢ φ \to \forall k \in ℤ \forall u \in S (k) \forall v \in S (k) u D v < {(\frac{1}{2})}^{k}$
7		iscmet3.10	$⊢ φ \to \forall k \in Z \forall n \in (M \dots k) F (k) \in S (n)$
8		iscmet3.7	$⊢ φ \to G \in Fil (X)$
9		iscmet3.8	$⊢ φ \to S : ℤ ⟶ G$
10		iscmet3.5	$⊢ φ \to F \in dom \underset{t}{⇝} (J)$
11		eldmg	$⊢ F \in dom \underset{t}{⇝} (J) \to (F \in dom \underset{t}{⇝} (J) \leftrightarrow \exists x F \underset{t}{⇝} (J) x)$
12	11	ibi	$⊢ F \in dom \underset{t}{⇝} (J) \to \exists x F \underset{t}{⇝} (J) x$
13	10 12	syl	$⊢ φ \to \exists x F \underset{t}{⇝} (J) x$
14		metxmet	$⊢ D \in Met (X) \to D \in ∞Met (X)$
15	4 14	syl	$⊢ φ \to D \in ∞Met (X)$
16	2	mopntopon	$⊢ D \in ∞Met (X) \to J \in TopOn (X)$
17	15 16	syl	$⊢ φ \to J \in TopOn (X)$
18		lmcl	$⊢ (J \in TopOn (X) \land F \underset{t}{⇝} (J) x) \to x \in X$
19	17 18	sylan	$⊢ (φ \land F \underset{t}{⇝} (J) x) \to x \in X$
20	15	adantr	$⊢ (φ \land F \underset{t}{⇝} (J) x) \to D \in ∞Met (X)$
21	2	mopni2	$⊢ (D \in ∞Met (X) \land y \in J \land x \in y) \to \exists r \in ℝ^{+} x ball (D) r \subseteq y$
22	21	3expia	$⊢ (D \in ∞Met (X) \land y \in J) \to (x \in y \to \exists r \in ℝ^{+} x ball (D) r \subseteq y)$
23	20 22	sylan	$⊢ ((φ \land F \underset{t}{⇝} (J) x) \land y \in J) \to (x \in y \to \exists r \in ℝ^{+} x ball (D) r \subseteq y)$
24	8	ad3antrrr	$⊢ (((φ \land F \underset{t}{⇝} (J) x) \land y \in J) \land (r \in ℝ^{+} \land x ball (D) r \subseteq y)) \to G \in Fil (X)$
25	3	ad2antrr	$⊢ ((φ \land F \underset{t}{⇝} (J) x) \land r \in ℝ^{+}) \to M \in ℤ$
26		rphalfcl	$⊢ r \in ℝ^{+} \to \frac{r}{2} \in ℝ^{+}$
27	26	adantl	$⊢ ((φ \land F \underset{t}{⇝} (J) x) \land r \in ℝ^{+}) \to \frac{r}{2} \in ℝ^{+}$
28	1	iscmet3lem3	$⊢ (M \in ℤ \land \frac{r}{2} \in ℝ^{+}) \to \exists j \in Z \forall k \in ℤ_{\geq j} {(\frac{1}{2})}^{k} < \frac{r}{2}$
29	25 27 28	syl2anc	$⊢ ((φ \land F \underset{t}{⇝} (J) x) \land r \in ℝ^{+}) \to \exists j \in Z \forall k \in ℤ_{\geq j} {(\frac{1}{2})}^{k} < \frac{r}{2}$
30	20	adantr	$⊢ ((φ \land F \underset{t}{⇝} (J) x) \land r \in ℝ^{+}) \to D \in ∞Met (X)$
31	19	adantr	$⊢ ((φ \land F \underset{t}{⇝} (J) x) \land r \in ℝ^{+}) \to x \in X$
32		blcntr	$⊢ (D \in ∞Met (X) \land x \in X \land \frac{r}{2} \in ℝ^{+}) \to x \in (x ball (D) (\frac{r}{2}))$
33	30 31 27 32	syl3anc	$⊢ ((φ \land F \underset{t}{⇝} (J) x) \land r \in ℝ^{+}) \to x \in (x ball (D) (\frac{r}{2}))$
34		simplr	$⊢ ((φ \land F \underset{t}{⇝} (J) x) \land r \in ℝ^{+}) \to F \underset{t}{⇝} (J) x$
35	27	rpxrd	$⊢ ((φ \land F \underset{t}{⇝} (J) x) \land r \in ℝ^{+}) \to \frac{r}{2} \in ℝ^{*}$
36	2	blopn	$⊢ (D \in ∞Met (X) \land x \in X \land \frac{r}{2} \in ℝ^{*}) \to x ball (D) (\frac{r}{2}) \in J$
37	30 31 35 36	syl3anc	$⊢ ((φ \land F \underset{t}{⇝} (J) x) \land r \in ℝ^{+}) \to x ball (D) (\frac{r}{2}) \in J$
38	1 33 25 34 37	lmcvg	$⊢ ((φ \land F \underset{t}{⇝} (J) x) \land r \in ℝ^{+}) \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in (x ball (D) (\frac{r}{2}))$
39	1	rexanuz2	$⊢ \exists j \in Z \forall k \in ℤ_{\geq j} ({(\frac{1}{2})}^{k} < \frac{r}{2} \land F (k) \in (x ball (D) (\frac{r}{2}))) \leftrightarrow (\exists j \in Z \forall k \in ℤ_{\geq j} {(\frac{1}{2})}^{k} < \frac{r}{2} \land \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in (x ball (D) (\frac{r}{2})))$
40	1	r19.2uz	$⊢ \exists j \in Z \forall k \in ℤ_{\geq j} ({(\frac{1}{2})}^{k} < \frac{r}{2} \land F (k) \in (x ball (D) (\frac{r}{2}))) \to \exists k \in Z ({(\frac{1}{2})}^{k} < \frac{r}{2} \land F (k) \in (x ball (D) (\frac{r}{2})))$
41	8	ad3antrrr	$⊢ (((φ \land F \underset{t}{⇝} (J) x) \land r \in ℝ^{+}) \land (k \in Z \land ({(\frac{1}{2})}^{k} < \frac{r}{2} \land F (k) \in (x ball (D) (\frac{r}{2}))))) \to G \in Fil (X)$
42	9	ad3antrrr	$⊢ (((φ \land F \underset{t}{⇝} (J) x) \land r \in ℝ^{+}) \land (k \in Z \land ({(\frac{1}{2})}^{k} < \frac{r}{2} \land F (k) \in (x ball (D) (\frac{r}{2}))))) \to S : ℤ ⟶ G$
43		eluzelz	$⊢ k \in ℤ_{\geq M} \to k \in ℤ$
44	43 1	eleq2s	$⊢ k \in Z \to k \in ℤ$
45	44	ad2antrl	$⊢ (((φ \land F \underset{t}{⇝} (J) x) \land r \in ℝ^{+}) \land (k \in Z \land ({(\frac{1}{2})}^{k} < \frac{r}{2} \land F (k) \in (x ball (D) (\frac{r}{2}))))) \to k \in ℤ$
46		ffvelrn	$⊢ (S : ℤ ⟶ G \land k \in ℤ) \to S (k) \in G$
47	42 45 46	syl2anc	$⊢ (((φ \land F \underset{t}{⇝} (J) x) \land r \in ℝ^{+}) \land (k \in Z \land ({(\frac{1}{2})}^{k} < \frac{r}{2} \land F (k) \in (x ball (D) (\frac{r}{2}))))) \to S (k) \in G$
48		rpxr	$⊢ r \in ℝ^{+} \to r \in ℝ^{*}$
49	48	adantl	$⊢ ((φ \land F \underset{t}{⇝} (J) x) \land r \in ℝ^{+}) \to r \in ℝ^{*}$
50		blssm	$⊢ (D \in ∞Met (X) \land x \in X \land r \in ℝ^{*}) \to x ball (D) r \subseteq X$
51	30 31 49 50	syl3anc	$⊢ ((φ \land F \underset{t}{⇝} (J) x) \land r \in ℝ^{+}) \to x ball (D) r \subseteq X$
52	51	adantr	$⊢ (((φ \land F \underset{t}{⇝} (J) x) \land r \in ℝ^{+}) \land (k \in Z \land ({(\frac{1}{2})}^{k} < \frac{r}{2} \land F (k) \in (x ball (D) (\frac{r}{2}))))) \to x ball (D) r \subseteq X$
53	44	adantl	$⊢ (((φ \land F \underset{t}{⇝} (J) x) \land r \in ℝ^{+}) \land k \in Z) \to k \in ℤ$
54		1rp	$⊢ 1 \in ℝ^{+}$
55		rphalfcl	$⊢ 1 \in ℝ^{+} \to \frac{1}{2} \in ℝ^{+}$
56	54 55	ax-mp	$⊢ \frac{1}{2} \in ℝ^{+}$
57		rpexpcl	$⊢ (\frac{1}{2} \in ℝ^{+} \land k \in ℤ) \to {(\frac{1}{2})}^{k} \in ℝ^{+}$
58	56 57	mpan	$⊢ k \in ℤ \to {(\frac{1}{2})}^{k} \in ℝ^{+}$
59	53 58	syl	$⊢ (((φ \land F \underset{t}{⇝} (J) x) \land r \in ℝ^{+}) \land k \in Z) \to {(\frac{1}{2})}^{k} \in ℝ^{+}$
60	59	rpred	$⊢ (((φ \land F \underset{t}{⇝} (J) x) \land r \in ℝ^{+}) \land k \in Z) \to {(\frac{1}{2})}^{k} \in ℝ$
61	27	adantr	$⊢ (((φ \land F \underset{t}{⇝} (J) x) \land r \in ℝ^{+}) \land k \in Z) \to \frac{r}{2} \in ℝ^{+}$
62	61	rpred	$⊢ (((φ \land F \underset{t}{⇝} (J) x) \land r \in ℝ^{+}) \land k \in Z) \to \frac{r}{2} \in ℝ$
63		ltle	$⊢ ({(\frac{1}{2})}^{k} \in ℝ \land \frac{r}{2} \in ℝ) \to ({(\frac{1}{2})}^{k} < \frac{r}{2} \to {(\frac{1}{2})}^{k} \leq \frac{r}{2})$
64	60 62 63	syl2anc	$⊢ (((φ \land F \underset{t}{⇝} (J) x) \land r \in ℝ^{+}) \land k \in Z) \to ({(\frac{1}{2})}^{k} < \frac{r}{2} \to {(\frac{1}{2})}^{k} \leq \frac{r}{2})$
65		fveq2	$⊢ n = k \to S (n) = S (k)$
66	65	eleq2d	$⊢ n = k \to (F (k) \in S (n) \leftrightarrow F (k) \in S (k))$
67	7	r19.21bi	$⊢ (φ \land k \in Z) \to \forall n \in (M \dots k) F (k) \in S (n)$
68		eluzfz2	$⊢ k \in ℤ_{\geq M} \to k \in (M \dots k)$
69	68 1	eleq2s	$⊢ k \in Z \to k \in (M \dots k)$
70	69	adantl	$⊢ (φ \land k \in Z) \to k \in (M \dots k)$
71	66 67 70	rspcdva	$⊢ (φ \land k \in Z) \to F (k) \in S (k)$
72	71	adantr	$⊢ ((φ \land k \in Z) \land y \in S (k)) \to F (k) \in S (k)$
73		simpr	$⊢ ((φ \land k \in Z) \land y \in S (k)) \to y \in S (k)$
74	6	ad2antrr	$⊢ ((φ \land k \in Z) \land y \in S (k)) \to \forall k \in ℤ \forall u \in S (k) \forall v \in S (k) u D v < {(\frac{1}{2})}^{k}$
75	44	ad2antlr	$⊢ ((φ \land k \in Z) \land y \in S (k)) \to k \in ℤ$
76		rsp	$⊢ \forall k \in ℤ \forall u \in S (k) \forall v \in S (k) u D v < {(\frac{1}{2})}^{k} \to (k \in ℤ \to \forall u \in S (k) \forall v \in S (k) u D v < {(\frac{1}{2})}^{k})$
77	74 75 76	sylc	$⊢ ((φ \land k \in Z) \land y \in S (k)) \to \forall u \in S (k) \forall v \in S (k) u D v < {(\frac{1}{2})}^{k}$
78		oveq1	$⊢ u = F (k) \to u D v = F (k) D v$
79	78	breq1d	$⊢ u = F (k) \to (u D v < {(\frac{1}{2})}^{k} \leftrightarrow F (k) D v < {(\frac{1}{2})}^{k})$
80		oveq2	$⊢ v = y \to F (k) D v = F (k) D y$
81	80	breq1d	$⊢ v = y \to (F (k) D v < {(\frac{1}{2})}^{k} \leftrightarrow F (k) D y < {(\frac{1}{2})}^{k})$
82	79 81	rspc2va	$⊢ ((F (k) \in S (k) \land y \in S (k)) \land \forall u \in S (k) \forall v \in S (k) u D v < {(\frac{1}{2})}^{k}) \to F (k) D y < {(\frac{1}{2})}^{k}$
83	72 73 77 82	syl21anc	$⊢ ((φ \land k \in Z) \land y \in S (k)) \to F (k) D y < {(\frac{1}{2})}^{k}$
84	15	ad2antrr	$⊢ ((φ \land k \in Z) \land y \in S (k)) \to D \in ∞Met (X)$
85	44 58	syl	$⊢ k \in Z \to {(\frac{1}{2})}^{k} \in ℝ^{+}$
86	85	rpxrd	$⊢ k \in Z \to {(\frac{1}{2})}^{k} \in ℝ^{*}$
87	86	ad2antlr	$⊢ ((φ \land k \in Z) \land y \in S (k)) \to {(\frac{1}{2})}^{k} \in ℝ^{*}$
88	5	ffvelrnda	$⊢ (φ \land k \in Z) \to F (k) \in X$
89	88	adantr	$⊢ ((φ \land k \in Z) \land y \in S (k)) \to F (k) \in X$
90	8	adantr	$⊢ (φ \land k \in Z) \to G \in Fil (X)$
91	9 44 46	syl2an	$⊢ (φ \land k \in Z) \to S (k) \in G$
92		filelss	$⊢ (G \in Fil (X) \land S (k) \in G) \to S (k) \subseteq X$
93	90 91 92	syl2anc	$⊢ (φ \land k \in Z) \to S (k) \subseteq X$
94	93	sselda	$⊢ ((φ \land k \in Z) \land y \in S (k)) \to y \in X$
95		elbl2	$⊢ ((D \in ∞Met (X) \land {(\frac{1}{2})}^{k} \in ℝ^{*}) \land (F (k) \in X \land y \in X)) \to (y \in (F (k) ball (D) {(\frac{1}{2})}^{k}) \leftrightarrow F (k) D y < {(\frac{1}{2})}^{k})$
96	84 87 89 94 95	syl22anc	$⊢ ((φ \land k \in Z) \land y \in S (k)) \to (y \in (F (k) ball (D) {(\frac{1}{2})}^{k}) \leftrightarrow F (k) D y < {(\frac{1}{2})}^{k})$
97	83 96	mpbird	$⊢ ((φ \land k \in Z) \land y \in S (k)) \to y \in (F (k) ball (D) {(\frac{1}{2})}^{k})$
98	97	ex	$⊢ (φ \land k \in Z) \to (y \in S (k) \to y \in (F (k) ball (D) {(\frac{1}{2})}^{k}))$
99	98	ssrdv	$⊢ (φ \land k \in Z) \to S (k) \subseteq F (k) ball (D) {(\frac{1}{2})}^{k}$
100	99	ad4ant14	$⊢ (((φ \land F \underset{t}{⇝} (J) x) \land r \in ℝ^{+}) \land k \in Z) \to S (k) \subseteq F (k) ball (D) {(\frac{1}{2})}^{k}$
101	30	adantr	$⊢ (((φ \land F \underset{t}{⇝} (J) x) \land r \in ℝ^{+}) \land k \in Z) \to D \in ∞Met (X)$
102	5	ad2antrr	$⊢ ((φ \land F \underset{t}{⇝} (J) x) \land r \in ℝ^{+}) \to F : Z ⟶ X$
103	102	ffvelrnda	$⊢ (((φ \land F \underset{t}{⇝} (J) x) \land r \in ℝ^{+}) \land k \in Z) \to F (k) \in X$
104	59	rpxrd	$⊢ (((φ \land F \underset{t}{⇝} (J) x) \land r \in ℝ^{+}) \land k \in Z) \to {(\frac{1}{2})}^{k} \in ℝ^{*}$
105	35	adantr	$⊢ (((φ \land F \underset{t}{⇝} (J) x) \land r \in ℝ^{+}) \land k \in Z) \to \frac{r}{2} \in ℝ^{*}$
106		ssbl	$⊢ ((D \in ∞Met (X) \land F (k) \in X) \land ({(\frac{1}{2})}^{k} \in ℝ^{} \land \frac{r}{2} \in ℝ^{}) \land {(\frac{1}{2})}^{k} \leq \frac{r}{2}) \to F (k) ball (D) {(\frac{1}{2})}^{k} \subseteq F (k) ball (D) (\frac{r}{2})$
107	106	3expia	$⊢ ((D \in ∞Met (X) \land F (k) \in X) \land ({(\frac{1}{2})}^{k} \in ℝ^{} \land \frac{r}{2} \in ℝ^{})) \to ({(\frac{1}{2})}^{k} \leq \frac{r}{2} \to F (k) ball (D) {(\frac{1}{2})}^{k} \subseteq F (k) ball (D) (\frac{r}{2}))$
108	101 103 104 105 107	syl22anc	$⊢ (((φ \land F \underset{t}{⇝} (J) x) \land r \in ℝ^{+}) \land k \in Z) \to ({(\frac{1}{2})}^{k} \leq \frac{r}{2} \to F (k) ball (D) {(\frac{1}{2})}^{k} \subseteq F (k) ball (D) (\frac{r}{2}))$
109		sstr	$⊢ (S (k) \subseteq F (k) ball (D) {(\frac{1}{2})}^{k} \land F (k) ball (D) {(\frac{1}{2})}^{k} \subseteq F (k) ball (D) (\frac{r}{2})) \to S (k) \subseteq F (k) ball (D) (\frac{r}{2})$
110	100 108 109	syl6an	$⊢ (((φ \land F \underset{t}{⇝} (J) x) \land r \in ℝ^{+}) \land k \in Z) \to ({(\frac{1}{2})}^{k} \leq \frac{r}{2} \to S (k) \subseteq F (k) ball (D) (\frac{r}{2}))$
111	64 110	syld	$⊢ (((φ \land F \underset{t}{⇝} (J) x) \land r \in ℝ^{+}) \land k \in Z) \to ({(\frac{1}{2})}^{k} < \frac{r}{2} \to S (k) \subseteq F (k) ball (D) (\frac{r}{2}))$
112	111	adantrd	$⊢ (((φ \land F \underset{t}{⇝} (J) x) \land r \in ℝ^{+}) \land k \in Z) \to (({(\frac{1}{2})}^{k} < \frac{r}{2} \land F (k) \in (x ball (D) (\frac{r}{2}))) \to S (k) \subseteq F (k) ball (D) (\frac{r}{2}))$
113	112	impr	$⊢ (((φ \land F \underset{t}{⇝} (J) x) \land r \in ℝ^{+}) \land (k \in Z \land ({(\frac{1}{2})}^{k} < \frac{r}{2} \land F (k) \in (x ball (D) (\frac{r}{2}))))) \to S (k) \subseteq F (k) ball (D) (\frac{r}{2})$
114	31	adantr	$⊢ (((φ \land F \underset{t}{⇝} (J) x) \land r \in ℝ^{+}) \land k \in Z) \to x \in X$
115		blcom	$⊢ ((D \in ∞Met (X) \land \frac{r}{2} \in ℝ^{*}) \land (x \in X \land F (k) \in X)) \to (F (k) \in (x ball (D) (\frac{r}{2})) \leftrightarrow x \in (F (k) ball (D) (\frac{r}{2})))$
116	101 105 114 103 115	syl22anc	$⊢ (((φ \land F \underset{t}{⇝} (J) x) \land r \in ℝ^{+}) \land k \in Z) \to (F (k) \in (x ball (D) (\frac{r}{2})) \leftrightarrow x \in (F (k) ball (D) (\frac{r}{2})))$
117		rpre	$⊢ r \in ℝ^{+} \to r \in ℝ$
118	117	ad2antlr	$⊢ (((φ \land F \underset{t}{⇝} (J) x) \land r \in ℝ^{+}) \land k \in Z) \to r \in ℝ$
119		blhalf	$⊢ ((D \in ∞Met (X) \land F (k) \in X) \land (r \in ℝ \land x \in (F (k) ball (D) (\frac{r}{2})))) \to F (k) ball (D) (\frac{r}{2}) \subseteq x ball (D) r$
120	119	expr	$⊢ ((D \in ∞Met (X) \land F (k) \in X) \land r \in ℝ) \to (x \in (F (k) ball (D) (\frac{r}{2})) \to F (k) ball (D) (\frac{r}{2}) \subseteq x ball (D) r)$
121	101 103 118 120	syl21anc	$⊢ (((φ \land F \underset{t}{⇝} (J) x) \land r \in ℝ^{+}) \land k \in Z) \to (x \in (F (k) ball (D) (\frac{r}{2})) \to F (k) ball (D) (\frac{r}{2}) \subseteq x ball (D) r)$
122	116 121	sylbid	$⊢ (((φ \land F \underset{t}{⇝} (J) x) \land r \in ℝ^{+}) \land k \in Z) \to (F (k) \in (x ball (D) (\frac{r}{2})) \to F (k) ball (D) (\frac{r}{2}) \subseteq x ball (D) r)$
123	122	adantld	$⊢ (((φ \land F \underset{t}{⇝} (J) x) \land r \in ℝ^{+}) \land k \in Z) \to (({(\frac{1}{2})}^{k} < \frac{r}{2} \land F (k) \in (x ball (D) (\frac{r}{2}))) \to F (k) ball (D) (\frac{r}{2}) \subseteq x ball (D) r)$
124	123	impr	$⊢ (((φ \land F \underset{t}{⇝} (J) x) \land r \in ℝ^{+}) \land (k \in Z \land ({(\frac{1}{2})}^{k} < \frac{r}{2} \land F (k) \in (x ball (D) (\frac{r}{2}))))) \to F (k) ball (D) (\frac{r}{2}) \subseteq x ball (D) r$
125	113 124	sstrd	$⊢ (((φ \land F \underset{t}{⇝} (J) x) \land r \in ℝ^{+}) \land (k \in Z \land ({(\frac{1}{2})}^{k} < \frac{r}{2} \land F (k) \in (x ball (D) (\frac{r}{2}))))) \to S (k) \subseteq x ball (D) r$
126		filss	$⊢ (G \in Fil (X) \land (S (k) \in G \land x ball (D) r \subseteq X \land S (k) \subseteq x ball (D) r)) \to x ball (D) r \in G$
127	41 47 52 125 126	syl13anc	$⊢ (((φ \land F \underset{t}{⇝} (J) x) \land r \in ℝ^{+}) \land (k \in Z \land ({(\frac{1}{2})}^{k} < \frac{r}{2} \land F (k) \in (x ball (D) (\frac{r}{2}))))) \to x ball (D) r \in G$
128	127	rexlimdvaa	$⊢ ((φ \land F \underset{t}{⇝} (J) x) \land r \in ℝ^{+}) \to (\exists k \in Z ({(\frac{1}{2})}^{k} < \frac{r}{2} \land F (k) \in (x ball (D) (\frac{r}{2}))) \to x ball (D) r \in G)$
129	40 128	syl5	$⊢ ((φ \land F \underset{t}{⇝} (J) x) \land r \in ℝ^{+}) \to (\exists j \in Z \forall k \in ℤ_{\geq j} ({(\frac{1}{2})}^{k} < \frac{r}{2} \land F (k) \in (x ball (D) (\frac{r}{2}))) \to x ball (D) r \in G)$
130	39 129	syl5bir	$⊢ ((φ \land F \underset{t}{⇝} (J) x) \land r \in ℝ^{+}) \to ((\exists j \in Z \forall k \in ℤ_{\geq j} {(\frac{1}{2})}^{k} < \frac{r}{2} \land \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in (x ball (D) (\frac{r}{2}))) \to x ball (D) r \in G)$
131	29 38 130	mp2and	$⊢ ((φ \land F \underset{t}{⇝} (J) x) \land r \in ℝ^{+}) \to x ball (D) r \in G$
132	131	ad2ant2r	$⊢ (((φ \land F \underset{t}{⇝} (J) x) \land y \in J) \land (r \in ℝ^{+} \land x ball (D) r \subseteq y)) \to x ball (D) r \in G$
133	17	adantr	$⊢ (φ \land F \underset{t}{⇝} (J) x) \to J \in TopOn (X)$
134		toponss	$⊢ (J \in TopOn (X) \land y \in J) \to y \subseteq X$
135	133 134	sylan	$⊢ ((φ \land F \underset{t}{⇝} (J) x) \land y \in J) \to y \subseteq X$
136	135	adantr	$⊢ (((φ \land F \underset{t}{⇝} (J) x) \land y \in J) \land (r \in ℝ^{+} \land x ball (D) r \subseteq y)) \to y \subseteq X$
137		simprr	$⊢ (((φ \land F \underset{t}{⇝} (J) x) \land y \in J) \land (r \in ℝ^{+} \land x ball (D) r \subseteq y)) \to x ball (D) r \subseteq y$
138		filss	$⊢ (G \in Fil (X) \land (x ball (D) r \in G \land y \subseteq X \land x ball (D) r \subseteq y)) \to y \in G$
139	24 132 136 137 138	syl13anc	$⊢ (((φ \land F \underset{t}{⇝} (J) x) \land y \in J) \land (r \in ℝ^{+} \land x ball (D) r \subseteq y)) \to y \in G$
140	139	rexlimdvaa	$⊢ ((φ \land F \underset{t}{⇝} (J) x) \land y \in J) \to (\exists r \in ℝ^{+} x ball (D) r \subseteq y \to y \in G)$
141	23 140	syld	$⊢ ((φ \land F \underset{t}{⇝} (J) x) \land y \in J) \to (x \in y \to y \in G)$
142	141	ralrimiva	$⊢ (φ \land F \underset{t}{⇝} (J) x) \to \forall y \in J (x \in y \to y \in G)$
143		flimopn	$⊢ (J \in TopOn (X) \land G \in Fil (X)) \to (x \in (J fLim G) \leftrightarrow (x \in X \land \forall y \in J (x \in y \to y \in G)))$
144	17 8 143	syl2anc	$⊢ φ \to (x \in (J fLim G) \leftrightarrow (x \in X \land \forall y \in J (x \in y \to y \in G)))$
145	144	adantr	$⊢ (φ \land F \underset{t}{⇝} (J) x) \to (x \in (J fLim G) \leftrightarrow (x \in X \land \forall y \in J (x \in y \to y \in G)))$
146	19 142 145	mpbir2and	$⊢ (φ \land F \underset{t}{⇝} (J) x) \to x \in (J fLim G)$
147	146	ne0d	$⊢ (φ \land F \underset{t}{⇝} (J) x) \to J fLim G \neq \emptyset$
148	13 147	exlimddv	$⊢ φ \to J fLim G \neq \emptyset$

Metamath Proof Explorer

Theorem iscmet3lem2

Proof