stoweidlem46

Description: This lemma proves that sets U(t) as defined in Lemma 1 of BrosowskiDeutsh p. 90, are a cover of T \ U. Using this lemma, in a later theorem we will prove that a finite subcover exists. (Contributed by Glauco Siliprandi, 20-Apr-2017)

	Ref	Expression
Hypotheses	stoweidlem46.1	$⊢ \underline{Ⅎ} t U$
	stoweidlem46.2	$⊢ \underline{Ⅎ} h Q$
	stoweidlem46.3	$⊢ Ⅎ q φ$
	stoweidlem46.4	$⊢ Ⅎ t φ$
	stoweidlem46.5	$⊢ K = topGen (ran (.))$
	stoweidlem46.6	$⊢ Q = \{h \in A \| (h (Z) = 0 \land \forall t \in T (0 \leq h (t) \land h (t) \leq 1))\}$
	stoweidlem46.7	$⊢ W = \{w \in J \| \exists h \in Q w = \{t \in T \| 0 < h (t)\}\}$
	stoweidlem46.8	$⊢ T = ⋃ J$
	stoweidlem46.9	$⊢ φ \to J \in Comp$
	stoweidlem46.10	$⊢ φ \to A \subseteq J Cn K$
	stoweidlem46.11	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) + g (t)) \in A$
	stoweidlem46.12	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
	stoweidlem46.13	$⊢ (φ \land x \in ℝ) \to (t \in T ⟼ x) \in A$
	stoweidlem46.14	$⊢ (φ \land (r \in T \land t \in T \land r \neq t)) \to \exists q \in A q (r) \neq q (t)$
	stoweidlem46.15	$⊢ φ \to U \in J$
	stoweidlem46.16	$⊢ φ \to Z \in U$
	stoweidlem46.17	$⊢ φ \to T \in V$
Assertion	stoweidlem46	$⊢ φ \to T ∖ U \subseteq ⋃ W$

Proof

