heiborlem9

Description: Lemma for heibor . Discharge the hypotheses of heiborlem8 by applying caubl to get a convergent point and adding the open cover assumption. (Contributed by Jeff Madsen, 20-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}}⟩)$
	heibor.13	$⊢ φ \to U \subseteq J$
	heiborlem9.14	$⊢ φ \to ⋃ U = X$
Assertion	heiborlem9	$⊢ φ \to ψ$

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		heibor.13	$⊢ φ \to U \subseteq J$
13		heiborlem9.14	$⊢ φ \to ⋃ U = X$
14		cmetmet	$⊢ D \in CMet (X) \to D \in Met (X)$
15		metxmet	$⊢ D \in Met (X) \to D \in ∞Met (X)$
16	5 14 15	3syl	$⊢ φ \to D \in ∞Met (X)$
17	1	mopntopon	$⊢ D \in ∞Met (X) \to J \in TopOn (X)$
18	16 17	syl	$⊢ φ \to J \in TopOn (X)$
19	1 2 3 4 5 6 7 8 9 10 11	heiborlem5	$⊢ φ \to M : ℕ ⟶ X \times ℝ^{+}$
20	1 2 3 4 5 6 7 8 9 10 11	heiborlem6	$⊢ φ \to \forall k \in ℕ ball (D) (M (k + 1)) \subseteq ball (D) (M (k))$
21	1 2 3 4 5 6 7 8 9 10 11	heiborlem7	$⊢ \forall r \in ℝ^{+} \exists k \in ℕ 2^{nd} (M (k)) < r$
22	21	a1i	$⊢ φ \to \forall r \in ℝ^{+} \exists k \in ℕ 2^{nd} (M (k)) < r$
23	16 19 20 22	caubl	$⊢ φ \to 1^{st} \circ M \in Cau (D)$
24	1	cmetcau	$⊢ (D \in CMet (X) \land 1^{st} \circ M \in Cau (D)) \to 1^{st} \circ M \in dom \underset{t}{⇝} (J)$
25	5 23 24	syl2anc	$⊢ φ \to 1^{st} \circ M \in dom \underset{t}{⇝} (J)$
26	1	methaus	$⊢ D \in ∞Met (X) \to J \in Haus$
27	16 26	syl	$⊢ φ \to J \in Haus$
28		lmfun	$⊢ J \in Haus \to Fun \underset{t}{⇝} (J)$
29		funfvbrb	$⊢ Fun \underset{t}{⇝} (J) \to (1^{st} \circ M \in dom \underset{t}{⇝} (J) \leftrightarrow (1^{st} \circ M) \underset{t}{⇝} (J) \underset{t}{⇝} (J) (1^{st} \circ M))$
30	27 28 29	3syl	$⊢ φ \to (1^{st} \circ M \in dom \underset{t}{⇝} (J) \leftrightarrow (1^{st} \circ M) \underset{t}{⇝} (J) \underset{t}{⇝} (J) (1^{st} \circ M))$
31	25 30	mpbid	$⊢ φ \to (1^{st} \circ M) \underset{t}{⇝} (J) \underset{t}{⇝} (J) (1^{st} \circ M)$
32		lmcl	$⊢ (J \in TopOn (X) \land (1^{st} \circ M) \underset{t}{⇝} (J) \underset{t}{⇝} (J) (1^{st} \circ M)) \to \underset{t}{⇝} (J) (1^{st} \circ M) \in X$
33	18 31 32	syl2anc	$⊢ φ \to \underset{t}{⇝} (J) (1^{st} \circ M) \in X$
34	33 13	eleqtrrd	$⊢ φ \to \underset{t}{⇝} (J) (1^{st} \circ M) \in ⋃ U$
35		eluni2	$⊢ \underset{t}{⇝} (J) (1^{st} \circ M) \in ⋃ U \leftrightarrow \exists t \in U \underset{t}{⇝} (J) (1^{st} \circ M) \in t$
36	34 35	sylib	$⊢ φ \to \exists t \in U \underset{t}{⇝} (J) (1^{st} \circ M) \in t$
37	5	adantr	$⊢ (φ \land (t \in U \land \underset{t}{⇝} (J) (1^{st} \circ M) \in t)) \to D \in CMet (X)$
38	6	adantr	$⊢ (φ \land (t \in U \land \underset{t}{⇝} (J) (1^{st} \circ M) \in t)) \to F : ℕ_{0} ⟶ 𝒫 X \cap Fin$
39	7	adantr	$⊢ (φ \land (t \in U \land \underset{t}{⇝} (J) (1^{st} \circ M) \in t)) \to \forall n \in ℕ_{0} X = ⋃_{y \in F (n)} (y B n)$
40	8	adantr	$⊢ (φ \land (t \in U \land \underset{t}{⇝} (J) (1^{st} \circ M) \in t)) \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)$
41	9	adantr	$⊢ (φ \land (t \in U \land \underset{t}{⇝} (J) (1^{st} \circ M) \in t)) \to C G 0$
42	12	adantr	$⊢ (φ \land (t \in U \land \underset{t}{⇝} (J) (1^{st} \circ M) \in t)) \to U \subseteq J$
43		fvex	$⊢ \underset{t}{⇝} (J) (1^{st} \circ M) \in V$
44		simprr	$⊢ (φ \land (t \in U \land \underset{t}{⇝} (J) (1^{st} \circ M) \in t)) \to \underset{t}{⇝} (J) (1^{st} \circ M) \in t$
45		simprl	$⊢ (φ \land (t \in U \land \underset{t}{⇝} (J) (1^{st} \circ M) \in t)) \to t \in U$
46	31	adantr	$⊢ (φ \land (t \in U \land \underset{t}{⇝} (J) (1^{st} \circ M) \in t)) \to (1^{st} \circ M) \underset{t}{⇝} (J) \underset{t}{⇝} (J) (1^{st} \circ M)$
47	1 2 3 4 37 38 39 40 41 10 11 42 43 44 45 46	heiborlem8	$⊢ (φ \land (t \in U \land \underset{t}{⇝} (J) (1^{st} \circ M) \in t)) \to ψ$
48	36 47	rexlimddv	$⊢ φ \to ψ$

Metamath Proof Explorer

Theorem heiborlem9

Proof