heiborlem8

Description: Lemma for heibor . The previous lemmas establish that the sequence M is Cauchy, so using completeness we now consider the convergent point Y . By assumption, U is an open cover, so Y is an element of some Z e. U , and some ball centered at Y is contained in Z . But the sequence contains arbitrarily small balls close to Y , so some element ball ( Mn ) of the sequence is contained in Z . And finally we arrive at a contradiction, because { Z } is a finite subcover of U that covers ball ( Mn ) , yet ball ( Mn ) e. K . For convenience, we write this contradiction as ph -> ps where ph is all the accumulated hypotheses and ps is anything at all. (Contributed by Jeff Madsen, 22-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$
	heibor.14	$⊢ Y \in V$
	heibor.15	$⊢ φ \to Y \in Z$
	heibor.16	$⊢ φ \to Z \in U$
	heibor.17	$⊢ φ \to (1^{st} \circ M) \underset{t}{⇝} (J) Y$
Assertion	heiborlem8	$⊢ φ \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		heibor.14	$⊢ Y \in V$
14		heibor.15	$⊢ φ \to Y \in Z$
15		heibor.16	$⊢ φ \to Z \in U$
16		heibor.17	$⊢ φ \to (1^{st} \circ M) \underset{t}{⇝} (J) Y$
17		cmetmet	$⊢ D \in CMet (X) \to D \in Met (X)$
18		metxmet	$⊢ D \in Met (X) \to D \in ∞Met (X)$
19	5 17 18	3syl	$⊢ φ \to D \in ∞Met (X)$
20	12 15	sseldd	$⊢ φ \to Z \in J$
21	1	mopni2	$⊢ (D \in ∞Met (X) \land Z \in J \land Y \in Z) \to \exists x \in ℝ^{+} Y ball (D) x \subseteq Z$
22	19 20 14 21	syl3anc	$⊢ φ \to \exists x \in ℝ^{+} Y ball (D) x \subseteq Z$
23		rphalfcl	$⊢ x \in ℝ^{+} \to \frac{x}{2} \in ℝ^{+}$
24		breq2	$⊢ r = \frac{x}{2} \to (2^{nd} (M (k)) < r \leftrightarrow 2^{nd} (M (k)) < \frac{x}{2})$
25	24	rexbidv	$⊢ r = \frac{x}{2} \to (\exists k \in ℕ 2^{nd} (M (k)) < r \leftrightarrow \exists k \in ℕ 2^{nd} (M (k)) < \frac{x}{2})$
26	1 2 3 4 5 6 7 8 9 10 11	heiborlem7	$⊢ \forall r \in ℝ^{+} \exists k \in ℕ 2^{nd} (M (k)) < r$
27	25 26	vtoclri	$⊢ \frac{x}{2} \in ℝ^{+} \to \exists k \in ℕ 2^{nd} (M (k)) < \frac{x}{2}$
28	23 27	syl	$⊢ x \in ℝ^{+} \to \exists k \in ℕ 2^{nd} (M (k)) < \frac{x}{2}$
29	28	adantl	$⊢ (φ \land x \in ℝ^{+}) \to \exists k \in ℕ 2^{nd} (M (k)) < \frac{x}{2}$
30		nnnn0	$⊢ k \in ℕ \to k \in ℕ_{0}$
31	1 2 3 4 5 6 7 8 9 10	heiborlem4	$⊢ (φ \land k \in ℕ_{0}) \to S (k) G k$
32		fvex	$⊢ S (k) \in V$
33		vex	$⊢ k \in V$
34	1 2 3 32 33	heiborlem2	$⊢ S (k) G k \leftrightarrow (k \in ℕ_{0} \land S (k) \in F (k) \land S (k) B k \in K)$
35	34	simp3bi	$⊢ S (k) G k \to S (k) B k \in K$
36	31 35	syl	$⊢ (φ \land k \in ℕ_{0}) \to S (k) B k \in K$
37	30 36	sylan2	$⊢ (φ \land k \in ℕ) \to S (k) B k \in K$
38	37	ad2ant2r	$⊢ ((φ \land x \in ℝ^{+}) \land (k \in ℕ \land 2^{nd} (M (k)) < \frac{x}{2})) \to S (k) B k \in K$
39	19	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land (k \in ℕ \land 2^{nd} (M (k)) < \frac{x}{2})) \to D \in ∞Met (X)$
40	1 2 3 4 5 6 7 8 9 10 11	heiborlem5	$⊢ φ \to M : ℕ ⟶ X \times ℝ^{+}$
41	40	ffvelrnda	$⊢ (φ \land k \in ℕ) \to M (k) \in (X \times ℝ^{+})$
42	41	ad2ant2r	$⊢ ((φ \land x \in ℝ^{+}) \land (k \in ℕ \land 2^{nd} (M (k)) < \frac{x}{2})) \to M (k) \in (X \times ℝ^{+})$
43		xp1st	$⊢ M (k) \in (X \times ℝ^{+}) \to 1^{st} (M (k)) \in X$
44	42 43	syl	$⊢ ((φ \land x \in ℝ^{+}) \land (k \in ℕ \land 2^{nd} (M (k)) < \frac{x}{2})) \to 1^{st} (M (k)) \in X$
45		2nn	$⊢ 2 \in ℕ$
46		nnexpcl	$⊢ (2 \in ℕ \land k \in ℕ_{0}) \to 2^{k} \in ℕ$
47	45 30 46	sylancr	$⊢ k \in ℕ \to 2^{k} \in ℕ$
48	47	nnrpd	$⊢ k \in ℕ \to 2^{k} \in ℝ^{+}$
49	48	rpreccld	$⊢ k \in ℕ \to \frac{1}{2^{k}} \in ℝ^{+}$
50	49	ad2antrl	$⊢ ((φ \land x \in ℝ^{+}) \land (k \in ℕ \land 2^{nd} (M (k)) < \frac{x}{2})) \to \frac{1}{2^{k}} \in ℝ^{+}$
51	50	rpxrd	$⊢ ((φ \land x \in ℝ^{+}) \land (k \in ℕ \land 2^{nd} (M (k)) < \frac{x}{2})) \to \frac{1}{2^{k}} \in ℝ^{*}$
52		xp2nd	$⊢ M (k) \in (X \times ℝ^{+}) \to 2^{nd} (M (k)) \in ℝ^{+}$
53	42 52	syl	$⊢ ((φ \land x \in ℝ^{+}) \land (k \in ℕ \land 2^{nd} (M (k)) < \frac{x}{2})) \to 2^{nd} (M (k)) \in ℝ^{+}$
54	53	rpxrd	$⊢ ((φ \land x \in ℝ^{+}) \land (k \in ℕ \land 2^{nd} (M (k)) < \frac{x}{2})) \to 2^{nd} (M (k)) \in ℝ^{*}$
55		1le3	$⊢ 1 \leq 3$
56		elrp	$⊢ 2^{k} \in ℝ^{+} \leftrightarrow (2^{k} \in ℝ \land 0 < 2^{k})$
57		1re	$⊢ 1 \in ℝ$
58		3re	$⊢ 3 \in ℝ$
59		lediv1	$⊢ (1 \in ℝ \land 3 \in ℝ \land (2^{k} \in ℝ \land 0 < 2^{k})) \to (1 \leq 3 \leftrightarrow \frac{1}{2^{k}} \leq \frac{3}{2^{k}})$
60	57 58 59	mp3an12	$⊢ (2^{k} \in ℝ \land 0 < 2^{k}) \to (1 \leq 3 \leftrightarrow \frac{1}{2^{k}} \leq \frac{3}{2^{k}})$
61	56 60	sylbi	$⊢ 2^{k} \in ℝ^{+} \to (1 \leq 3 \leftrightarrow \frac{1}{2^{k}} \leq \frac{3}{2^{k}})$
62	55 61	mpbii	$⊢ 2^{k} \in ℝ^{+} \to \frac{1}{2^{k}} \leq \frac{3}{2^{k}}$
63	48 62	syl	$⊢ k \in ℕ \to \frac{1}{2^{k}} \leq \frac{3}{2^{k}}$
64	63	ad2antrl	$⊢ ((φ \land x \in ℝ^{+}) \land (k \in ℕ \land 2^{nd} (M (k)) < \frac{x}{2})) \to \frac{1}{2^{k}} \leq \frac{3}{2^{k}}$
65		fveq2	$⊢ n = k \to S (n) = S (k)$
66		oveq2	$⊢ n = k \to 2^{n} = 2^{k}$
67	66	oveq2d	$⊢ n = k \to \frac{3}{2^{n}} = \frac{3}{2^{k}}$
68	65 67	opeq12d	$⊢ n = k \to ⟨S (n), \frac{3}{2^{n}}⟩ = ⟨S (k), \frac{3}{2^{k}}⟩$
69		opex	$⊢ ⟨S (k), \frac{3}{2^{k}}⟩ \in V$
70	68 11 69	fvmpt	$⊢ k \in ℕ \to M (k) = ⟨S (k), \frac{3}{2^{k}}⟩$
71	70	fveq2d	$⊢ k \in ℕ \to 2^{nd} (M (k)) = 2^{nd} (⟨S (k), \frac{3}{2^{k}}⟩)$
72		ovex	$⊢ \frac{3}{2^{k}} \in V$
73	32 72	op2nd	$⊢ 2^{nd} (⟨S (k), \frac{3}{2^{k}}⟩) = \frac{3}{2^{k}}$
74	71 73	eqtrdi	$⊢ k \in ℕ \to 2^{nd} (M (k)) = \frac{3}{2^{k}}$
75	74	ad2antrl	$⊢ ((φ \land x \in ℝ^{+}) \land (k \in ℕ \land 2^{nd} (M (k)) < \frac{x}{2})) \to 2^{nd} (M (k)) = \frac{3}{2^{k}}$
76	64 75	breqtrrd	$⊢ ((φ \land x \in ℝ^{+}) \land (k \in ℕ \land 2^{nd} (M (k)) < \frac{x}{2})) \to \frac{1}{2^{k}} \leq 2^{nd} (M (k))$
77		ssbl	$⊢ ((D \in ∞Met (X) \land 1^{st} (M (k)) \in X) \land (\frac{1}{2^{k}} \in ℝ^{} \land 2^{nd} (M (k)) \in ℝ^{}) \land \frac{1}{2^{k}} \leq 2^{nd} (M (k))) \to 1^{st} (M (k)) ball (D) (\frac{1}{2^{k}}) \subseteq 1^{st} (M (k)) ball (D) 2^{nd} (M (k))$
78	39 44 51 54 76 77	syl221anc	$⊢ ((φ \land x \in ℝ^{+}) \land (k \in ℕ \land 2^{nd} (M (k)) < \frac{x}{2})) \to 1^{st} (M (k)) ball (D) (\frac{1}{2^{k}}) \subseteq 1^{st} (M (k)) ball (D) 2^{nd} (M (k))$
79	30	ad2antrl	$⊢ ((φ \land x \in ℝ^{+}) \land (k \in ℕ \land 2^{nd} (M (k)) < \frac{x}{2})) \to k \in ℕ_{0}$
80		oveq1	$⊢ z = 1^{st} (M (k)) \to z ball (D) (\frac{1}{2^{m}}) = 1^{st} (M (k)) ball (D) (\frac{1}{2^{m}})$
81		oveq2	$⊢ m = k \to 2^{m} = 2^{k}$
82	81	oveq2d	$⊢ m = k \to \frac{1}{2^{m}} = \frac{1}{2^{k}}$
83	82	oveq2d	$⊢ m = k \to 1^{st} (M (k)) ball (D) (\frac{1}{2^{m}}) = 1^{st} (M (k)) ball (D) (\frac{1}{2^{k}})$
84		ovex	$⊢ 1^{st} (M (k)) ball (D) (\frac{1}{2^{k}}) \in V$
85	80 83 4 84	ovmpo	$⊢ (1^{st} (M (k)) \in X \land k \in ℕ_{0}) \to 1^{st} (M (k)) B k = 1^{st} (M (k)) ball (D) (\frac{1}{2^{k}})$
86	44 79 85	syl2anc	$⊢ ((φ \land x \in ℝ^{+}) \land (k \in ℕ \land 2^{nd} (M (k)) < \frac{x}{2})) \to 1^{st} (M (k)) B k = 1^{st} (M (k)) ball (D) (\frac{1}{2^{k}})$
87	70	fveq2d	$⊢ k \in ℕ \to 1^{st} (M (k)) = 1^{st} (⟨S (k), \frac{3}{2^{k}}⟩)$
88	32 72	op1st	$⊢ 1^{st} (⟨S (k), \frac{3}{2^{k}}⟩) = S (k)$
89	87 88	eqtrdi	$⊢ k \in ℕ \to 1^{st} (M (k)) = S (k)$
90	89	ad2antrl	$⊢ ((φ \land x \in ℝ^{+}) \land (k \in ℕ \land 2^{nd} (M (k)) < \frac{x}{2})) \to 1^{st} (M (k)) = S (k)$
91	90	oveq1d	$⊢ ((φ \land x \in ℝ^{+}) \land (k \in ℕ \land 2^{nd} (M (k)) < \frac{x}{2})) \to 1^{st} (M (k)) B k = S (k) B k$
92	86 91	eqtr3d	$⊢ ((φ \land x \in ℝ^{+}) \land (k \in ℕ \land 2^{nd} (M (k)) < \frac{x}{2})) \to 1^{st} (M (k)) ball (D) (\frac{1}{2^{k}}) = S (k) B k$
93		df-ov	$⊢ 1^{st} (M (k)) ball (D) 2^{nd} (M (k)) = ball (D) (⟨1^{st} (M (k)), 2^{nd} (M (k))⟩)$
94		1st2nd2	$⊢ M (k) \in (X \times ℝ^{+}) \to M (k) = ⟨1^{st} (M (k)), 2^{nd} (M (k))⟩$
95	42 94	syl	$⊢ ((φ \land x \in ℝ^{+}) \land (k \in ℕ \land 2^{nd} (M (k)) < \frac{x}{2})) \to M (k) = ⟨1^{st} (M (k)), 2^{nd} (M (k))⟩$
96	95	fveq2d	$⊢ ((φ \land x \in ℝ^{+}) \land (k \in ℕ \land 2^{nd} (M (k)) < \frac{x}{2})) \to ball (D) (M (k)) = ball (D) (⟨1^{st} (M (k)), 2^{nd} (M (k))⟩)$
97	93 96	eqtr4id	$⊢ ((φ \land x \in ℝ^{+}) \land (k \in ℕ \land 2^{nd} (M (k)) < \frac{x}{2})) \to 1^{st} (M (k)) ball (D) 2^{nd} (M (k)) = ball (D) (M (k))$
98	78 92 97	3sstr3d	$⊢ ((φ \land x \in ℝ^{+}) \land (k \in ℕ \land 2^{nd} (M (k)) < \frac{x}{2})) \to S (k) B k \subseteq ball (D) (M (k))$
99	1	mopntop	$⊢ D \in ∞Met (X) \to J \in Top$
100	39 99	syl	$⊢ ((φ \land x \in ℝ^{+}) \land (k \in ℕ \land 2^{nd} (M (k)) < \frac{x}{2})) \to J \in Top$
101		blssm	$⊢ (D \in ∞Met (X) \land 1^{st} (M (k)) \in X \land 2^{nd} (M (k)) \in ℝ^{*}) \to 1^{st} (M (k)) ball (D) 2^{nd} (M (k)) \subseteq X$
102	39 44 54 101	syl3anc	$⊢ ((φ \land x \in ℝ^{+}) \land (k \in ℕ \land 2^{nd} (M (k)) < \frac{x}{2})) \to 1^{st} (M (k)) ball (D) 2^{nd} (M (k)) \subseteq X$
103	1	mopnuni	$⊢ D \in ∞Met (X) \to X = ⋃ J$
104	39 103	syl	$⊢ ((φ \land x \in ℝ^{+}) \land (k \in ℕ \land 2^{nd} (M (k)) < \frac{x}{2})) \to X = ⋃ J$
105	102 97 104	3sstr3d	$⊢ ((φ \land x \in ℝ^{+}) \land (k \in ℕ \land 2^{nd} (M (k)) < \frac{x}{2})) \to ball (D) (M (k)) \subseteq ⋃ J$
106		eqid	$⊢ ⋃ J = ⋃ J$
107	106	sscls	$⊢ (J \in Top \land ball (D) (M (k)) \subseteq ⋃ J) \to ball (D) (M (k)) \subseteq cls (J) (ball (D) (M (k)))$
108	100 105 107	syl2anc	$⊢ ((φ \land x \in ℝ^{+}) \land (k \in ℕ \land 2^{nd} (M (k)) < \frac{x}{2})) \to ball (D) (M (k)) \subseteq cls (J) (ball (D) (M (k)))$
109	97	fveq2d	$⊢ ((φ \land x \in ℝ^{+}) \land (k \in ℕ \land 2^{nd} (M (k)) < \frac{x}{2})) \to cls (J) (1^{st} (M (k)) ball (D) 2^{nd} (M (k))) = cls (J) (ball (D) (M (k)))$
110	23	ad2antlr	$⊢ ((φ \land x \in ℝ^{+}) \land (k \in ℕ \land 2^{nd} (M (k)) < \frac{x}{2})) \to \frac{x}{2} \in ℝ^{+}$
111	110	rpxrd	$⊢ ((φ \land x \in ℝ^{+}) \land (k \in ℕ \land 2^{nd} (M (k)) < \frac{x}{2})) \to \frac{x}{2} \in ℝ^{*}$
112		simprr	$⊢ ((φ \land x \in ℝ^{+}) \land (k \in ℕ \land 2^{nd} (M (k)) < \frac{x}{2})) \to 2^{nd} (M (k)) < \frac{x}{2}$
113	1	blsscls	$⊢ ((D \in ∞Met (X) \land 1^{st} (M (k)) \in X) \land (2^{nd} (M (k)) \in ℝ^{} \land \frac{x}{2} \in ℝ^{} \land 2^{nd} (M (k)) < \frac{x}{2})) \to cls (J) (1^{st} (M (k)) ball (D) 2^{nd} (M (k))) \subseteq 1^{st} (M (k)) ball (D) (\frac{x}{2})$
114	39 44 54 111 112 113	syl23anc	$⊢ ((φ \land x \in ℝ^{+}) \land (k \in ℕ \land 2^{nd} (M (k)) < \frac{x}{2})) \to cls (J) (1^{st} (M (k)) ball (D) 2^{nd} (M (k))) \subseteq 1^{st} (M (k)) ball (D) (\frac{x}{2})$
115	109 114	eqsstrrd	$⊢ ((φ \land x \in ℝ^{+}) \land (k \in ℕ \land 2^{nd} (M (k)) < \frac{x}{2})) \to cls (J) (ball (D) (M (k))) \subseteq 1^{st} (M (k)) ball (D) (\frac{x}{2})$
116		rpre	$⊢ x \in ℝ^{+} \to x \in ℝ$
117	116	ad2antlr	$⊢ ((φ \land x \in ℝ^{+}) \land (k \in ℕ \land 2^{nd} (M (k)) < \frac{x}{2})) \to x \in ℝ$
118	1 2 3 4 5 6 7 8 9 10 11	heiborlem6	$⊢ φ \to \forall t \in ℕ ball (D) (M (t + 1)) \subseteq ball (D) (M (t))$
119	19 40 118 1	caublcls	$⊢ (φ \land (1^{st} \circ M) \underset{t}{⇝} (J) Y \land k \in ℕ) \to Y \in cls (J) (ball (D) (M (k)))$
120	119	3expia	$⊢ (φ \land (1^{st} \circ M) \underset{t}{⇝} (J) Y) \to (k \in ℕ \to Y \in cls (J) (ball (D) (M (k))))$
121	16 120	mpdan	$⊢ φ \to (k \in ℕ \to Y \in cls (J) (ball (D) (M (k))))$
122	121	imp	$⊢ (φ \land k \in ℕ) \to Y \in cls (J) (ball (D) (M (k)))$
123	122	ad2ant2r	$⊢ ((φ \land x \in ℝ^{+}) \land (k \in ℕ \land 2^{nd} (M (k)) < \frac{x}{2})) \to Y \in cls (J) (ball (D) (M (k)))$
124	115 123	sseldd	$⊢ ((φ \land x \in ℝ^{+}) \land (k \in ℕ \land 2^{nd} (M (k)) < \frac{x}{2})) \to Y \in (1^{st} (M (k)) ball (D) (\frac{x}{2}))$
125		blhalf	$⊢ ((D \in ∞Met (X) \land 1^{st} (M (k)) \in X) \land (x \in ℝ \land Y \in (1^{st} (M (k)) ball (D) (\frac{x}{2})))) \to 1^{st} (M (k)) ball (D) (\frac{x}{2}) \subseteq Y ball (D) x$
126	39 44 117 124 125	syl22anc	$⊢ ((φ \land x \in ℝ^{+}) \land (k \in ℕ \land 2^{nd} (M (k)) < \frac{x}{2})) \to 1^{st} (M (k)) ball (D) (\frac{x}{2}) \subseteq Y ball (D) x$
127	115 126	sstrd	$⊢ ((φ \land x \in ℝ^{+}) \land (k \in ℕ \land 2^{nd} (M (k)) < \frac{x}{2})) \to cls (J) (ball (D) (M (k))) \subseteq Y ball (D) x$
128	108 127	sstrd	$⊢ ((φ \land x \in ℝ^{+}) \land (k \in ℕ \land 2^{nd} (M (k)) < \frac{x}{2})) \to ball (D) (M (k)) \subseteq Y ball (D) x$
129	98 128	sstrd	$⊢ ((φ \land x \in ℝ^{+}) \land (k \in ℕ \land 2^{nd} (M (k)) < \frac{x}{2})) \to S (k) B k \subseteq Y ball (D) x$
130		sstr2	$⊢ S (k) B k \subseteq Y ball (D) x \to (Y ball (D) x \subseteq Z \to S (k) B k \subseteq Z)$
131	129 130	syl	$⊢ ((φ \land x \in ℝ^{+}) \land (k \in ℕ \land 2^{nd} (M (k)) < \frac{x}{2})) \to (Y ball (D) x \subseteq Z \to S (k) B k \subseteq Z)$
132		unisng	$⊢ Z \in U \to ⋃ \{Z\} = Z$
133	15 132	syl	$⊢ φ \to ⋃ \{Z\} = Z$
134	133	sseq2d	$⊢ φ \to (S (k) B k \subseteq ⋃ \{Z\} \leftrightarrow S (k) B k \subseteq Z)$
135	134	biimpar	$⊢ (φ \land S (k) B k \subseteq Z) \to S (k) B k \subseteq ⋃ \{Z\}$
136	15	snssd	$⊢ φ \to \{Z\} \subseteq U$
137		snex	$⊢ \{Z\} \in V$
138	137	elpw	$⊢ \{Z\} \in 𝒫 U \leftrightarrow \{Z\} \subseteq U$
139	136 138	sylibr	$⊢ φ \to \{Z\} \in 𝒫 U$
140		snfi	$⊢ \{Z\} \in Fin$
141	140	a1i	$⊢ φ \to \{Z\} \in Fin$
142	139 141	elind	$⊢ φ \to \{Z\} \in (𝒫 U \cap Fin)$
143		unieq	$⊢ v = \{Z\} \to ⋃ v = ⋃ \{Z\}$
144	143	sseq2d	$⊢ v = \{Z\} \to (S (k) B k \subseteq ⋃ v \leftrightarrow S (k) B k \subseteq ⋃ \{Z\})$
145	144	rspcev	$⊢ (\{Z\} \in (𝒫 U \cap Fin) \land S (k) B k \subseteq ⋃ \{Z\}) \to \exists v \in (𝒫 U \cap Fin) S (k) B k \subseteq ⋃ v$
146	142 145	sylan	$⊢ (φ \land S (k) B k \subseteq ⋃ \{Z\}) \to \exists v \in (𝒫 U \cap Fin) S (k) B k \subseteq ⋃ v$
147	135 146	syldan	$⊢ (φ \land S (k) B k \subseteq Z) \to \exists v \in (𝒫 U \cap Fin) S (k) B k \subseteq ⋃ v$
148		ovex	$⊢ S (k) B k \in V$
149		sseq1	$⊢ u = S (k) B k \to (u \subseteq ⋃ v \leftrightarrow S (k) B k \subseteq ⋃ v)$
150	149	rexbidv	$⊢ u = S (k) B k \to (\exists v \in (𝒫 U \cap Fin) u \subseteq ⋃ v \leftrightarrow \exists v \in (𝒫 U \cap Fin) S (k) B k \subseteq ⋃ v)$
151	150	notbid	$⊢ u = S (k) B k \to (\neg \exists v \in (𝒫 U \cap Fin) u \subseteq ⋃ v \leftrightarrow \neg \exists v \in (𝒫 U \cap Fin) S (k) B k \subseteq ⋃ v)$
152	148 151 2	elab2	$⊢ S (k) B k \in K \leftrightarrow \neg \exists v \in (𝒫 U \cap Fin) S (k) B k \subseteq ⋃ v$
153	152	con2bii	$⊢ \exists v \in (𝒫 U \cap Fin) S (k) B k \subseteq ⋃ v \leftrightarrow \neg S (k) B k \in K$
154	147 153	sylib	$⊢ (φ \land S (k) B k \subseteq Z) \to \neg S (k) B k \in K$
155	154	ex	$⊢ φ \to (S (k) B k \subseteq Z \to \neg S (k) B k \in K)$
156	155	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land (k \in ℕ \land 2^{nd} (M (k)) < \frac{x}{2})) \to (S (k) B k \subseteq Z \to \neg S (k) B k \in K)$
157	131 156	syld	$⊢ ((φ \land x \in ℝ^{+}) \land (k \in ℕ \land 2^{nd} (M (k)) < \frac{x}{2})) \to (Y ball (D) x \subseteq Z \to \neg S (k) B k \in K)$
158	38 157	mt2d	$⊢ ((φ \land x \in ℝ^{+}) \land (k \in ℕ \land 2^{nd} (M (k)) < \frac{x}{2})) \to \neg Y ball (D) x \subseteq Z$
159	29 158	rexlimddv	$⊢ (φ \land x \in ℝ^{+}) \to \neg Y ball (D) x \subseteq Z$
160	159	nrexdv	$⊢ φ \to \neg \exists x \in ℝ^{+} Y ball (D) x \subseteq Z$
161	22 160	pm2.21dd	$⊢ φ \to ψ$

Metamath Proof Explorer

Theorem heiborlem8

Proof