Step	Hyp	Ref	Expression
1		stoweidlem46.1	$⊢ \underline{Ⅎ} t U$
2		stoweidlem46.2	$⊢ \underline{Ⅎ} h Q$
3		stoweidlem46.3	$⊢ Ⅎ q φ$
4		stoweidlem46.4	$⊢ Ⅎ t φ$
5		stoweidlem46.5	$⊢ K = topGen (ran (.))$
6		stoweidlem46.6	$⊢ Q = \{h \in A \| (h (Z) = 0 \land \forall t \in T (0 \leq h (t) \land h (t) \leq 1))\}$
7		stoweidlem46.7	$⊢ W = \{w \in J \| \exists h \in Q w = \{t \in T \| 0 < h (t)\}\}$
8		stoweidlem46.8	$⊢ T = ⋃ J$
9		stoweidlem46.9	$⊢ φ \to J \in Comp$
10		stoweidlem46.10	$⊢ φ \to A \subseteq J Cn K$
11		stoweidlem46.11	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) + g (t)) \in A$
12		stoweidlem46.12	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
13		stoweidlem46.13	$⊢ (φ \land x \in ℝ) \to (t \in T ⟼ x) \in A$
14		stoweidlem46.14	$⊢ (φ \land (r \in T \land t \in T \land r \neq t)) \to \exists q \in A q (r) \neq q (t)$
15		stoweidlem46.15	$⊢ φ \to U \in J$
16		stoweidlem46.16	$⊢ φ \to Z \in U$
17		stoweidlem46.17	$⊢ φ \to T \in V$
18		nfv	$⊢ Ⅎ q s \in (T ∖ U)$
19	3 18	nfan	$⊢ Ⅎ q (φ \land s \in (T ∖ U))$
20		nfcv	$⊢ \underline{Ⅎ} t T$
21	20 1	nfdif	$⊢ \underline{Ⅎ} t (T ∖ U)$
22	21	nfel2	$⊢ Ⅎ t s \in (T ∖ U)$
23	4 22	nfan	$⊢ Ⅎ t (φ \land s \in (T ∖ U))$
24	9	adantr	$⊢ (φ \land s \in (T ∖ U)) \to J \in Comp$
25	10	adantr	$⊢ (φ \land s \in (T ∖ U)) \to A \subseteq J Cn K$
26	11	3adant1r	$⊢ ((φ \land s \in (T ∖ U)) \land f \in A \land g \in A) \to (t \in T ⟼ f (t) + g (t)) \in A$
27	12	3adant1r	$⊢ ((φ \land s \in (T ∖ U)) \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
28	13	adantlr	$⊢ ((φ \land s \in (T ∖ U)) \land x \in ℝ) \to (t \in T ⟼ x) \in A$
29	14	adantlr	$⊢ ((φ \land s \in (T ∖ U)) \land (r \in T \land t \in T \land r \neq t)) \to \exists q \in A q (r) \neq q (t)$
30	15	adantr	$⊢ (φ \land s \in (T ∖ U)) \to U \in J$
31	16	adantr	$⊢ (φ \land s \in (T ∖ U)) \to Z \in U$
32		simpr	$⊢ (φ \land s \in (T ∖ U)) \to s \in (T ∖ U)$
33	19 23 2 5 6 8 24 25 26 27 28 29 30 31 32	stoweidlem43	$⊢ (φ \land s \in (T ∖ U)) \to \exists h (h \in Q \land 0 < h (s))$
34		nfv	$⊢ Ⅎ g (h \in Q \land 0 < h (s))$
35	2	nfel2	$⊢ Ⅎ h g \in Q$
36		nfv	$⊢ Ⅎ h 0 < g (s)$
37	35 36	nfan	$⊢ Ⅎ h (g \in Q \land 0 < g (s))$
38		eleq1	$⊢ h = g \to (h \in Q \leftrightarrow g \in Q)$
39		fveq1	$⊢ h = g \to h (s) = g (s)$
40	39	breq2d	$⊢ h = g \to (0 < h (s) \leftrightarrow 0 < g (s))$
41	38 40	anbi12d	$⊢ h = g \to ((h \in Q \land 0 < h (s)) \leftrightarrow (g \in Q \land 0 < g (s)))$
42	34 37 41	cbvexv1	$⊢ \exists h (h \in Q \land 0 < h (s)) \leftrightarrow \exists g (g \in Q \land 0 < g (s))$
43	33 42	sylib	$⊢ (φ \land s \in (T ∖ U)) \to \exists g (g \in Q \land 0 < g (s))$
44		rabexg	$⊢ T \in V \to \{t \in T \| 0 < g (t)\} \in V$
45	17 44	syl	$⊢ φ \to \{t \in T \| 0 < g (t)\} \in V$
46	45	ad2antrr	$⊢ ((φ \land s \in (T ∖ U)) \land (g \in Q \land 0 < g (s))) \to \{t \in T \| 0 < g (t)\} \in V$
47		eldifi	$⊢ s \in (T ∖ U) \to s \in T$
48	47	ad2antlr	$⊢ ((φ \land s \in (T ∖ U)) \land (g \in Q \land 0 < g (s))) \to s \in T$
49		simprr	$⊢ ((φ \land s \in (T ∖ U)) \land (g \in Q \land 0 < g (s))) \to 0 < g (s)$
50		fveq2	$⊢ t = s \to g (t) = g (s)$
51	50	breq2d	$⊢ t = s \to (0 < g (t) \leftrightarrow 0 < g (s))$
52	51	elrab	$⊢ s \in \{t \in T \| 0 < g (t)\} \leftrightarrow (s \in T \land 0 < g (s))$
53	48 49 52	sylanbrc	$⊢ ((φ \land s \in (T ∖ U)) \land (g \in Q \land 0 < g (s))) \to s \in \{t \in T \| 0 < g (t)\}$
54		simpll	$⊢ ((φ \land s \in (T ∖ U)) \land (g \in Q \land 0 < g (s))) \to φ$
55	10	adantr	$⊢ (φ \land g \in Q) \to A \subseteq J Cn K$
56		simpr	$⊢ (φ \land g \in Q) \to g \in Q$
57	56 6	eleqtrdi	$⊢ (φ \land g \in Q) \to g \in \{h \in A \| (h (Z) = 0 \land \forall t \in T (0 \leq h (t) \land h (t) \leq 1))\}$
58		fveq1	$⊢ h = g \to h (Z) = g (Z)$
59	58	eqeq1d	$⊢ h = g \to (h (Z) = 0 \leftrightarrow g (Z) = 0)$
60		fveq1	$⊢ h = g \to h (t) = g (t)$
61	60	breq2d	$⊢ h = g \to (0 \leq h (t) \leftrightarrow 0 \leq g (t))$
62	60	breq1d	$⊢ h = g \to (h (t) \leq 1 \leftrightarrow g (t) \leq 1)$
63	61 62	anbi12d	$⊢ h = g \to ((0 \leq h (t) \land h (t) \leq 1) \leftrightarrow (0 \leq g (t) \land g (t) \leq 1))$
64	63	ralbidv	$⊢ h = g \to (\forall t \in T (0 \leq h (t) \land h (t) \leq 1) \leftrightarrow \forall t \in T (0 \leq g (t) \land g (t) \leq 1))$
65	59 64	anbi12d	$⊢ h = g \to ((h (Z) = 0 \land \forall t \in T (0 \leq h (t) \land h (t) \leq 1)) \leftrightarrow (g (Z) = 0 \land \forall t \in T (0 \leq g (t) \land g (t) \leq 1)))$
66	65	elrab	$⊢ g \in \{h \in A \| (h (Z) = 0 \land \forall t \in T (0 \leq h (t) \land h (t) \leq 1))\} \leftrightarrow (g \in A \land (g (Z) = 0 \land \forall t \in T (0 \leq g (t) \land g (t) \leq 1)))$
67	57 66	sylib	$⊢ (φ \land g \in Q) \to (g \in A \land (g (Z) = 0 \land \forall t \in T (0 \leq g (t) \land g (t) \leq 1)))$
68	67	simpld	$⊢ (φ \land g \in Q) \to g \in A$
69	55 68	sseldd	$⊢ (φ \land g \in Q) \to g \in (J Cn K)$
70	69	ad2ant2r	$⊢ ((φ \land s \in (T ∖ U)) \land (g \in Q \land 0 < g (s))) \to g \in (J Cn K)$
71		nfcv	$⊢ \underline{Ⅎ} t 0$
72		nfcv	$⊢ \underline{Ⅎ} t g$
73		nfv	$⊢ Ⅎ t g \in (J Cn K)$
74	4 73	nfan	$⊢ Ⅎ t (φ \land g \in (J Cn K))$
75		eqid	$⊢ \{t \in T \| 0 < g (t)\} = \{t \in T \| 0 < g (t)\}$
76		0xr	$⊢ 0 \in ℝ^{*}$
77	76	a1i	$⊢ (φ \land g \in (J Cn K)) \to 0 \in ℝ^{*}$
78		simpr	$⊢ (φ \land g \in (J Cn K)) \to g \in (J Cn K)$
79	71 72 74 5 8 75 77 78	rfcnpre1	$⊢ (φ \land g \in (J Cn K)) \to \{t \in T \| 0 < g (t)\} \in J$
80	54 70 79	syl2anc	$⊢ ((φ \land s \in (T ∖ U)) \land (g \in Q \land 0 < g (s))) \to \{t \in T \| 0 < g (t)\} \in J$
81		eqidd	$⊢ (φ \land g \in Q) \to \{t \in T \| 0 < g (t)\} = \{t \in T \| 0 < g (t)\}$
82		nfv	$⊢ Ⅎ h \{t \in T \| 0 < g (t)\} = \{t \in T \| 0 < g (t)\}$
83		nfcv	$⊢ \underline{Ⅎ} h g$
84	60	breq2d	$⊢ h = g \to (0 < h (t) \leftrightarrow 0 < g (t))$
85	84	rabbidv	$⊢ h = g \to \{t \in T \| 0 < h (t)\} = \{t \in T \| 0 < g (t)\}$
86	85	eqeq2d	$⊢ h = g \to (\{t \in T \| 0 < g (t)\} = \{t \in T \| 0 < h (t)\} \leftrightarrow \{t \in T \| 0 < g (t)\} = \{t \in T \| 0 < g (t)\})$
87	82 83 2 86	rspcegf	$⊢ (g \in Q \land \{t \in T \| 0 < g (t)\} = \{t \in T \| 0 < g (t)\}) \to \exists h \in Q \{t \in T \| 0 < g (t)\} = \{t \in T \| 0 < h (t)\}$
88	56 81 87	syl2anc	$⊢ (φ \land g \in Q) \to \exists h \in Q \{t \in T \| 0 < g (t)\} = \{t \in T \| 0 < h (t)\}$
89	88	ad2ant2r	$⊢ ((φ \land s \in (T ∖ U)) \land (g \in Q \land 0 < g (s))) \to \exists h \in Q \{t \in T \| 0 < g (t)\} = \{t \in T \| 0 < h (t)\}$
90		eqeq1	$⊢ w = \{t \in T \| 0 < g (t)\} \to (w = \{t \in T \| 0 < h (t)\} \leftrightarrow \{t \in T \| 0 < g (t)\} = \{t \in T \| 0 < h (t)\})$
91	90	rexbidv	$⊢ w = \{t \in T \| 0 < g (t)\} \to (\exists h \in Q w = \{t \in T \| 0 < h (t)\} \leftrightarrow \exists h \in Q \{t \in T \| 0 < g (t)\} = \{t \in T \| 0 < h (t)\})$
92	91	elrab	$⊢ \{t \in T \| 0 < g (t)\} \in \{w \in J \| \exists h \in Q w = \{t \in T \| 0 < h (t)\}\} \leftrightarrow (\{t \in T \| 0 < g (t)\} \in J \land \exists h \in Q \{t \in T \| 0 < g (t)\} = \{t \in T \| 0 < h (t)\})$
93	80 89 92	sylanbrc	$⊢ ((φ \land s \in (T ∖ U)) \land (g \in Q \land 0 < g (s))) \to \{t \in T \| 0 < g (t)\} \in \{w \in J \| \exists h \in Q w = \{t \in T \| 0 < h (t)\}\}$
94	93 7	eleqtrrdi	$⊢ ((φ \land s \in (T ∖ U)) \land (g \in Q \land 0 < g (s))) \to \{t \in T \| 0 < g (t)\} \in W$
95		nfcv	$⊢ \underline{Ⅎ} w \{t \in T \| 0 < g (t)\}$
96		nfv	$⊢ Ⅎ w s \in \{t \in T \| 0 < g (t)\}$
97		nfrab1	$⊢ \underline{Ⅎ} w \{w \in J \| \exists h \in Q w = \{t \in T \| 0 < h (t)\}\}$
98	7 97	nfcxfr	$⊢ \underline{Ⅎ} w W$
99	98	nfel2	$⊢ Ⅎ w \{t \in T \| 0 < g (t)\} \in W$
100	96 99	nfan	$⊢ Ⅎ w (s \in \{t \in T \| 0 < g (t)\} \land \{t \in T \| 0 < g (t)\} \in W)$
101		eleq2	$⊢ w = \{t \in T \| 0 < g (t)\} \to (s \in w \leftrightarrow s \in \{t \in T \| 0 < g (t)\})$
102		eleq1	$⊢ w = \{t \in T \| 0 < g (t)\} \to (w \in W \leftrightarrow \{t \in T \| 0 < g (t)\} \in W)$
103	101 102	anbi12d	$⊢ w = \{t \in T \| 0 < g (t)\} \to ((s \in w \land w \in W) \leftrightarrow (s \in \{t \in T \| 0 < g (t)\} \land \{t \in T \| 0 < g (t)\} \in W))$
104	95 100 103	spcegf	$⊢ \{t \in T \| 0 < g (t)\} \in V \to ((s \in \{t \in T \| 0 < g (t)\} \land \{t \in T \| 0 < g (t)\} \in W) \to \exists w (s \in w \land w \in W))$
105	104	imp	$⊢ (\{t \in T \| 0 < g (t)\} \in V \land (s \in \{t \in T \| 0 < g (t)\} \land \{t \in T \| 0 < g (t)\} \in W)) \to \exists w (s \in w \land w \in W)$
106	46 53 94 105	syl12anc	$⊢ ((φ \land s \in (T ∖ U)) \land (g \in Q \land 0 < g (s))) \to \exists w (s \in w \land w \in W)$
107	43 106	exlimddv	$⊢ (φ \land s \in (T ∖ U)) \to \exists w (s \in w \land w \in W)$
108		nfcv	$⊢ \underline{Ⅎ} w s$
109	108 98	elunif	$⊢ s \in ⋃ W \leftrightarrow \exists w (s \in w \land w \in W)$
110	107 109	sylibr	$⊢ (φ \land s \in (T ∖ U)) \to s \in ⋃ W$
111	110	ex	$⊢ φ \to (s \in (T ∖ U) \to s \in ⋃ W)$
112	111	ssrdv	$⊢ φ \to T ∖ U \subseteq ⋃ W$

Metamath Proof Explorer

Theorem stoweidlem46

Proof