heiborlem5

Description: Lemma for heibor . The function M is a set of point-and-radius pairs suitable for application to caubl . (Contributed by Jeff Madsen, 23-Jan-2014)

	Ref	Expression
Hypotheses	heibor.1	$⊢ J = MetOpen (D)$
	heibor.3	$⊢ K = \{u \| \neg \exists v \in (𝒫 U \cap Fin) u \subseteq ⋃ v\}$
	heibor.4	$⊢ G = \{⟨y, n⟩ \| (n \in ℕ_{0} \land y \in F (n) \land y B n \in K)\}$
	heibor.5	$⊢ B = (z \in X, m \in ℕ_{0} ⟼ z ball (D) (\frac{1}{2^{m}}))$
	heibor.6	$⊢ φ \to D \in CMet (X)$
	heibor.7	$⊢ φ \to F : ℕ_{0} ⟶ 𝒫 X \cap Fin$
	heibor.8	$⊢ φ \to \forall n \in ℕ_{0} X = ⋃_{y \in F (n)} (y B n)$
	heibor.9	$⊢ φ \to \forall x \in G (T (x) G (2^{nd} (x) + 1) \land B (x) \cap (T (x) B (2^{nd} (x) + 1)) \in K)$
	heibor.10	$⊢ φ \to C G 0$
	heibor.11	$⊢ S = seq 0 (T, (m \in ℕ_{0} ⟼ if (m = 0, C, m - 1)))$
	heibor.12	$⊢ M = (n \in ℕ ⟼ ⟨S (n), \frac{3}{2^{n}}⟩)$
Assertion	heiborlem5	$⊢ φ \to M : ℕ ⟶ X \times ℝ^{+}$

Proof

Step	Hyp	Ref	Expression
1		heibor.1	$⊢ J = MetOpen (D)$
2		heibor.3	$⊢ K = \{u \| \neg \exists v \in (𝒫 U \cap Fin) u \subseteq ⋃ v\}$
3		heibor.4	$⊢ G = \{⟨y, n⟩ \| (n \in ℕ_{0} \land y \in F (n) \land y B n \in K)\}$
4		heibor.5	$⊢ B = (z \in X, m \in ℕ_{0} ⟼ z ball (D) (\frac{1}{2^{m}}))$
5		heibor.6	$⊢ φ \to D \in CMet (X)$
6		heibor.7	$⊢ φ \to F : ℕ_{0} ⟶ 𝒫 X \cap Fin$
7		heibor.8	$⊢ φ \to \forall n \in ℕ_{0} X = ⋃_{y \in F (n)} (y B n)$
8		heibor.9	$⊢ φ \to \forall x \in G (T (x) G (2^{nd} (x) + 1) \land B (x) \cap (T (x) B (2^{nd} (x) + 1)) \in K)$
9		heibor.10	$⊢ φ \to C G 0$
10		heibor.11	$⊢ S = seq 0 (T, (m \in ℕ_{0} ⟼ if (m = 0, C, m - 1)))$
11		heibor.12	$⊢ M = (n \in ℕ ⟼ ⟨S (n), \frac{3}{2^{n}}⟩)$
12		nnnn0	$⊢ k \in ℕ \to k \in ℕ_{0}$
13		inss1	$⊢ 𝒫 X \cap Fin \subseteq 𝒫 X$
14	6	ffvelcdmda	$⊢ (φ \land k \in ℕ_{0}) \to F (k) \in (𝒫 X \cap Fin)$
15	13 14	sselid	$⊢ (φ \land k \in ℕ_{0}) \to F (k) \in 𝒫 X$
16	15	elpwid	$⊢ (φ \land k \in ℕ_{0}) \to F (k) \subseteq X$
17	1 2 3 4 5 6 7 8 9 10	heiborlem4	$⊢ (φ \land k \in ℕ_{0}) \to S (k) G k$
18		fvex	$⊢ S (k) \in V$
19		vex	$⊢ k \in V$
20	1 2 3 18 19	heiborlem2	$⊢ S (k) G k \leftrightarrow (k \in ℕ_{0} \land S (k) \in F (k) \land S (k) B k \in K)$
21	20	simp2bi	$⊢ S (k) G k \to S (k) \in F (k)$
22	17 21	syl	$⊢ (φ \land k \in ℕ_{0}) \to S (k) \in F (k)$
23	16 22	sseldd	$⊢ (φ \land k \in ℕ_{0}) \to S (k) \in X$
24	12 23	sylan2	$⊢ (φ \land k \in ℕ) \to S (k) \in X$
25	24	ralrimiva	$⊢ φ \to \forall k \in ℕ S (k) \in X$
26		fveq2	$⊢ k = n \to S (k) = S (n)$
27	26	eleq1d	$⊢ k = n \to (S (k) \in X \leftrightarrow S (n) \in X)$
28	27	cbvralvw	$⊢ \forall k \in ℕ S (k) \in X \leftrightarrow \forall n \in ℕ S (n) \in X$
29	25 28	sylib	$⊢ φ \to \forall n \in ℕ S (n) \in X$
30		3re	$⊢ 3 \in ℝ$
31		3pos	$⊢ 0 < 3$
32	30 31	elrpii	$⊢ 3 \in ℝ^{+}$
33		2nn	$⊢ 2 \in ℕ$
34		nnnn0	$⊢ n \in ℕ \to n \in ℕ_{0}$
35		nnexpcl	$⊢ (2 \in ℕ \land n \in ℕ_{0}) \to 2^{n} \in ℕ$
36	33 34 35	sylancr	$⊢ n \in ℕ \to 2^{n} \in ℕ$
37	36	nnrpd	$⊢ n \in ℕ \to 2^{n} \in ℝ^{+}$
38		rpdivcl	$⊢ (3 \in ℝ^{+} \land 2^{n} \in ℝ^{+}) \to \frac{3}{2^{n}} \in ℝ^{+}$
39	32 37 38	sylancr	$⊢ n \in ℕ \to \frac{3}{2^{n}} \in ℝ^{+}$
40		opelxpi	$⊢ (S (n) \in X \land \frac{3}{2^{n}} \in ℝ^{+}) \to ⟨S (n), \frac{3}{2^{n}}⟩ \in (X \times ℝ^{+})$
41	40	expcom	$⊢ \frac{3}{2^{n}} \in ℝ^{+} \to (S (n) \in X \to ⟨S (n), \frac{3}{2^{n}}⟩ \in (X \times ℝ^{+}))$
42	39 41	syl	$⊢ n \in ℕ \to (S (n) \in X \to ⟨S (n), \frac{3}{2^{n}}⟩ \in (X \times ℝ^{+}))$
43	42	ralimia	$⊢ \forall n \in ℕ S (n) \in X \to \forall n \in ℕ ⟨S (n), \frac{3}{2^{n}}⟩ \in (X \times ℝ^{+})$
44	29 43	syl	$⊢ φ \to \forall n \in ℕ ⟨S (n), \frac{3}{2^{n}}⟩ \in (X \times ℝ^{+})$
45	11	fmpt	$⊢ \forall n \in ℕ ⟨S (n), \frac{3}{2^{n}}⟩ \in (X \times ℝ^{+}) \leftrightarrow M : ℕ ⟶ X \times ℝ^{+}$
46	44 45	sylib	$⊢ φ \to M : ℕ ⟶ X \times ℝ^{+}$

Metamath Proof Explorer

Theorem heiborlem5

Proof