heibor1lem

Description: Lemma for heibor1 . A compact metric space is complete. This proof works by considering the collection cls ( F " ( ZZ>=n ) ) for each n e. NN , which has the finite intersection property because any finite intersection of upper integer sets is another upper integer set, so any finite intersection of the image closures will contain ( F " ( ZZ>=m ) ) for some m . Thus, by compactness, the intersection contains a point y , which must then be the convergent point of F . (Contributed by Jeff Madsen, 17-Jan-2014) (Revised by Mario Carneiro, 5-Jun-2014)

	Ref	Expression
Hypotheses	heibor.1	$⊢ J = MetOpen (D)$
	heibor1.3	$⊢ φ \to D \in Met (X)$
	heibor1.4	$⊢ φ \to J \in Comp$
	heibor1.5	$⊢ φ \to F \in Cau (D)$
	heibor1.6	$⊢ φ \to F : ℕ ⟶ X$
Assertion	heibor1lem	$⊢ φ \to F \in dom \underset{t}{⇝} (J)$

Proof

Step	Hyp	Ref	Expression
1		heibor.1	$⊢ J = MetOpen (D)$
2		heibor1.3	$⊢ φ \to D \in Met (X)$
3		heibor1.4	$⊢ φ \to J \in Comp$
4		heibor1.5	$⊢ φ \to F \in Cau (D)$
5		heibor1.6	$⊢ φ \to F : ℕ ⟶ X$
6		metxmet	$⊢ D \in Met (X) \to D \in ∞Met (X)$
7	2 6	syl	$⊢ φ \to D \in ∞Met (X)$
8	1	mopntop	$⊢ D \in ∞Met (X) \to J \in Top$
9	7 8	syl	$⊢ φ \to J \in Top$
10		imassrn	$⊢ F [u] \subseteq ran F$
11	5	frnd	$⊢ φ \to ran F \subseteq X$
12	1	mopnuni	$⊢ D \in ∞Met (X) \to X = ⋃ J$
13	7 12	syl	$⊢ φ \to X = ⋃ J$
14	11 13	sseqtrd	$⊢ φ \to ran F \subseteq ⋃ J$
15	10 14	sstrid	$⊢ φ \to F [u] \subseteq ⋃ J$
16		eqid	$⊢ ⋃ J = ⋃ J$
17	16	clscld	$⊢ (J \in Top \land F [u] \subseteq ⋃ J) \to cls (J) (F [u]) \in Clsd (J)$
18	9 15 17	syl2anc	$⊢ φ \to cls (J) (F [u]) \in Clsd (J)$
19		eleq1a	$⊢ cls (J) (F [u]) \in Clsd (J) \to (k = cls (J) (F [u]) \to k \in Clsd (J))$
20	18 19	syl	$⊢ φ \to (k = cls (J) (F [u]) \to k \in Clsd (J))$
21	20	rexlimdvw	$⊢ φ \to (\exists u \in ran ℤ_{\geq} k = cls (J) (F [u]) \to k \in Clsd (J))$
22	21	abssdv	$⊢ φ \to \{k \| \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])\} \subseteq Clsd (J)$
23		fvex	$⊢ Clsd (J) \in V$
24	23	elpw2	$⊢ \{k \| \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])\} \in 𝒫 Clsd (J) \leftrightarrow \{k \| \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])\} \subseteq Clsd (J)$
25	22 24	sylibr	$⊢ φ \to \{k \| \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])\} \in 𝒫 Clsd (J)$
26		elin	$⊢ r \in (𝒫 \{k \| \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])\} \cap Fin) \leftrightarrow (r \in 𝒫 \{k \| \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])\} \land r \in Fin)$
27		velpw	$⊢ r \in 𝒫 \{k \| \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])\} \leftrightarrow r \subseteq \{k \| \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])\}$
28		ssabral	$⊢ r \subseteq \{k \| \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])\} \leftrightarrow \forall k \in r \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])$
29	27 28	bitri	$⊢ r \in 𝒫 \{k \| \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])\} \leftrightarrow \forall k \in r \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])$
30	29	anbi1i	$⊢ (r \in 𝒫 \{k \| \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])\} \land r \in Fin) \leftrightarrow (\forall k \in r \exists u \in ran ℤ_{\geq} k = cls (J) (F [u]) \land r \in Fin)$
31	26 30	bitri	$⊢ r \in (𝒫 \{k \| \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])\} \cap Fin) \leftrightarrow (\forall k \in r \exists u \in ran ℤ_{\geq} k = cls (J) (F [u]) \land r \in Fin)$
32		raleq	$⊢ m = \emptyset \to (\forall k \in m \exists u \in ran ℤ_{\geq} k = cls (J) (F [u]) \leftrightarrow \forall k \in \emptyset \exists u \in ran ℤ_{\geq} k = cls (J) (F [u]))$
33	32	anbi2d	$⊢ m = \emptyset \to ((φ \land \forall k \in m \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])) \leftrightarrow (φ \land \forall k \in \emptyset \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])))$
34		inteq	$⊢ m = \emptyset \to ⋂ m = ⋂ \emptyset$
35	34	sseq2d	$⊢ m = \emptyset \to (F [k] \subseteq ⋂ m \leftrightarrow F [k] \subseteq ⋂ \emptyset)$
36	35	rexbidv	$⊢ m = \emptyset \to (\exists k \in ran ℤ_{\geq} F [k] \subseteq ⋂ m \leftrightarrow \exists k \in ran ℤ_{\geq} F [k] \subseteq ⋂ \emptyset)$
37	33 36	imbi12d	$⊢ m = \emptyset \to (((φ \land \forall k \in m \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])) \to \exists k \in ran ℤ_{\geq} F [k] \subseteq ⋂ m) \leftrightarrow ((φ \land \forall k \in \emptyset \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])) \to \exists k \in ran ℤ_{\geq} F [k] \subseteq ⋂ \emptyset))$
38		raleq	$⊢ m = y \to (\forall k \in m \exists u \in ran ℤ_{\geq} k = cls (J) (F [u]) \leftrightarrow \forall k \in y \exists u \in ran ℤ_{\geq} k = cls (J) (F [u]))$
39	38	anbi2d	$⊢ m = y \to ((φ \land \forall k \in m \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])) \leftrightarrow (φ \land \forall k \in y \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])))$
40		inteq	$⊢ m = y \to ⋂ m = ⋂ y$
41	40	sseq2d	$⊢ m = y \to (F [k] \subseteq ⋂ m \leftrightarrow F [k] \subseteq ⋂ y)$
42	41	rexbidv	$⊢ m = y \to (\exists k \in ran ℤ_{\geq} F [k] \subseteq ⋂ m \leftrightarrow \exists k \in ran ℤ_{\geq} F [k] \subseteq ⋂ y)$
43	39 42	imbi12d	$⊢ m = y \to (((φ \land \forall k \in m \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])) \to \exists k \in ran ℤ_{\geq} F [k] \subseteq ⋂ m) \leftrightarrow ((φ \land \forall k \in y \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])) \to \exists k \in ran ℤ_{\geq} F [k] \subseteq ⋂ y))$
44		raleq	$⊢ m = y \cup \{n\} \to (\forall k \in m \exists u \in ran ℤ_{\geq} k = cls (J) (F [u]) \leftrightarrow \forall k \in (y \cup \{n\}) \exists u \in ran ℤ_{\geq} k = cls (J) (F [u]))$
45	44	anbi2d	$⊢ m = y \cup \{n\} \to ((φ \land \forall k \in m \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])) \leftrightarrow (φ \land \forall k \in (y \cup \{n\}) \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])))$
46		inteq	$⊢ m = y \cup \{n\} \to ⋂ m = ⋂ (y \cup \{n\})$
47	46	sseq2d	$⊢ m = y \cup \{n\} \to (F [k] \subseteq ⋂ m \leftrightarrow F [k] \subseteq ⋂ (y \cup \{n\}))$
48	47	rexbidv	$⊢ m = y \cup \{n\} \to (\exists k \in ran ℤ_{\geq} F [k] \subseteq ⋂ m \leftrightarrow \exists k \in ran ℤ_{\geq} F [k] \subseteq ⋂ (y \cup \{n\}))$
49	45 48	imbi12d	$⊢ m = y \cup \{n\} \to (((φ \land \forall k \in m \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])) \to \exists k \in ran ℤ_{\geq} F [k] \subseteq ⋂ m) \leftrightarrow ((φ \land \forall k \in (y \cup \{n\}) \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])) \to \exists k \in ran ℤ_{\geq} F [k] \subseteq ⋂ (y \cup \{n\})))$
50		raleq	$⊢ m = r \to (\forall k \in m \exists u \in ran ℤ_{\geq} k = cls (J) (F [u]) \leftrightarrow \forall k \in r \exists u \in ran ℤ_{\geq} k = cls (J) (F [u]))$
51	50	anbi2d	$⊢ m = r \to ((φ \land \forall k \in m \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])) \leftrightarrow (φ \land \forall k \in r \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])))$
52		inteq	$⊢ m = r \to ⋂ m = ⋂ r$
53	52	sseq2d	$⊢ m = r \to (F [k] \subseteq ⋂ m \leftrightarrow F [k] \subseteq ⋂ r)$
54	53	rexbidv	$⊢ m = r \to (\exists k \in ran ℤ_{\geq} F [k] \subseteq ⋂ m \leftrightarrow \exists k \in ran ℤ_{\geq} F [k] \subseteq ⋂ r)$
55	51 54	imbi12d	$⊢ m = r \to (((φ \land \forall k \in m \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])) \to \exists k \in ran ℤ_{\geq} F [k] \subseteq ⋂ m) \leftrightarrow ((φ \land \forall k \in r \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])) \to \exists k \in ran ℤ_{\geq} F [k] \subseteq ⋂ r))$
56		uzf	$⊢ ℤ_{\geq} : ℤ ⟶ 𝒫 ℤ$
57		ffn	$⊢ ℤ_{\geq} : ℤ ⟶ 𝒫 ℤ \to ℤ_{\geq} Fn ℤ$
58	56 57	ax-mp	$⊢ ℤ_{\geq} Fn ℤ$
59		0z	$⊢ 0 \in ℤ$
60		fnfvelrn	$⊢ (ℤ_{\geq} Fn ℤ \land 0 \in ℤ) \to ℤ_{\geq 0} \in ran ℤ_{\geq}$
61	58 59 60	mp2an	$⊢ ℤ_{\geq 0} \in ran ℤ_{\geq}$
62		ssv	$⊢ F [ℤ_{\geq 0}] \subseteq V$
63		int0	$⊢ ⋂ \emptyset = V$
64	62 63	sseqtrri	$⊢ F [ℤ_{\geq 0}] \subseteq ⋂ \emptyset$
65		imaeq2	$⊢ k = ℤ_{\geq 0} \to F [k] = F [ℤ_{\geq 0}]$
66	65	sseq1d	$⊢ k = ℤ_{\geq 0} \to (F [k] \subseteq ⋂ \emptyset \leftrightarrow F [ℤ_{\geq 0}] \subseteq ⋂ \emptyset)$
67	66	rspcev	$⊢ (ℤ_{\geq 0} \in ran ℤ_{\geq} \land F [ℤ_{\geq 0}] \subseteq ⋂ \emptyset) \to \exists k \in ran ℤ_{\geq} F [k] \subseteq ⋂ \emptyset$
68	61 64 67	mp2an	$⊢ \exists k \in ran ℤ_{\geq} F [k] \subseteq ⋂ \emptyset$
69	68	a1i	$⊢ (φ \land \forall k \in \emptyset \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])) \to \exists k \in ran ℤ_{\geq} F [k] \subseteq ⋂ \emptyset$
70		ssun1	$⊢ y \subseteq y \cup \{n\}$
71		ssralv	$⊢ y \subseteq y \cup \{n\} \to (\forall k \in (y \cup \{n\}) \exists u \in ran ℤ_{\geq} k = cls (J) (F [u]) \to \forall k \in y \exists u \in ran ℤ_{\geq} k = cls (J) (F [u]))$
72	70 71	ax-mp	$⊢ \forall k \in (y \cup \{n\}) \exists u \in ran ℤ_{\geq} k = cls (J) (F [u]) \to \forall k \in y \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])$
73	72	anim2i	$⊢ (φ \land \forall k \in (y \cup \{n\}) \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])) \to (φ \land \forall k \in y \exists u \in ran ℤ_{\geq} k = cls (J) (F [u]))$
74	73	imim1i	$⊢ ((φ \land \forall k \in y \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])) \to \exists k \in ran ℤ_{\geq} F [k] \subseteq ⋂ y) \to ((φ \land \forall k \in (y \cup \{n\}) \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])) \to \exists k \in ran ℤ_{\geq} F [k] \subseteq ⋂ y)$
75		ssun2	$⊢ \{n\} \subseteq y \cup \{n\}$
76		ssralv	$⊢ \{n\} \subseteq y \cup \{n\} \to (\forall k \in (y \cup \{n\}) \exists u \in ran ℤ_{\geq} k = cls (J) (F [u]) \to \forall k \in \{n\} \exists u \in ran ℤ_{\geq} k = cls (J) (F [u]))$
77	75 76	ax-mp	$⊢ \forall k \in (y \cup \{n\}) \exists u \in ran ℤ_{\geq} k = cls (J) (F [u]) \to \forall k \in \{n\} \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])$
78		vex	$⊢ n \in V$
79		eqeq1	$⊢ k = n \to (k = cls (J) (F [u]) \leftrightarrow n = cls (J) (F [u]))$
80	79	rexbidv	$⊢ k = n \to (\exists u \in ran ℤ_{\geq} k = cls (J) (F [u]) \leftrightarrow \exists u \in ran ℤ_{\geq} n = cls (J) (F [u]))$
81	78 80	ralsn	$⊢ \forall k \in \{n\} \exists u \in ran ℤ_{\geq} k = cls (J) (F [u]) \leftrightarrow \exists u \in ran ℤ_{\geq} n = cls (J) (F [u])$
82	77 81	sylib	$⊢ \forall k \in (y \cup \{n\}) \exists u \in ran ℤ_{\geq} k = cls (J) (F [u]) \to \exists u \in ran ℤ_{\geq} n = cls (J) (F [u])$
83		uzin2	$⊢ (u \in ran ℤ_{\geq} \land k \in ran ℤ_{\geq}) \to u \cap k \in ran ℤ_{\geq}$
84	10 11	sstrid	$⊢ φ \to F [u] \subseteq X$
85	84 13	sseqtrd	$⊢ φ \to F [u] \subseteq ⋃ J$
86	16	sscls	$⊢ (J \in Top \land F [u] \subseteq ⋃ J) \to F [u] \subseteq cls (J) (F [u])$
87	9 85 86	syl2anc	$⊢ φ \to F [u] \subseteq cls (J) (F [u])$
88		sseq2	$⊢ n = cls (J) (F [u]) \to (F [u] \subseteq n \leftrightarrow F [u] \subseteq cls (J) (F [u]))$
89	87 88	syl5ibrcom	$⊢ φ \to (n = cls (J) (F [u]) \to F [u] \subseteq n)$
90		inss2	$⊢ u \cap k \subseteq k$
91		inss1	$⊢ u \cap k \subseteq u$
92		imass2	$⊢ u \cap k \subseteq k \to F [u \cap k] \subseteq F [k]$
93		imass2	$⊢ u \cap k \subseteq u \to F [u \cap k] \subseteq F [u]$
94	92 93	anim12i	$⊢ (u \cap k \subseteq k \land u \cap k \subseteq u) \to (F [u \cap k] \subseteq F [k] \land F [u \cap k] \subseteq F [u])$
95		ssin	$⊢ (F [u \cap k] \subseteq F [k] \land F [u \cap k] \subseteq F [u]) \leftrightarrow F [u \cap k] \subseteq F [k] \cap F [u]$
96	94 95	sylib	$⊢ (u \cap k \subseteq k \land u \cap k \subseteq u) \to F [u \cap k] \subseteq F [k] \cap F [u]$
97	90 91 96	mp2an	$⊢ F [u \cap k] \subseteq F [k] \cap F [u]$
98		ss2in	$⊢ (F [k] \subseteq ⋂ y \land F [u] \subseteq n) \to F [k] \cap F [u] \subseteq ⋂ y \cap n$
99	97 98	sstrid	$⊢ (F [k] \subseteq ⋂ y \land F [u] \subseteq n) \to F [u \cap k] \subseteq ⋂ y \cap n$
100	78	intunsn	$⊢ ⋂ (y \cup \{n\}) = ⋂ y \cap n$
101	99 100	sseqtrrdi	$⊢ (F [k] \subseteq ⋂ y \land F [u] \subseteq n) \to F [u \cap k] \subseteq ⋂ (y \cup \{n\})$
102	101	expcom	$⊢ F [u] \subseteq n \to (F [k] \subseteq ⋂ y \to F [u \cap k] \subseteq ⋂ (y \cup \{n\}))$
103	89 102	syl6	$⊢ φ \to (n = cls (J) (F [u]) \to (F [k] \subseteq ⋂ y \to F [u \cap k] \subseteq ⋂ (y \cup \{n\})))$
104	103	impd	$⊢ φ \to ((n = cls (J) (F [u]) \land F [k] \subseteq ⋂ y) \to F [u \cap k] \subseteq ⋂ (y \cup \{n\}))$
105		imaeq2	$⊢ m = u \cap k \to F [m] = F [u \cap k]$
106	105	sseq1d	$⊢ m = u \cap k \to (F [m] \subseteq ⋂ (y \cup \{n\}) \leftrightarrow F [u \cap k] \subseteq ⋂ (y \cup \{n\}))$
107	106	rspcev	$⊢ (u \cap k \in ran ℤ_{\geq} \land F [u \cap k] \subseteq ⋂ (y \cup \{n\})) \to \exists m \in ran ℤ_{\geq} F [m] \subseteq ⋂ (y \cup \{n\})$
108	107	expcom	$⊢ F [u \cap k] \subseteq ⋂ (y \cup \{n\}) \to (u \cap k \in ran ℤ_{\geq} \to \exists m \in ran ℤ_{\geq} F [m] \subseteq ⋂ (y \cup \{n\}))$
109	104 108	syl6	$⊢ φ \to ((n = cls (J) (F [u]) \land F [k] \subseteq ⋂ y) \to (u \cap k \in ran ℤ_{\geq} \to \exists m \in ran ℤ_{\geq} F [m] \subseteq ⋂ (y \cup \{n\})))$
110	109	com23	$⊢ φ \to (u \cap k \in ran ℤ_{\geq} \to ((n = cls (J) (F [u]) \land F [k] \subseteq ⋂ y) \to \exists m \in ran ℤ_{\geq} F [m] \subseteq ⋂ (y \cup \{n\})))$
111	83 110	syl5	$⊢ φ \to ((u \in ran ℤ_{\geq} \land k \in ran ℤ_{\geq}) \to ((n = cls (J) (F [u]) \land F [k] \subseteq ⋂ y) \to \exists m \in ran ℤ_{\geq} F [m] \subseteq ⋂ (y \cup \{n\})))$
112	111	rexlimdvv	$⊢ φ \to (\exists u \in ran ℤ_{\geq} \exists k \in ran ℤ_{\geq} (n = cls (J) (F [u]) \land F [k] \subseteq ⋂ y) \to \exists m \in ran ℤ_{\geq} F [m] \subseteq ⋂ (y \cup \{n\}))$
113		reeanv	$⊢ \exists u \in ran ℤ_{\geq} \exists k \in ran ℤ_{\geq} (n = cls (J) (F [u]) \land F [k] \subseteq ⋂ y) \leftrightarrow (\exists u \in ran ℤ_{\geq} n = cls (J) (F [u]) \land \exists k \in ran ℤ_{\geq} F [k] \subseteq ⋂ y)$
114		imaeq2	$⊢ m = k \to F [m] = F [k]$
115	114	sseq1d	$⊢ m = k \to (F [m] \subseteq ⋂ (y \cup \{n\}) \leftrightarrow F [k] \subseteq ⋂ (y \cup \{n\}))$
116	115	cbvrexvw	$⊢ \exists m \in ran ℤ_{\geq} F [m] \subseteq ⋂ (y \cup \{n\}) \leftrightarrow \exists k \in ran ℤ_{\geq} F [k] \subseteq ⋂ (y \cup \{n\})$
117	112 113 116	3imtr3g	$⊢ φ \to ((\exists u \in ran ℤ_{\geq} n = cls (J) (F [u]) \land \exists k \in ran ℤ_{\geq} F [k] \subseteq ⋂ y) \to \exists k \in ran ℤ_{\geq} F [k] \subseteq ⋂ (y \cup \{n\}))$
118	117	expd	$⊢ φ \to (\exists u \in ran ℤ_{\geq} n = cls (J) (F [u]) \to (\exists k \in ran ℤ_{\geq} F [k] \subseteq ⋂ y \to \exists k \in ran ℤ_{\geq} F [k] \subseteq ⋂ (y \cup \{n\})))$
119	82 118	syl5	$⊢ φ \to (\forall k \in (y \cup \{n\}) \exists u \in ran ℤ_{\geq} k = cls (J) (F [u]) \to (\exists k \in ran ℤ_{\geq} F [k] \subseteq ⋂ y \to \exists k \in ran ℤ_{\geq} F [k] \subseteq ⋂ (y \cup \{n\})))$
120	119	imp	$⊢ (φ \land \forall k \in (y \cup \{n\}) \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])) \to (\exists k \in ran ℤ_{\geq} F [k] \subseteq ⋂ y \to \exists k \in ran ℤ_{\geq} F [k] \subseteq ⋂ (y \cup \{n\}))$
121	74 120	sylcom	$⊢ ((φ \land \forall k \in y \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])) \to \exists k \in ran ℤ_{\geq} F [k] \subseteq ⋂ y) \to ((φ \land \forall k \in (y \cup \{n\}) \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])) \to \exists k \in ran ℤ_{\geq} F [k] \subseteq ⋂ (y \cup \{n\}))$
122	121	a1i	$⊢ y \in Fin \to (((φ \land \forall k \in y \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])) \to \exists k \in ran ℤ_{\geq} F [k] \subseteq ⋂ y) \to ((φ \land \forall k \in (y \cup \{n\}) \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])) \to \exists k \in ran ℤ_{\geq} F [k] \subseteq ⋂ (y \cup \{n\})))$
123	37 43 49 55 69 122	findcard2	$⊢ r \in Fin \to ((φ \land \forall k \in r \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])) \to \exists k \in ran ℤ_{\geq} F [k] \subseteq ⋂ r)$
124	123	com12	$⊢ (φ \land \forall k \in r \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])) \to (r \in Fin \to \exists k \in ran ℤ_{\geq} F [k] \subseteq ⋂ r)$
125	124	impr	$⊢ (φ \land (\forall k \in r \exists u \in ran ℤ_{\geq} k = cls (J) (F [u]) \land r \in Fin)) \to \exists k \in ran ℤ_{\geq} F [k] \subseteq ⋂ r$
126	5	ffnd	$⊢ φ \to F Fn ℕ$
127		inss1	$⊢ k \cap ℕ \subseteq k$
128		imass2	$⊢ k \cap ℕ \subseteq k \to F [k \cap ℕ] \subseteq F [k]$
129	127 128	ax-mp	$⊢ F [k \cap ℕ] \subseteq F [k]$
130		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
131		1z	$⊢ 1 \in ℤ$
132		fnfvelrn	$⊢ (ℤ_{\geq} Fn ℤ \land 1 \in ℤ) \to ℤ_{\geq 1} \in ran ℤ_{\geq}$
133	58 131 132	mp2an	$⊢ ℤ_{\geq 1} \in ran ℤ_{\geq}$
134	130 133	eqeltri	$⊢ ℕ \in ran ℤ_{\geq}$
135		uzin2	$⊢ (k \in ran ℤ_{\geq} \land ℕ \in ran ℤ_{\geq}) \to k \cap ℕ \in ran ℤ_{\geq}$
136	134 135	mpan2	$⊢ k \in ran ℤ_{\geq} \to k \cap ℕ \in ran ℤ_{\geq}$
137		uzn0	$⊢ k \cap ℕ \in ran ℤ_{\geq} \to k \cap ℕ \neq \emptyset$
138	136 137	syl	$⊢ k \in ran ℤ_{\geq} \to k \cap ℕ \neq \emptyset$
139		n0	$⊢ k \cap ℕ \neq \emptyset \leftrightarrow \exists y y \in (k \cap ℕ)$
140	138 139	sylib	$⊢ k \in ran ℤ_{\geq} \to \exists y y \in (k \cap ℕ)$
141		fnfun	$⊢ F Fn ℕ \to Fun F$
142		inss2	$⊢ k \cap ℕ \subseteq ℕ$
143		fndm	$⊢ F Fn ℕ \to dom F = ℕ$
144	142 143	sseqtrrid	$⊢ F Fn ℕ \to k \cap ℕ \subseteq dom F$
145		funfvima2	$⊢ (Fun F \land k \cap ℕ \subseteq dom F) \to (y \in (k \cap ℕ) \to F (y) \in F [k \cap ℕ])$
146	141 144 145	syl2anc	$⊢ F Fn ℕ \to (y \in (k \cap ℕ) \to F (y) \in F [k \cap ℕ])$
147		ne0i	$⊢ F (y) \in F [k \cap ℕ] \to F [k \cap ℕ] \neq \emptyset$
148	146 147	syl6	$⊢ F Fn ℕ \to (y \in (k \cap ℕ) \to F [k \cap ℕ] \neq \emptyset)$
149	148	exlimdv	$⊢ F Fn ℕ \to (\exists y y \in (k \cap ℕ) \to F [k \cap ℕ] \neq \emptyset)$
150	140 149	syl5	$⊢ F Fn ℕ \to (k \in ran ℤ_{\geq} \to F [k \cap ℕ] \neq \emptyset)$
151	150	imp	$⊢ (F Fn ℕ \land k \in ran ℤ_{\geq}) \to F [k \cap ℕ] \neq \emptyset$
152		ssn0	$⊢ (F [k \cap ℕ] \subseteq F [k] \land F [k \cap ℕ] \neq \emptyset) \to F [k] \neq \emptyset$
153	129 151 152	sylancr	$⊢ (F Fn ℕ \land k \in ran ℤ_{\geq}) \to F [k] \neq \emptyset$
154		ssn0	$⊢ (F [k] \subseteq ⋂ r \land F [k] \neq \emptyset) \to ⋂ r \neq \emptyset$
155	154	expcom	$⊢ F [k] \neq \emptyset \to (F [k] \subseteq ⋂ r \to ⋂ r \neq \emptyset)$
156	153 155	syl	$⊢ (F Fn ℕ \land k \in ran ℤ_{\geq}) \to (F [k] \subseteq ⋂ r \to ⋂ r \neq \emptyset)$
157	156	rexlimdva	$⊢ F Fn ℕ \to (\exists k \in ran ℤ_{\geq} F [k] \subseteq ⋂ r \to ⋂ r \neq \emptyset)$
158	126 157	syl	$⊢ φ \to (\exists k \in ran ℤ_{\geq} F [k] \subseteq ⋂ r \to ⋂ r \neq \emptyset)$
159	158	adantr	$⊢ (φ \land (\forall k \in r \exists u \in ran ℤ_{\geq} k = cls (J) (F [u]) \land r \in Fin)) \to (\exists k \in ran ℤ_{\geq} F [k] \subseteq ⋂ r \to ⋂ r \neq \emptyset)$
160	125 159	mpd	$⊢ (φ \land (\forall k \in r \exists u \in ran ℤ_{\geq} k = cls (J) (F [u]) \land r \in Fin)) \to ⋂ r \neq \emptyset$
161	160	necomd	$⊢ (φ \land (\forall k \in r \exists u \in ran ℤ_{\geq} k = cls (J) (F [u]) \land r \in Fin)) \to \emptyset \neq ⋂ r$
162	161	neneqd	$⊢ (φ \land (\forall k \in r \exists u \in ran ℤ_{\geq} k = cls (J) (F [u]) \land r \in Fin)) \to \neg \emptyset = ⋂ r$
163	31 162	sylan2b	$⊢ (φ \land r \in (𝒫 \{k \| \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])\} \cap Fin)) \to \neg \emptyset = ⋂ r$
164	163	nrexdv	$⊢ φ \to \neg \exists r \in (𝒫 \{k \| \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])\} \cap Fin) \emptyset = ⋂ r$
165		0ex	$⊢ \emptyset \in V$
166		zex	$⊢ ℤ \in V$
167	166	pwex	$⊢ 𝒫 ℤ \in V$
168		frn	$⊢ ℤ_{\geq} : ℤ ⟶ 𝒫 ℤ \to ran ℤ_{\geq} \subseteq 𝒫 ℤ$
169	56 168	ax-mp	$⊢ ran ℤ_{\geq} \subseteq 𝒫 ℤ$
170	167 169	ssexi	$⊢ ran ℤ_{\geq} \in V$
171	170	abrexex	$⊢ \{k \| \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])\} \in V$
172		elfi	$⊢ (\emptyset \in V \land \{k \| \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])\} \in V) \to (\emptyset \in fi (\{k \| \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])\}) \leftrightarrow \exists r \in (𝒫 \{k \| \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])\} \cap Fin) \emptyset = ⋂ r)$
173	165 171 172	mp2an	$⊢ \emptyset \in fi (\{k \| \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])\}) \leftrightarrow \exists r \in (𝒫 \{k \| \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])\} \cap Fin) \emptyset = ⋂ r$
174	164 173	sylnibr	$⊢ φ \to \neg \emptyset \in fi (\{k \| \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])\})$
175		cmptop	$⊢ J \in Comp \to J \in Top$
176		cmpfi	$⊢ J \in Top \to (J \in Comp \leftrightarrow \forall m \in 𝒫 Clsd (J) (\neg \emptyset \in fi (m) \to ⋂ m \neq \emptyset))$
177	175 176	syl	$⊢ J \in Comp \to (J \in Comp \leftrightarrow \forall m \in 𝒫 Clsd (J) (\neg \emptyset \in fi (m) \to ⋂ m \neq \emptyset))$
178	177	ibi	$⊢ J \in Comp \to \forall m \in 𝒫 Clsd (J) (\neg \emptyset \in fi (m) \to ⋂ m \neq \emptyset)$
179		fveq2	$⊢ m = \{k \| \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])\} \to fi (m) = fi (\{k \| \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])\})$
180	179	eleq2d	$⊢ m = \{k \| \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])\} \to (\emptyset \in fi (m) \leftrightarrow \emptyset \in fi (\{k \| \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])\}))$
181	180	notbid	$⊢ m = \{k \| \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])\} \to (\neg \emptyset \in fi (m) \leftrightarrow \neg \emptyset \in fi (\{k \| \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])\}))$
182		inteq	$⊢ m = \{k \| \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])\} \to ⋂ m = ⋂ \{k \| \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])\}$
183	182	neeq1d	$⊢ m = \{k \| \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])\} \to (⋂ m \neq \emptyset \leftrightarrow ⋂ \{k \| \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])\} \neq \emptyset)$
184		n0	$⊢ ⋂ \{k \| \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])\} \neq \emptyset \leftrightarrow \exists y y \in ⋂ \{k \| \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])\}$
185	183 184	bitrdi	$⊢ m = \{k \| \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])\} \to (⋂ m \neq \emptyset \leftrightarrow \exists y y \in ⋂ \{k \| \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])\})$
186	181 185	imbi12d	$⊢ m = \{k \| \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])\} \to ((\neg \emptyset \in fi (m) \to ⋂ m \neq \emptyset) \leftrightarrow (\neg \emptyset \in fi (\{k \| \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])\}) \to \exists y y \in ⋂ \{k \| \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])\}))$
187	186	rspccv	$⊢ \forall m \in 𝒫 Clsd (J) (\neg \emptyset \in fi (m) \to ⋂ m \neq \emptyset) \to (\{k \| \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])\} \in 𝒫 Clsd (J) \to (\neg \emptyset \in fi (\{k \| \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])\}) \to \exists y y \in ⋂ \{k \| \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])\}))$
188	178 187	syl	$⊢ J \in Comp \to (\{k \| \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])\} \in 𝒫 Clsd (J) \to (\neg \emptyset \in fi (\{k \| \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])\}) \to \exists y y \in ⋂ \{k \| \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])\}))$
189	3 25 174 188	syl3c	$⊢ φ \to \exists y y \in ⋂ \{k \| \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])\}$
190		lmrel	$⊢ Rel \underset{t}{⇝} (J)$
191		r19.23v	$⊢ \forall u \in ran ℤ_{\geq} (k = cls (J) (F [u]) \to y \in k) \leftrightarrow (\exists u \in ran ℤ_{\geq} k = cls (J) (F [u]) \to y \in k)$
192	191	albii	$⊢ \forall k \forall u \in ran ℤ_{\geq} (k = cls (J) (F [u]) \to y \in k) \leftrightarrow \forall k (\exists u \in ran ℤ_{\geq} k = cls (J) (F [u]) \to y \in k)$
193		fvex	$⊢ cls (J) (F [u]) \in V$
194		eleq2	$⊢ k = cls (J) (F [u]) \to (y \in k \leftrightarrow y \in cls (J) (F [u]))$
195	193 194	ceqsalv	$⊢ \forall k (k = cls (J) (F [u]) \to y \in k) \leftrightarrow y \in cls (J) (F [u])$
196	195	ralbii	$⊢ \forall u \in ran ℤ_{\geq} \forall k (k = cls (J) (F [u]) \to y \in k) \leftrightarrow \forall u \in ran ℤ_{\geq} y \in cls (J) (F [u])$
197		ralcom4	$⊢ \forall u \in ran ℤ_{\geq} \forall k (k = cls (J) (F [u]) \to y \in k) \leftrightarrow \forall k \forall u \in ran ℤ_{\geq} (k = cls (J) (F [u]) \to y \in k)$
198	196 197	bitr3i	$⊢ \forall u \in ran ℤ_{\geq} y \in cls (J) (F [u]) \leftrightarrow \forall k \forall u \in ran ℤ_{\geq} (k = cls (J) (F [u]) \to y \in k)$
199		vex	$⊢ y \in V$
200	199	elintab	$⊢ y \in ⋂ \{k \| \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])\} \leftrightarrow \forall k (\exists u \in ran ℤ_{\geq} k = cls (J) (F [u]) \to y \in k)$
201	192 198 200	3bitr4i	$⊢ \forall u \in ran ℤ_{\geq} y \in cls (J) (F [u]) \leftrightarrow y \in ⋂ \{k \| \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])\}$
202		eqid	$⊢ cls (J) (F [ℕ]) = cls (J) (F [ℕ])$
203		imaeq2	$⊢ u = ℕ \to F [u] = F [ℕ]$
204	203	fveq2d	$⊢ u = ℕ \to cls (J) (F [u]) = cls (J) (F [ℕ])$
205	204	rspceeqv	$⊢ (ℕ \in ran ℤ_{\geq} \land cls (J) (F [ℕ]) = cls (J) (F [ℕ])) \to \exists u \in ran ℤ_{\geq} cls (J) (F [ℕ]) = cls (J) (F [u])$
206	134 202 205	mp2an	$⊢ \exists u \in ran ℤ_{\geq} cls (J) (F [ℕ]) = cls (J) (F [u])$
207		fvex	$⊢ cls (J) (F [ℕ]) \in V$
208		eqeq1	$⊢ k = cls (J) (F [ℕ]) \to (k = cls (J) (F [u]) \leftrightarrow cls (J) (F [ℕ]) = cls (J) (F [u]))$
209	208	rexbidv	$⊢ k = cls (J) (F [ℕ]) \to (\exists u \in ran ℤ_{\geq} k = cls (J) (F [u]) \leftrightarrow \exists u \in ran ℤ_{\geq} cls (J) (F [ℕ]) = cls (J) (F [u]))$
210	207 209	elab	$⊢ cls (J) (F [ℕ]) \in \{k \| \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])\} \leftrightarrow \exists u \in ran ℤ_{\geq} cls (J) (F [ℕ]) = cls (J) (F [u])$
211	206 210	mpbir	$⊢ cls (J) (F [ℕ]) \in \{k \| \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])\}$
212		intss1	$⊢ cls (J) (F [ℕ]) \in \{k \| \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])\} \to ⋂ \{k \| \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])\} \subseteq cls (J) (F [ℕ])$
213	211 212	ax-mp	$⊢ ⋂ \{k \| \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])\} \subseteq cls (J) (F [ℕ])$
214		imassrn	$⊢ F [ℕ] \subseteq ran F$
215	214 14	sstrid	$⊢ φ \to F [ℕ] \subseteq ⋃ J$
216	16	clsss3	$⊢ (J \in Top \land F [ℕ] \subseteq ⋃ J) \to cls (J) (F [ℕ]) \subseteq ⋃ J$
217	9 215 216	syl2anc	$⊢ φ \to cls (J) (F [ℕ]) \subseteq ⋃ J$
218	217 13	sseqtrrd	$⊢ φ \to cls (J) (F [ℕ]) \subseteq X$
219	213 218	sstrid	$⊢ φ \to ⋂ \{k \| \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])\} \subseteq X$
220	219	sselda	$⊢ (φ \land y \in ⋂ \{k \| \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])\}) \to y \in X$
221	201 220	sylan2b	$⊢ (φ \land \forall u \in ran ℤ_{\geq} y \in cls (J) (F [u])) \to y \in X$
222		1zzd	$⊢ φ \to 1 \in ℤ$
223	130 7 222	iscau3	$⊢ φ \to (F \in Cau (D) \leftrightarrow (F \in (X ↑_{𝑝𝑚} ℂ) \land \forall y \in ℝ^{+} \exists m \in ℕ \forall k \in ℤ_{\geq m} (k \in dom F \land F (k) \in X \land \forall n \in ℤ_{\geq k} F (k) D F (n) < y)))$
224	4 223	mpbid	$⊢ φ \to (F \in (X ↑_{𝑝𝑚} ℂ) \land \forall y \in ℝ^{+} \exists m \in ℕ \forall k \in ℤ_{\geq m} (k \in dom F \land F (k) \in X \land \forall n \in ℤ_{\geq k} F (k) D F (n) < y))$
225	224	simprd	$⊢ φ \to \forall y \in ℝ^{+} \exists m \in ℕ \forall k \in ℤ_{\geq m} (k \in dom F \land F (k) \in X \land \forall n \in ℤ_{\geq k} F (k) D F (n) < y)$
226		simp3	$⊢ (k \in dom F \land F (k) \in X \land \forall n \in ℤ_{\geq k} F (k) D F (n) < y) \to \forall n \in ℤ_{\geq k} F (k) D F (n) < y$
227	226	ralimi	$⊢ \forall k \in ℤ_{\geq m} (k \in dom F \land F (k) \in X \land \forall n \in ℤ_{\geq k} F (k) D F (n) < y) \to \forall k \in ℤ_{\geq m} \forall n \in ℤ_{\geq k} F (k) D F (n) < y$
228	227	reximi	$⊢ \exists m \in ℕ \forall k \in ℤ_{\geq m} (k \in dom F \land F (k) \in X \land \forall n \in ℤ_{\geq k} F (k) D F (n) < y) \to \exists m \in ℕ \forall k \in ℤ_{\geq m} \forall n \in ℤ_{\geq k} F (k) D F (n) < y$
229	228	ralimi	$⊢ \forall y \in ℝ^{+} \exists m \in ℕ \forall k \in ℤ_{\geq m} (k \in dom F \land F (k) \in X \land \forall n \in ℤ_{\geq k} F (k) D F (n) < y) \to \forall y \in ℝ^{+} \exists m \in ℕ \forall k \in ℤ_{\geq m} \forall n \in ℤ_{\geq k} F (k) D F (n) < y$
230	225 229	syl	$⊢ φ \to \forall y \in ℝ^{+} \exists m \in ℕ \forall k \in ℤ_{\geq m} \forall n \in ℤ_{\geq k} F (k) D F (n) < y$
231	230	adantr	$⊢ (φ \land \forall u \in ran ℤ_{\geq} y \in cls (J) (F [u])) \to \forall y \in ℝ^{+} \exists m \in ℕ \forall k \in ℤ_{\geq m} \forall n \in ℤ_{\geq k} F (k) D F (n) < y$
232		rphalfcl	$⊢ r \in ℝ^{+} \to \frac{r}{2} \in ℝ^{+}$
233		breq2	$⊢ y = \frac{r}{2} \to (F (k) D F (n) < y \leftrightarrow F (k) D F (n) < \frac{r}{2})$
234	233	2ralbidv	$⊢ y = \frac{r}{2} \to (\forall k \in ℤ_{\geq m} \forall n \in ℤ_{\geq k} F (k) D F (n) < y \leftrightarrow \forall k \in ℤ_{\geq m} \forall n \in ℤ_{\geq k} F (k) D F (n) < \frac{r}{2})$
235	234	rexbidv	$⊢ y = \frac{r}{2} \to (\exists m \in ℕ \forall k \in ℤ_{\geq m} \forall n \in ℤ_{\geq k} F (k) D F (n) < y \leftrightarrow \exists m \in ℕ \forall k \in ℤ_{\geq m} \forall n \in ℤ_{\geq k} F (k) D F (n) < \frac{r}{2})$
236	235	rspccva	$⊢ (\forall y \in ℝ^{+} \exists m \in ℕ \forall k \in ℤ_{\geq m} \forall n \in ℤ_{\geq k} F (k) D F (n) < y \land \frac{r}{2} \in ℝ^{+}) \to \exists m \in ℕ \forall k \in ℤ_{\geq m} \forall n \in ℤ_{\geq k} F (k) D F (n) < \frac{r}{2}$
237	231 232 236	syl2an	$⊢ ((φ \land \forall u \in ran ℤ_{\geq} y \in cls (J) (F [u])) \land r \in ℝ^{+}) \to \exists m \in ℕ \forall k \in ℤ_{\geq m} \forall n \in ℤ_{\geq k} F (k) D F (n) < \frac{r}{2}$
238	5	ffund	$⊢ φ \to Fun F$
239	238	ad2antrr	$⊢ ((φ \land \forall u \in ran ℤ_{\geq} y \in cls (J) (F [u])) \land (r \in ℝ^{+} \land m \in ℕ)) \to Fun F$
240	9	ad2antrr	$⊢ ((φ \land \forall u \in ran ℤ_{\geq} y \in cls (J) (F [u])) \land (r \in ℝ^{+} \land m \in ℕ)) \to J \in Top$
241		imassrn	$⊢ F [ℤ_{\geq m}] \subseteq ran F$
242	241 14	sstrid	$⊢ φ \to F [ℤ_{\geq m}] \subseteq ⋃ J$
243	242	ad2antrr	$⊢ ((φ \land \forall u \in ran ℤ_{\geq} y \in cls (J) (F [u])) \land (r \in ℝ^{+} \land m \in ℕ)) \to F [ℤ_{\geq m}] \subseteq ⋃ J$
244		nnz	$⊢ m \in ℕ \to m \in ℤ$
245		fnfvelrn	$⊢ (ℤ_{\geq} Fn ℤ \land m \in ℤ) \to ℤ_{\geq m} \in ran ℤ_{\geq}$
246	58 244 245	sylancr	$⊢ m \in ℕ \to ℤ_{\geq m} \in ran ℤ_{\geq}$
247	246	ad2antll	$⊢ ((φ \land \forall u \in ran ℤ_{\geq} y \in cls (J) (F [u])) \land (r \in ℝ^{+} \land m \in ℕ)) \to ℤ_{\geq m} \in ran ℤ_{\geq}$
248		simplr	$⊢ ((φ \land \forall u \in ran ℤ_{\geq} y \in cls (J) (F [u])) \land (r \in ℝ^{+} \land m \in ℕ)) \to \forall u \in ran ℤ_{\geq} y \in cls (J) (F [u])$
249		imaeq2	$⊢ u = ℤ_{\geq m} \to F [u] = F [ℤ_{\geq m}]$
250	249	fveq2d	$⊢ u = ℤ_{\geq m} \to cls (J) (F [u]) = cls (J) (F [ℤ_{\geq m}])$
251	250	eleq2d	$⊢ u = ℤ_{\geq m} \to (y \in cls (J) (F [u]) \leftrightarrow y \in cls (J) (F [ℤ_{\geq m}]))$
252	251	rspcv	$⊢ ℤ_{\geq m} \in ran ℤ_{\geq} \to (\forall u \in ran ℤ_{\geq} y \in cls (J) (F [u]) \to y \in cls (J) (F [ℤ_{\geq m}]))$
253	247 248 252	sylc	$⊢ ((φ \land \forall u \in ran ℤ_{\geq} y \in cls (J) (F [u])) \land (r \in ℝ^{+} \land m \in ℕ)) \to y \in cls (J) (F [ℤ_{\geq m}])$
254	7	ad2antrr	$⊢ ((φ \land \forall u \in ran ℤ_{\geq} y \in cls (J) (F [u])) \land (r \in ℝ^{+} \land m \in ℕ)) \to D \in ∞Met (X)$
255	221	adantr	$⊢ ((φ \land \forall u \in ran ℤ_{\geq} y \in cls (J) (F [u])) \land (r \in ℝ^{+} \land m \in ℕ)) \to y \in X$
256	232	ad2antrl	$⊢ ((φ \land \forall u \in ran ℤ_{\geq} y \in cls (J) (F [u])) \land (r \in ℝ^{+} \land m \in ℕ)) \to \frac{r}{2} \in ℝ^{+}$
257	256	rpxrd	$⊢ ((φ \land \forall u \in ran ℤ_{\geq} y \in cls (J) (F [u])) \land (r \in ℝ^{+} \land m \in ℕ)) \to \frac{r}{2} \in ℝ^{*}$
258	1	blopn	$⊢ (D \in ∞Met (X) \land y \in X \land \frac{r}{2} \in ℝ^{*}) \to y ball (D) (\frac{r}{2}) \in J$
259	254 255 257 258	syl3anc	$⊢ ((φ \land \forall u \in ran ℤ_{\geq} y \in cls (J) (F [u])) \land (r \in ℝ^{+} \land m \in ℕ)) \to y ball (D) (\frac{r}{2}) \in J$
260		blcntr	$⊢ (D \in ∞Met (X) \land y \in X \land \frac{r}{2} \in ℝ^{+}) \to y \in (y ball (D) (\frac{r}{2}))$
261	254 255 256 260	syl3anc	$⊢ ((φ \land \forall u \in ran ℤ_{\geq} y \in cls (J) (F [u])) \land (r \in ℝ^{+} \land m \in ℕ)) \to y \in (y ball (D) (\frac{r}{2}))$
262	16	clsndisj	$⊢ ((J \in Top \land F [ℤ_{\geq m}] \subseteq ⋃ J \land y \in cls (J) (F [ℤ_{\geq m}])) \land (y ball (D) (\frac{r}{2}) \in J \land y \in (y ball (D) (\frac{r}{2})))) \to (y ball (D) (\frac{r}{2})) \cap F [ℤ_{\geq m}] \neq \emptyset$
263	240 243 253 259 261 262	syl32anc	$⊢ ((φ \land \forall u \in ran ℤ_{\geq} y \in cls (J) (F [u])) \land (r \in ℝ^{+} \land m \in ℕ)) \to (y ball (D) (\frac{r}{2})) \cap F [ℤ_{\geq m}] \neq \emptyset$
264		n0	$⊢ (y ball (D) (\frac{r}{2})) \cap F [ℤ_{\geq m}] \neq \emptyset \leftrightarrow \exists n n \in ((y ball (D) (\frac{r}{2})) \cap F [ℤ_{\geq m}])$
265		inss2	$⊢ (y ball (D) (\frac{r}{2})) \cap F [ℤ_{\geq m}] \subseteq F [ℤ_{\geq m}]$
266	265	sseli	$⊢ n \in ((y ball (D) (\frac{r}{2})) \cap F [ℤ_{\geq m}]) \to n \in F [ℤ_{\geq m}]$
267		fvelima	$⊢ (Fun F \land n \in F [ℤ_{\geq m}]) \to \exists k \in ℤ_{\geq m} F (k) = n$
268	266 267	sylan2	$⊢ (Fun F \land n \in ((y ball (D) (\frac{r}{2})) \cap F [ℤ_{\geq m}])) \to \exists k \in ℤ_{\geq m} F (k) = n$
269		inss1	$⊢ (y ball (D) (\frac{r}{2})) \cap F [ℤ_{\geq m}] \subseteq y ball (D) (\frac{r}{2})$
270	269	sseli	$⊢ n \in ((y ball (D) (\frac{r}{2})) \cap F [ℤ_{\geq m}]) \to n \in (y ball (D) (\frac{r}{2}))$
271	270	adantl	$⊢ (Fun F \land n \in ((y ball (D) (\frac{r}{2})) \cap F [ℤ_{\geq m}])) \to n \in (y ball (D) (\frac{r}{2}))$
272		eleq1a	$⊢ n \in (y ball (D) (\frac{r}{2})) \to (F (k) = n \to F (k) \in (y ball (D) (\frac{r}{2})))$
273	271 272	syl	$⊢ (Fun F \land n \in ((y ball (D) (\frac{r}{2})) \cap F [ℤ_{\geq m}])) \to (F (k) = n \to F (k) \in (y ball (D) (\frac{r}{2})))$
274	273	reximdv	$⊢ (Fun F \land n \in ((y ball (D) (\frac{r}{2})) \cap F [ℤ_{\geq m}])) \to (\exists k \in ℤ_{\geq m} F (k) = n \to \exists k \in ℤ_{\geq m} F (k) \in (y ball (D) (\frac{r}{2})))$
275	268 274	mpd	$⊢ (Fun F \land n \in ((y ball (D) (\frac{r}{2})) \cap F [ℤ_{\geq m}])) \to \exists k \in ℤ_{\geq m} F (k) \in (y ball (D) (\frac{r}{2}))$
276	275	ex	$⊢ Fun F \to (n \in ((y ball (D) (\frac{r}{2})) \cap F [ℤ_{\geq m}]) \to \exists k \in ℤ_{\geq m} F (k) \in (y ball (D) (\frac{r}{2})))$
277	276	exlimdv	$⊢ Fun F \to (\exists n n \in ((y ball (D) (\frac{r}{2})) \cap F [ℤ_{\geq m}]) \to \exists k \in ℤ_{\geq m} F (k) \in (y ball (D) (\frac{r}{2})))$
278	264 277	syl5bi	$⊢ Fun F \to ((y ball (D) (\frac{r}{2})) \cap F [ℤ_{\geq m}] \neq \emptyset \to \exists k \in ℤ_{\geq m} F (k) \in (y ball (D) (\frac{r}{2})))$
279	239 263 278	sylc	$⊢ ((φ \land \forall u \in ran ℤ_{\geq} y \in cls (J) (F [u])) \land (r \in ℝ^{+} \land m \in ℕ)) \to \exists k \in ℤ_{\geq m} F (k) \in (y ball (D) (\frac{r}{2}))$
280		r19.29	$⊢ (\forall k \in ℤ_{\geq m} \forall n \in ℤ_{\geq k} F (k) D F (n) < \frac{r}{2} \land \exists k \in ℤ_{\geq m} F (k) \in (y ball (D) (\frac{r}{2}))) \to \exists k \in ℤ_{\geq m} (\forall n \in ℤ_{\geq k} F (k) D F (n) < \frac{r}{2} \land F (k) \in (y ball (D) (\frac{r}{2})))$
281		uznnssnn	$⊢ m \in ℕ \to ℤ_{\geq m} \subseteq ℕ$
282	281	ad2antll	$⊢ ((φ \land y \in X) \land (r \in ℝ^{+} \land m \in ℕ)) \to ℤ_{\geq m} \subseteq ℕ$
283		simprlr	$⊢ (((φ \land y \in X) \land (r \in ℝ^{+} \land m \in ℕ)) \land ((k \in ℤ_{\geq m} \land F (k) \in (y ball (D) (\frac{r}{2}))) \land n \in ℤ_{\geq k})) \to F (k) \in (y ball (D) (\frac{r}{2}))$
284	7	ad3antrrr	$⊢ (((φ \land y \in X) \land (r \in ℝ^{+} \land m \in ℕ)) \land ((k \in ℤ_{\geq m} \land F (k) \in (y ball (D) (\frac{r}{2}))) \land n \in ℤ_{\geq k})) \to D \in ∞Met (X)$
285		simplrl	$⊢ (((φ \land y \in X) \land (r \in ℝ^{+} \land m \in ℕ)) \land ((k \in ℤ_{\geq m} \land F (k) \in (y ball (D) (\frac{r}{2}))) \land n \in ℤ_{\geq k})) \to r \in ℝ^{+}$
286	285 232	syl	$⊢ (((φ \land y \in X) \land (r \in ℝ^{+} \land m \in ℕ)) \land ((k \in ℤ_{\geq m} \land F (k) \in (y ball (D) (\frac{r}{2}))) \land n \in ℤ_{\geq k})) \to \frac{r}{2} \in ℝ^{+}$
287	286	rpxrd	$⊢ (((φ \land y \in X) \land (r \in ℝ^{+} \land m \in ℕ)) \land ((k \in ℤ_{\geq m} \land F (k) \in (y ball (D) (\frac{r}{2}))) \land n \in ℤ_{\geq k})) \to \frac{r}{2} \in ℝ^{*}$
288		simpllr	$⊢ (((φ \land y \in X) \land (r \in ℝ^{+} \land m \in ℕ)) \land ((k \in ℤ_{\geq m} \land F (k) \in (y ball (D) (\frac{r}{2}))) \land n \in ℤ_{\geq k})) \to y \in X$
289	5	ad3antrrr	$⊢ (((φ \land y \in X) \land (r \in ℝ^{+} \land m \in ℕ)) \land ((k \in ℤ_{\geq m} \land F (k) \in (y ball (D) (\frac{r}{2}))) \land n \in ℤ_{\geq k})) \to F : ℕ ⟶ X$
290		eluznn	$⊢ (m \in ℕ \land k \in ℤ_{\geq m}) \to k \in ℕ$
291	290	ad2ant2lr	$⊢ ((r \in ℝ^{+} \land m \in ℕ) \land (k \in ℤ_{\geq m} \land F (k) \in (y ball (D) (\frac{r}{2})))) \to k \in ℕ$
292	291	ad2ant2lr	$⊢ (((φ \land y \in X) \land (r \in ℝ^{+} \land m \in ℕ)) \land ((k \in ℤ_{\geq m} \land F (k) \in (y ball (D) (\frac{r}{2}))) \land n \in ℤ_{\geq k})) \to k \in ℕ$
293	289 292	ffvelrnd	$⊢ (((φ \land y \in X) \land (r \in ℝ^{+} \land m \in ℕ)) \land ((k \in ℤ_{\geq m} \land F (k) \in (y ball (D) (\frac{r}{2}))) \land n \in ℤ_{\geq k})) \to F (k) \in X$
294		elbl3	$⊢ ((D \in ∞Met (X) \land \frac{r}{2} \in ℝ^{*}) \land (y \in X \land F (k) \in X)) \to (F (k) \in (y ball (D) (\frac{r}{2})) \leftrightarrow F (k) D y < \frac{r}{2})$
295	284 287 288 293 294	syl22anc	$⊢ (((φ \land y \in X) \land (r \in ℝ^{+} \land m \in ℕ)) \land ((k \in ℤ_{\geq m} \land F (k) \in (y ball (D) (\frac{r}{2}))) \land n \in ℤ_{\geq k})) \to (F (k) \in (y ball (D) (\frac{r}{2})) \leftrightarrow F (k) D y < \frac{r}{2})$
296	283 295	mpbid	$⊢ (((φ \land y \in X) \land (r \in ℝ^{+} \land m \in ℕ)) \land ((k \in ℤ_{\geq m} \land F (k) \in (y ball (D) (\frac{r}{2}))) \land n \in ℤ_{\geq k})) \to F (k) D y < \frac{r}{2}$
297	2	ad3antrrr	$⊢ (((φ \land y \in X) \land (r \in ℝ^{+} \land m \in ℕ)) \land ((k \in ℤ_{\geq m} \land F (k) \in (y ball (D) (\frac{r}{2}))) \land n \in ℤ_{\geq k})) \to D \in Met (X)$
298		simprr	$⊢ (((φ \land y \in X) \land (r \in ℝ^{+} \land m \in ℕ)) \land ((k \in ℤ_{\geq m} \land F (k) \in (y ball (D) (\frac{r}{2}))) \land n \in ℤ_{\geq k})) \to n \in ℤ_{\geq k}$
299		eluznn	$⊢ (k \in ℕ \land n \in ℤ_{\geq k}) \to n \in ℕ$
300	292 298 299	syl2anc	$⊢ (((φ \land y \in X) \land (r \in ℝ^{+} \land m \in ℕ)) \land ((k \in ℤ_{\geq m} \land F (k) \in (y ball (D) (\frac{r}{2}))) \land n \in ℤ_{\geq k})) \to n \in ℕ$
301	289 300	ffvelrnd	$⊢ (((φ \land y \in X) \land (r \in ℝ^{+} \land m \in ℕ)) \land ((k \in ℤ_{\geq m} \land F (k) \in (y ball (D) (\frac{r}{2}))) \land n \in ℤ_{\geq k})) \to F (n) \in X$
302		metcl	$⊢ (D \in Met (X) \land F (k) \in X \land F (n) \in X) \to F (k) D F (n) \in ℝ$
303	297 293 301 302	syl3anc	$⊢ (((φ \land y \in X) \land (r \in ℝ^{+} \land m \in ℕ)) \land ((k \in ℤ_{\geq m} \land F (k) \in (y ball (D) (\frac{r}{2}))) \land n \in ℤ_{\geq k})) \to F (k) D F (n) \in ℝ$
304		metcl	$⊢ (D \in Met (X) \land F (k) \in X \land y \in X) \to F (k) D y \in ℝ$
305	297 293 288 304	syl3anc	$⊢ (((φ \land y \in X) \land (r \in ℝ^{+} \land m \in ℕ)) \land ((k \in ℤ_{\geq m} \land F (k) \in (y ball (D) (\frac{r}{2}))) \land n \in ℤ_{\geq k})) \to F (k) D y \in ℝ$
306	286	rpred	$⊢ (((φ \land y \in X) \land (r \in ℝ^{+} \land m \in ℕ)) \land ((k \in ℤ_{\geq m} \land F (k) \in (y ball (D) (\frac{r}{2}))) \land n \in ℤ_{\geq k})) \to \frac{r}{2} \in ℝ$
307		lt2add	$⊢ ((F (k) D F (n) \in ℝ \land F (k) D y \in ℝ) \land (\frac{r}{2} \in ℝ \land \frac{r}{2} \in ℝ)) \to ((F (k) D F (n) < \frac{r}{2} \land F (k) D y < \frac{r}{2}) \to (F (k) D F (n)) + (F (k) D y) < (\frac{r}{2}) + (\frac{r}{2}))$
308	303 305 306 306 307	syl22anc	$⊢ (((φ \land y \in X) \land (r \in ℝ^{+} \land m \in ℕ)) \land ((k \in ℤ_{\geq m} \land F (k) \in (y ball (D) (\frac{r}{2}))) \land n \in ℤ_{\geq k})) \to ((F (k) D F (n) < \frac{r}{2} \land F (k) D y < \frac{r}{2}) \to (F (k) D F (n)) + (F (k) D y) < (\frac{r}{2}) + (\frac{r}{2}))$
309	296 308	mpan2d	$⊢ (((φ \land y \in X) \land (r \in ℝ^{+} \land m \in ℕ)) \land ((k \in ℤ_{\geq m} \land F (k) \in (y ball (D) (\frac{r}{2}))) \land n \in ℤ_{\geq k})) \to (F (k) D F (n) < \frac{r}{2} \to (F (k) D F (n)) + (F (k) D y) < (\frac{r}{2}) + (\frac{r}{2}))$
310	285	rpcnd	$⊢ (((φ \land y \in X) \land (r \in ℝ^{+} \land m \in ℕ)) \land ((k \in ℤ_{\geq m} \land F (k) \in (y ball (D) (\frac{r}{2}))) \land n \in ℤ_{\geq k})) \to r \in ℂ$
311	310	2halvesd	$⊢ (((φ \land y \in X) \land (r \in ℝ^{+} \land m \in ℕ)) \land ((k \in ℤ_{\geq m} \land F (k) \in (y ball (D) (\frac{r}{2}))) \land n \in ℤ_{\geq k})) \to (\frac{r}{2}) + (\frac{r}{2}) = r$
312	311	breq2d	$⊢ (((φ \land y \in X) \land (r \in ℝ^{+} \land m \in ℕ)) \land ((k \in ℤ_{\geq m} \land F (k) \in (y ball (D) (\frac{r}{2}))) \land n \in ℤ_{\geq k})) \to ((F (k) D F (n)) + (F (k) D y) < (\frac{r}{2}) + (\frac{r}{2}) \leftrightarrow (F (k) D F (n)) + (F (k) D y) < r)$
313	309 312	sylibd	$⊢ (((φ \land y \in X) \land (r \in ℝ^{+} \land m \in ℕ)) \land ((k \in ℤ_{\geq m} \land F (k) \in (y ball (D) (\frac{r}{2}))) \land n \in ℤ_{\geq k})) \to (F (k) D F (n) < \frac{r}{2} \to (F (k) D F (n)) + (F (k) D y) < r)$
314		mettri2	$⊢ (D \in Met (X) \land (F (k) \in X \land F (n) \in X \land y \in X)) \to F (n) D y \leq (F (k) D F (n)) + (F (k) D y)$
315	297 293 301 288 314	syl13anc	$⊢ (((φ \land y \in X) \land (r \in ℝ^{+} \land m \in ℕ)) \land ((k \in ℤ_{\geq m} \land F (k) \in (y ball (D) (\frac{r}{2}))) \land n \in ℤ_{\geq k})) \to F (n) D y \leq (F (k) D F (n)) + (F (k) D y)$
316		metcl	$⊢ (D \in Met (X) \land F (n) \in X \land y \in X) \to F (n) D y \in ℝ$
317	297 301 288 316	syl3anc	$⊢ (((φ \land y \in X) \land (r \in ℝ^{+} \land m \in ℕ)) \land ((k \in ℤ_{\geq m} \land F (k) \in (y ball (D) (\frac{r}{2}))) \land n \in ℤ_{\geq k})) \to F (n) D y \in ℝ$
318	303 305	readdcld	$⊢ (((φ \land y \in X) \land (r \in ℝ^{+} \land m \in ℕ)) \land ((k \in ℤ_{\geq m} \land F (k) \in (y ball (D) (\frac{r}{2}))) \land n \in ℤ_{\geq k})) \to (F (k) D F (n)) + (F (k) D y) \in ℝ$
319	285	rpred	$⊢ (((φ \land y \in X) \land (r \in ℝ^{+} \land m \in ℕ)) \land ((k \in ℤ_{\geq m} \land F (k) \in (y ball (D) (\frac{r}{2}))) \land n \in ℤ_{\geq k})) \to r \in ℝ$
320		lelttr	$⊢ (F (n) D y \in ℝ \land (F (k) D F (n)) + (F (k) D y) \in ℝ \land r \in ℝ) \to ((F (n) D y \leq (F (k) D F (n)) + (F (k) D y) \land (F (k) D F (n)) + (F (k) D y) < r) \to F (n) D y < r)$
321	317 318 319 320	syl3anc	$⊢ (((φ \land y \in X) \land (r \in ℝ^{+} \land m \in ℕ)) \land ((k \in ℤ_{\geq m} \land F (k) \in (y ball (D) (\frac{r}{2}))) \land n \in ℤ_{\geq k})) \to ((F (n) D y \leq (F (k) D F (n)) + (F (k) D y) \land (F (k) D F (n)) + (F (k) D y) < r) \to F (n) D y < r)$
322	315 321	mpand	$⊢ (((φ \land y \in X) \land (r \in ℝ^{+} \land m \in ℕ)) \land ((k \in ℤ_{\geq m} \land F (k) \in (y ball (D) (\frac{r}{2}))) \land n \in ℤ_{\geq k})) \to ((F (k) D F (n)) + (F (k) D y) < r \to F (n) D y < r)$
323	313 322	syld	$⊢ (((φ \land y \in X) \land (r \in ℝ^{+} \land m \in ℕ)) \land ((k \in ℤ_{\geq m} \land F (k) \in (y ball (D) (\frac{r}{2}))) \land n \in ℤ_{\geq k})) \to (F (k) D F (n) < \frac{r}{2} \to F (n) D y < r)$
324	323	anassrs	$⊢ ((((φ \land y \in X) \land (r \in ℝ^{+} \land m \in ℕ)) \land (k \in ℤ_{\geq m} \land F (k) \in (y ball (D) (\frac{r}{2})))) \land n \in ℤ_{\geq k}) \to (F (k) D F (n) < \frac{r}{2} \to F (n) D y < r)$
325	324	ralimdva	$⊢ (((φ \land y \in X) \land (r \in ℝ^{+} \land m \in ℕ)) \land (k \in ℤ_{\geq m} \land F (k) \in (y ball (D) (\frac{r}{2})))) \to (\forall n \in ℤ_{\geq k} F (k) D F (n) < \frac{r}{2} \to \forall n \in ℤ_{\geq k} F (n) D y < r)$
326	325	expr	$⊢ (((φ \land y \in X) \land (r \in ℝ^{+} \land m \in ℕ)) \land k \in ℤ_{\geq m}) \to (F (k) \in (y ball (D) (\frac{r}{2})) \to (\forall n \in ℤ_{\geq k} F (k) D F (n) < \frac{r}{2} \to \forall n \in ℤ_{\geq k} F (n) D y < r))$
327	326	com23	$⊢ (((φ \land y \in X) \land (r \in ℝ^{+} \land m \in ℕ)) \land k \in ℤ_{\geq m}) \to (\forall n \in ℤ_{\geq k} F (k) D F (n) < \frac{r}{2} \to (F (k) \in (y ball (D) (\frac{r}{2})) \to \forall n \in ℤ_{\geq k} F (n) D y < r))$
328	327	impd	$⊢ (((φ \land y \in X) \land (r \in ℝ^{+} \land m \in ℕ)) \land k \in ℤ_{\geq m}) \to ((\forall n \in ℤ_{\geq k} F (k) D F (n) < \frac{r}{2} \land F (k) \in (y ball (D) (\frac{r}{2}))) \to \forall n \in ℤ_{\geq k} F (n) D y < r)$
329	328	reximdva	$⊢ ((φ \land y \in X) \land (r \in ℝ^{+} \land m \in ℕ)) \to (\exists k \in ℤ_{\geq m} (\forall n \in ℤ_{\geq k} F (k) D F (n) < \frac{r}{2} \land F (k) \in (y ball (D) (\frac{r}{2}))) \to \exists k \in ℤ_{\geq m} \forall n \in ℤ_{\geq k} F (n) D y < r)$
330		ssrexv	$⊢ ℤ_{\geq m} \subseteq ℕ \to (\exists k \in ℤ_{\geq m} \forall n \in ℤ_{\geq k} F (n) D y < r \to \exists k \in ℕ \forall n \in ℤ_{\geq k} F (n) D y < r)$
331	282 329 330	sylsyld	$⊢ ((φ \land y \in X) \land (r \in ℝ^{+} \land m \in ℕ)) \to (\exists k \in ℤ_{\geq m} (\forall n \in ℤ_{\geq k} F (k) D F (n) < \frac{r}{2} \land F (k) \in (y ball (D) (\frac{r}{2}))) \to \exists k \in ℕ \forall n \in ℤ_{\geq k} F (n) D y < r)$
332	221 331	syldanl	$⊢ ((φ \land \forall u \in ran ℤ_{\geq} y \in cls (J) (F [u])) \land (r \in ℝ^{+} \land m \in ℕ)) \to (\exists k \in ℤ_{\geq m} (\forall n \in ℤ_{\geq k} F (k) D F (n) < \frac{r}{2} \land F (k) \in (y ball (D) (\frac{r}{2}))) \to \exists k \in ℕ \forall n \in ℤ_{\geq k} F (n) D y < r)$
333	280 332	syl5	$⊢ ((φ \land \forall u \in ran ℤ_{\geq} y \in cls (J) (F [u])) \land (r \in ℝ^{+} \land m \in ℕ)) \to ((\forall k \in ℤ_{\geq m} \forall n \in ℤ_{\geq k} F (k) D F (n) < \frac{r}{2} \land \exists k \in ℤ_{\geq m} F (k) \in (y ball (D) (\frac{r}{2}))) \to \exists k \in ℕ \forall n \in ℤ_{\geq k} F (n) D y < r)$
334	279 333	mpan2d	$⊢ ((φ \land \forall u \in ran ℤ_{\geq} y \in cls (J) (F [u])) \land (r \in ℝ^{+} \land m \in ℕ)) \to (\forall k \in ℤ_{\geq m} \forall n \in ℤ_{\geq k} F (k) D F (n) < \frac{r}{2} \to \exists k \in ℕ \forall n \in ℤ_{\geq k} F (n) D y < r)$
335	334	anassrs	$⊢ (((φ \land \forall u \in ran ℤ_{\geq} y \in cls (J) (F [u])) \land r \in ℝ^{+}) \land m \in ℕ) \to (\forall k \in ℤ_{\geq m} \forall n \in ℤ_{\geq k} F (k) D F (n) < \frac{r}{2} \to \exists k \in ℕ \forall n \in ℤ_{\geq k} F (n) D y < r)$
336	335	rexlimdva	$⊢ ((φ \land \forall u \in ran ℤ_{\geq} y \in cls (J) (F [u])) \land r \in ℝ^{+}) \to (\exists m \in ℕ \forall k \in ℤ_{\geq m} \forall n \in ℤ_{\geq k} F (k) D F (n) < \frac{r}{2} \to \exists k \in ℕ \forall n \in ℤ_{\geq k} F (n) D y < r)$
337	237 336	mpd	$⊢ ((φ \land \forall u \in ran ℤ_{\geq} y \in cls (J) (F [u])) \land r \in ℝ^{+}) \to \exists k \in ℕ \forall n \in ℤ_{\geq k} F (n) D y < r$
338	337	ralrimiva	$⊢ (φ \land \forall u \in ran ℤ_{\geq} y \in cls (J) (F [u])) \to \forall r \in ℝ^{+} \exists k \in ℕ \forall n \in ℤ_{\geq k} F (n) D y < r$
339		eqidd	$⊢ (φ \land n \in ℕ) \to F (n) = F (n)$
340	1 7 130 222 339 5	lmmbrf	$⊢ φ \to (F \underset{t}{⇝} (J) y \leftrightarrow (y \in X \land \forall r \in ℝ^{+} \exists k \in ℕ \forall n \in ℤ_{\geq k} F (n) D y < r))$
341	340	adantr	$⊢ (φ \land \forall u \in ran ℤ_{\geq} y \in cls (J) (F [u])) \to (F \underset{t}{⇝} (J) y \leftrightarrow (y \in X \land \forall r \in ℝ^{+} \exists k \in ℕ \forall n \in ℤ_{\geq k} F (n) D y < r))$
342	221 338 341	mpbir2and	$⊢ (φ \land \forall u \in ran ℤ_{\geq} y \in cls (J) (F [u])) \to F \underset{t}{⇝} (J) y$
343	201 342	sylan2br	$⊢ (φ \land y \in ⋂ \{k \| \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])\}) \to F \underset{t}{⇝} (J) y$
344		releldm	$⊢ (Rel \underset{t}{⇝} (J) \land F \underset{t}{⇝} (J) y) \to F \in dom \underset{t}{⇝} (J)$
345	190 343 344	sylancr	$⊢ (φ \land y \in ⋂ \{k \| \exists u \in ran ℤ_{\geq} k = cls (J) (F [u])\}) \to F \in dom \underset{t}{⇝} (J)$
346	189 345	exlimddv	$⊢ φ \to F \in dom \underset{t}{⇝} (J)$

Metamath Proof Explorer

Theorem heibor1lem

Proof