heiborlem10

Description: Lemma for heibor . The last remaining piece of the proof is to find an element C such that C G 0 , i.e. C is an element of ( F0 ) that has no finite subcover, which is true by heiborlem1 , since ( F0 ) is a finite cover of X , which has no finite subcover. Thus, the rest of the proof follows to a contradiction, and thus there must be a finite subcover of U that covers X , i.e. X is compact. (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)$
Assertion	heiborlem10	$⊢ (φ \land (U \subseteq J \land ⋃ J = ⋃ U)) \to \exists v \in (𝒫 U \cap Fin) ⋃ J = ⋃ v$

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		0nn0	$⊢ 0 \in ℕ_{0}$
9		inss2	$⊢ 𝒫 X \cap Fin \subseteq Fin$
10		ffvelcdm	$⊢ (F : ℕ_{0} ⟶ 𝒫 X \cap Fin \land 0 \in ℕ_{0}) \to F (0) \in (𝒫 X \cap Fin)$
11	9 10	sselid	$⊢ (F : ℕ_{0} ⟶ 𝒫 X \cap Fin \land 0 \in ℕ_{0}) \to F (0) \in Fin$
12	6 8 11	sylancl	$⊢ φ \to F (0) \in Fin$
13		fveq2	$⊢ n = 0 \to F (n) = F (0)$
14		oveq2	$⊢ n = 0 \to y B n = y B 0$
15	13 14	iuneq12d	$⊢ n = 0 \to ⋃_{y \in F (n)} (y B n) = ⋃_{y \in F (0)} (y B 0)$
16	15	eqeq2d	$⊢ n = 0 \to (X = ⋃_{y \in F (n)} (y B n) \leftrightarrow X = ⋃_{y \in F (0)} (y B 0))$
17	16	rspccva	$⊢ (\forall n \in ℕ_{0} X = ⋃_{y \in F (n)} (y B n) \land 0 \in ℕ_{0}) \to X = ⋃_{y \in F (0)} (y B 0)$
18	7 8 17	sylancl	$⊢ φ \to X = ⋃_{y \in F (0)} (y B 0)$
19		eqimss	$⊢ X = ⋃_{y \in F (0)} (y B 0) \to X \subseteq ⋃_{y \in F (0)} (y B 0)$
20	18 19	syl	$⊢ φ \to X \subseteq ⋃_{y \in F (0)} (y B 0)$
21		ovex	$⊢ y B 0 \in V$
22	1 2 21	heiborlem1	$⊢ (F (0) \in Fin \land X \subseteq ⋃_{y \in F (0)} (y B 0) \land X \in K) \to \exists y \in F (0) y B 0 \in K$
23		oveq1	$⊢ y = x \to y B 0 = x B 0$
24	23	eleq1d	$⊢ y = x \to (y B 0 \in K \leftrightarrow x B 0 \in K)$
25	24	cbvrexvw	$⊢ \exists y \in F (0) y B 0 \in K \leftrightarrow \exists x \in F (0) x B 0 \in K$
26	22 25	sylib	$⊢ (F (0) \in Fin \land X \subseteq ⋃_{y \in F (0)} (y B 0) \land X \in K) \to \exists x \in F (0) x B 0 \in K$
27	26	3expia	$⊢ (F (0) \in Fin \land X \subseteq ⋃_{y \in F (0)} (y B 0)) \to (X \in K \to \exists x \in F (0) x B 0 \in K)$
28	12 20 27	syl2anc	$⊢ φ \to (X \in K \to \exists x \in F (0) x B 0 \in K)$
29	28	adantr	$⊢ (φ \land (U \subseteq J \land ⋃ J = ⋃ U)) \to (X \in K \to \exists x \in F (0) x B 0 \in K)$
30		vex	$⊢ x \in V$
31		c0ex	$⊢ 0 \in V$
32	1 2 3 30 31	heiborlem2	$⊢ x G 0 \leftrightarrow (0 \in ℕ_{0} \land x \in F (0) \land x B 0 \in K)$
33	1 2 3 4 5 6 7	heiborlem3	$⊢ φ \to \exists g \forall x \in G (g (x) G (2^{nd} (x) + 1) \land B (x) \cap (g (x) B (2^{nd} (x) + 1)) \in K)$
34	33	ad2antrr	$⊢ ((φ \land (U \subseteq J \land ⋃ J = ⋃ U)) \land x G 0) \to \exists g \forall x \in G (g (x) G (2^{nd} (x) + 1) \land B (x) \cap (g (x) B (2^{nd} (x) + 1)) \in K)$
35	5	ad2antrr	$⊢ ((φ \land (U \subseteq J \land ⋃ J = ⋃ U)) \land (x G 0 \land \forall x \in G (g (x) G (2^{nd} (x) + 1) \land B (x) \cap (g (x) B (2^{nd} (x) + 1)) \in K))) \to D \in CMet (X)$
36	6	ad2antrr	$⊢ ((φ \land (U \subseteq J \land ⋃ J = ⋃ U)) \land (x G 0 \land \forall x \in G (g (x) G (2^{nd} (x) + 1) \land B (x) \cap (g (x) B (2^{nd} (x) + 1)) \in K))) \to F : ℕ_{0} ⟶ 𝒫 X \cap Fin$
37	7	ad2antrr	$⊢ ((φ \land (U \subseteq J \land ⋃ J = ⋃ U)) \land (x G 0 \land \forall x \in G (g (x) G (2^{nd} (x) + 1) \land B (x) \cap (g (x) B (2^{nd} (x) + 1)) \in K))) \to \forall n \in ℕ_{0} X = ⋃_{y \in F (n)} (y B n)$
38		simprr	$⊢ ((φ \land (U \subseteq J \land ⋃ J = ⋃ U)) \land (x G 0 \land \forall x \in G (g (x) G (2^{nd} (x) + 1) \land B (x) \cap (g (x) B (2^{nd} (x) + 1)) \in K))) \to \forall x \in G (g (x) G (2^{nd} (x) + 1) \land B (x) \cap (g (x) B (2^{nd} (x) + 1)) \in K)$
39		fveq2	$⊢ x = t \to g (x) = g (t)$
40		fveq2	$⊢ x = t \to 2^{nd} (x) = 2^{nd} (t)$
41	40	oveq1d	$⊢ x = t \to 2^{nd} (x) + 1 = 2^{nd} (t) + 1$
42	39 41	breq12d	$⊢ x = t \to (g (x) G (2^{nd} (x) + 1) \leftrightarrow g (t) G (2^{nd} (t) + 1))$
43		fveq2	$⊢ x = t \to B (x) = B (t)$
44	39 41	oveq12d	$⊢ x = t \to g (x) B (2^{nd} (x) + 1) = g (t) B (2^{nd} (t) + 1)$
45	43 44	ineq12d	$⊢ x = t \to B (x) \cap (g (x) B (2^{nd} (x) + 1)) = B (t) \cap (g (t) B (2^{nd} (t) + 1))$
46	45	eleq1d	$⊢ x = t \to (B (x) \cap (g (x) B (2^{nd} (x) + 1)) \in K \leftrightarrow B (t) \cap (g (t) B (2^{nd} (t) + 1)) \in K)$
47	42 46	anbi12d	$⊢ x = t \to ((g (x) G (2^{nd} (x) + 1) \land B (x) \cap (g (x) B (2^{nd} (x) + 1)) \in K) \leftrightarrow (g (t) G (2^{nd} (t) + 1) \land B (t) \cap (g (t) B (2^{nd} (t) + 1)) \in K))$
48	47	cbvralvw	$⊢ \forall x \in G (g (x) G (2^{nd} (x) + 1) \land B (x) \cap (g (x) B (2^{nd} (x) + 1)) \in K) \leftrightarrow \forall t \in G (g (t) G (2^{nd} (t) + 1) \land B (t) \cap (g (t) B (2^{nd} (t) + 1)) \in K)$
49	38 48	sylib	$⊢ ((φ \land (U \subseteq J \land ⋃ J = ⋃ U)) \land (x G 0 \land \forall x \in G (g (x) G (2^{nd} (x) + 1) \land B (x) \cap (g (x) B (2^{nd} (x) + 1)) \in K))) \to \forall t \in G (g (t) G (2^{nd} (t) + 1) \land B (t) \cap (g (t) B (2^{nd} (t) + 1)) \in K)$
50		simprl	$⊢ ((φ \land (U \subseteq J \land ⋃ J = ⋃ U)) \land (x G 0 \land \forall x \in G (g (x) G (2^{nd} (x) + 1) \land B (x) \cap (g (x) B (2^{nd} (x) + 1)) \in K))) \to x G 0$
51		eqeq1	$⊢ g = m \to (g = 0 \leftrightarrow m = 0)$
52		oveq1	$⊢ g = m \to g - 1 = m - 1$
53	51 52	ifbieq2d	$⊢ g = m \to if (g = 0, x, g - 1) = if (m = 0, x, m - 1)$
54	53	cbvmptv	$⊢ (g \in ℕ_{0} ⟼ if (g = 0, x, g - 1)) = (m \in ℕ_{0} ⟼ if (m = 0, x, m - 1))$
55		seqeq3	$⊢ (g \in ℕ_{0} ⟼ if (g = 0, x, g - 1)) = (m \in ℕ_{0} ⟼ if (m = 0, x, m - 1)) \to seq 0 (g, (g \in ℕ_{0} ⟼ if (g = 0, x, g - 1))) = seq 0 (g, (m \in ℕ_{0} ⟼ if (m = 0, x, m - 1)))$
56	54 55	ax-mp	$⊢ seq 0 (g, (g \in ℕ_{0} ⟼ if (g = 0, x, g - 1))) = seq 0 (g, (m \in ℕ_{0} ⟼ if (m = 0, x, m - 1)))$
57		eqid	$⊢ (n \in ℕ ⟼ ⟨seq 0 (g, (g \in ℕ_{0} ⟼ if (g = 0, x, g - 1))) (n), \frac{3}{2^{n}}⟩) = (n \in ℕ ⟼ ⟨seq 0 (g, (g \in ℕ_{0} ⟼ if (g = 0, x, g - 1))) (n), \frac{3}{2^{n}}⟩)$
58		simplrl	$⊢ ((φ \land (U \subseteq J \land ⋃ J = ⋃ U)) \land (x G 0 \land \forall x \in G (g (x) G (2^{nd} (x) + 1) \land B (x) \cap (g (x) B (2^{nd} (x) + 1)) \in K))) \to U \subseteq J$
59		cmetmet	$⊢ D \in CMet (X) \to D \in Met (X)$
60		metxmet	$⊢ D \in Met (X) \to D \in ∞Met (X)$
61	1	mopnuni	$⊢ D \in ∞Met (X) \to X = ⋃ J$
62	5 59 60 61	4syl	$⊢ φ \to X = ⋃ J$
63	62	adantr	$⊢ (φ \land (U \subseteq J \land ⋃ J = ⋃ U)) \to X = ⋃ J$
64		simprr	$⊢ (φ \land (U \subseteq J \land ⋃ J = ⋃ U)) \to ⋃ J = ⋃ U$
65	63 64	eqtr2d	$⊢ (φ \land (U \subseteq J \land ⋃ J = ⋃ U)) \to ⋃ U = X$
66	65	adantr	$⊢ ((φ \land (U \subseteq J \land ⋃ J = ⋃ U)) \land (x G 0 \land \forall x \in G (g (x) G (2^{nd} (x) + 1) \land B (x) \cap (g (x) B (2^{nd} (x) + 1)) \in K))) \to ⋃ U = X$
67	1 2 3 4 35 36 37 49 50 56 57 58 66	heiborlem9	$⊢ ((φ \land (U \subseteq J \land ⋃ J = ⋃ U)) \land (x G 0 \land \forall x \in G (g (x) G (2^{nd} (x) + 1) \land B (x) \cap (g (x) B (2^{nd} (x) + 1)) \in K))) \to \neg X \in K$
68	67	expr	$⊢ ((φ \land (U \subseteq J \land ⋃ J = ⋃ U)) \land x G 0) \to (\forall x \in G (g (x) G (2^{nd} (x) + 1) \land B (x) \cap (g (x) B (2^{nd} (x) + 1)) \in K) \to \neg X \in K)$
69	68	exlimdv	$⊢ ((φ \land (U \subseteq J \land ⋃ J = ⋃ U)) \land x G 0) \to (\exists g \forall x \in G (g (x) G (2^{nd} (x) + 1) \land B (x) \cap (g (x) B (2^{nd} (x) + 1)) \in K) \to \neg X \in K)$
70	34 69	mpd	$⊢ ((φ \land (U \subseteq J \land ⋃ J = ⋃ U)) \land x G 0) \to \neg X \in K$
71	32 70	sylan2br	$⊢ ((φ \land (U \subseteq J \land ⋃ J = ⋃ U)) \land (0 \in ℕ_{0} \land x \in F (0) \land x B 0 \in K)) \to \neg X \in K$
72	71	3exp2	$⊢ (φ \land (U \subseteq J \land ⋃ J = ⋃ U)) \to (0 \in ℕ_{0} \to (x \in F (0) \to (x B 0 \in K \to \neg X \in K)))$
73	8 72	mpi	$⊢ (φ \land (U \subseteq J \land ⋃ J = ⋃ U)) \to (x \in F (0) \to (x B 0 \in K \to \neg X \in K))$
74	73	rexlimdv	$⊢ (φ \land (U \subseteq J \land ⋃ J = ⋃ U)) \to (\exists x \in F (0) x B 0 \in K \to \neg X \in K)$
75	29 74	syld	$⊢ (φ \land (U \subseteq J \land ⋃ J = ⋃ U)) \to (X \in K \to \neg X \in K)$
76	75	pm2.01d	$⊢ (φ \land (U \subseteq J \land ⋃ J = ⋃ U)) \to \neg X \in K$
77		elfvdm	$⊢ D \in CMet (X) \to X \in dom CMet$
78		sseq1	$⊢ u = X \to (u \subseteq ⋃ v \leftrightarrow X \subseteq ⋃ v)$
79	78	rexbidv	$⊢ u = X \to (\exists v \in (𝒫 U \cap Fin) u \subseteq ⋃ v \leftrightarrow \exists v \in (𝒫 U \cap Fin) X \subseteq ⋃ v)$
80	79	notbid	$⊢ u = X \to (\neg \exists v \in (𝒫 U \cap Fin) u \subseteq ⋃ v \leftrightarrow \neg \exists v \in (𝒫 U \cap Fin) X \subseteq ⋃ v)$
81	80 2	elab2g	$⊢ X \in dom CMet \to (X \in K \leftrightarrow \neg \exists v \in (𝒫 U \cap Fin) X \subseteq ⋃ v)$
82	5 77 81	3syl	$⊢ φ \to (X \in K \leftrightarrow \neg \exists v \in (𝒫 U \cap Fin) X \subseteq ⋃ v)$
83	82	adantr	$⊢ (φ \land (U \subseteq J \land ⋃ J = ⋃ U)) \to (X \in K \leftrightarrow \neg \exists v \in (𝒫 U \cap Fin) X \subseteq ⋃ v)$
84	83	con2bid	$⊢ (φ \land (U \subseteq J \land ⋃ J = ⋃ U)) \to (\exists v \in (𝒫 U \cap Fin) X \subseteq ⋃ v \leftrightarrow \neg X \in K)$
85	76 84	mpbird	$⊢ (φ \land (U \subseteq J \land ⋃ J = ⋃ U)) \to \exists v \in (𝒫 U \cap Fin) X \subseteq ⋃ v$
86	62	ad2antrr	$⊢ ((φ \land (U \subseteq J \land ⋃ J = ⋃ U)) \land v \in (𝒫 U \cap Fin)) \to X = ⋃ J$
87	86	sseq1d	$⊢ ((φ \land (U \subseteq J \land ⋃ J = ⋃ U)) \land v \in (𝒫 U \cap Fin)) \to (X \subseteq ⋃ v \leftrightarrow ⋃ J \subseteq ⋃ v)$
88		inss1	$⊢ 𝒫 U \cap Fin \subseteq 𝒫 U$
89	88	sseli	$⊢ v \in (𝒫 U \cap Fin) \to v \in 𝒫 U$
90	89	elpwid	$⊢ v \in (𝒫 U \cap Fin) \to v \subseteq U$
91		simprl	$⊢ (φ \land (U \subseteq J \land ⋃ J = ⋃ U)) \to U \subseteq J$
92		sstr	$⊢ (v \subseteq U \land U \subseteq J) \to v \subseteq J$
93	92	unissd	$⊢ (v \subseteq U \land U \subseteq J) \to ⋃ v \subseteq ⋃ J$
94	90 91 93	syl2anr	$⊢ ((φ \land (U \subseteq J \land ⋃ J = ⋃ U)) \land v \in (𝒫 U \cap Fin)) \to ⋃ v \subseteq ⋃ J$
95	94	biantrud	$⊢ ((φ \land (U \subseteq J \land ⋃ J = ⋃ U)) \land v \in (𝒫 U \cap Fin)) \to (⋃ J \subseteq ⋃ v \leftrightarrow (⋃ J \subseteq ⋃ v \land ⋃ v \subseteq ⋃ J))$
96		eqss	$⊢ ⋃ J = ⋃ v \leftrightarrow (⋃ J \subseteq ⋃ v \land ⋃ v \subseteq ⋃ J)$
97	95 96	bitr4di	$⊢ ((φ \land (U \subseteq J \land ⋃ J = ⋃ U)) \land v \in (𝒫 U \cap Fin)) \to (⋃ J \subseteq ⋃ v \leftrightarrow ⋃ J = ⋃ v)$
98	87 97	bitrd	$⊢ ((φ \land (U \subseteq J \land ⋃ J = ⋃ U)) \land v \in (𝒫 U \cap Fin)) \to (X \subseteq ⋃ v \leftrightarrow ⋃ J = ⋃ v)$
99	98	rexbidva	$⊢ (φ \land (U \subseteq J \land ⋃ J = ⋃ U)) \to (\exists v \in (𝒫 U \cap Fin) X \subseteq ⋃ v \leftrightarrow \exists v \in (𝒫 U \cap Fin) ⋃ J = ⋃ v)$
100	85 99	mpbid	$⊢ (φ \land (U \subseteq J \land ⋃ J = ⋃ U)) \to \exists v \in (𝒫 U \cap Fin) ⋃ J = ⋃ v$

Metamath Proof Explorer

Theorem heiborlem10

Proof