stoweidlem52

Description: There exists a neighborhood V as in Lemma 1 of BrosowskiDeutsh p. 90. Here Z is used to represent t_0 in the paper, and v is used to represent V in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017)

	Ref	Expression
Hypotheses	stoweidlem52.1	$⊢ \underline{Ⅎ} t U$
	stoweidlem52.2	$⊢ Ⅎ t φ$
	stoweidlem52.3	$⊢ \underline{Ⅎ} t P$
	stoweidlem52.4	$⊢ K = topGen (ran (.))$
	stoweidlem52.5	$⊢ V = \{t \in T \| P (t) < \frac{D}{2}\}$
	stoweidlem52.7	$⊢ T = ⋃ J$
	stoweidlem52.8	$⊢ C = J Cn K$
	stoweidlem52.9	$⊢ φ \to A \subseteq C$
	stoweidlem52.10	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) + g (t)) \in A$
	stoweidlem52.11	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
	stoweidlem52.12	$⊢ (φ \land a \in ℝ) \to (t \in T ⟼ a) \in A$
	stoweidlem52.13	$⊢ φ \to D \in ℝ^{+}$
	stoweidlem52.14	$⊢ φ \to D < 1$
	stoweidlem52.15	$⊢ φ \to U \in J$
	stoweidlem52.16	$⊢ φ \to Z \in U$
	stoweidlem52.17	$⊢ φ \to P \in A$
	stoweidlem52.18	$⊢ φ \to \forall t \in T (0 \leq P (t) \land P (t) \leq 1)$
	stoweidlem52.19	$⊢ φ \to P (Z) = 0$
	stoweidlem52.20	$⊢ φ \to \forall t \in (T ∖ U) D \leq P (t)$
Assertion	stoweidlem52	$⊢ φ \to \exists v \in J ((Z \in v \land v \subseteq U) \land \forall e \in ℝ^{+} \exists x \in A (\forall t \in T (0 \leq x (t) \land x (t) \leq 1) \land \forall t \in v x (t) < e \land \forall t \in (T ∖ U) 1 - e < x (t)))$

Proof

Step	Hyp	Ref	Expression
1		stoweidlem52.1	$⊢ \underline{Ⅎ} t U$
2		stoweidlem52.2	$⊢ Ⅎ t φ$
3		stoweidlem52.3	$⊢ \underline{Ⅎ} t P$
4		stoweidlem52.4	$⊢ K = topGen (ran (.))$
5		stoweidlem52.5	$⊢ V = \{t \in T \| P (t) < \frac{D}{2}\}$
6		stoweidlem52.7	$⊢ T = ⋃ J$
7		stoweidlem52.8	$⊢ C = J Cn K$
8		stoweidlem52.9	$⊢ φ \to A \subseteq C$
9		stoweidlem52.10	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) + g (t)) \in A$
10		stoweidlem52.11	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
11		stoweidlem52.12	$⊢ (φ \land a \in ℝ) \to (t \in T ⟼ a) \in A$
12		stoweidlem52.13	$⊢ φ \to D \in ℝ^{+}$
13		stoweidlem52.14	$⊢ φ \to D < 1$
14		stoweidlem52.15	$⊢ φ \to U \in J$
15		stoweidlem52.16	$⊢ φ \to Z \in U$
16		stoweidlem52.17	$⊢ φ \to P \in A$
17		stoweidlem52.18	$⊢ φ \to \forall t \in T (0 \leq P (t) \land P (t) \leq 1)$
18		stoweidlem52.19	$⊢ φ \to P (Z) = 0$
19		stoweidlem52.20	$⊢ φ \to \forall t \in (T ∖ U) D \leq P (t)$
20		nfcv	$⊢ \underline{Ⅎ} t (\frac{D}{2})$
21	12	rpred	$⊢ φ \to D \in ℝ$
22	21	rehalfcld	$⊢ φ \to \frac{D}{2} \in ℝ$
23	22	rexrd	$⊢ φ \to \frac{D}{2} \in ℝ^{*}$
24	8 7	sseqtrdi	$⊢ φ \to A \subseteq J Cn K$
25	24 16	sseldd	$⊢ φ \to P \in (J Cn K)$
26	20 3 2 4 6 5 23 25	rfcnpre2	$⊢ φ \to V \in J$
27		elssuni	$⊢ U \in J \to U \subseteq ⋃ J$
28	14 27	syl	$⊢ φ \to U \subseteq ⋃ J$
29	28 6	sseqtrrdi	$⊢ φ \to U \subseteq T$
30	29 15	sseldd	$⊢ φ \to Z \in T$
31		2re	$⊢ 2 \in ℝ$
32	31	a1i	$⊢ φ \to 2 \in ℝ$
33	12	rpgt0d	$⊢ φ \to 0 < D$
34		2pos	$⊢ 0 < 2$
35	34	a1i	$⊢ φ \to 0 < 2$
36	21 32 33 35	divgt0d	$⊢ φ \to 0 < \frac{D}{2}$
37	18 36	eqbrtrd	$⊢ φ \to P (Z) < \frac{D}{2}$
38		nfcv	$⊢ \underline{Ⅎ} t Z$
39		nfcv	$⊢ \underline{Ⅎ} t T$
40	3 38	nffv	$⊢ \underline{Ⅎ} t P (Z)$
41		nfcv	$⊢ \underline{Ⅎ} t <$
42	40 41 20	nfbr	$⊢ Ⅎ t P (Z) < \frac{D}{2}$
43		fveq2	$⊢ t = Z \to P (t) = P (Z)$
44	43	breq1d	$⊢ t = Z \to (P (t) < \frac{D}{2} \leftrightarrow P (Z) < \frac{D}{2})$
45	38 39 42 44	elrabf	$⊢ Z \in \{t \in T \| P (t) < \frac{D}{2}\} \leftrightarrow (Z \in T \land P (Z) < \frac{D}{2})$
46	30 37 45	sylanbrc	$⊢ φ \to Z \in \{t \in T \| P (t) < \frac{D}{2}\}$
47	46 5	eleqtrrdi	$⊢ φ \to Z \in V$
48		nfrab1	$⊢ \underline{Ⅎ} t \{t \in T \| P (t) < \frac{D}{2}\}$
49	5 48	nfcxfr	$⊢ \underline{Ⅎ} t V$
50	8 16	sseldd	$⊢ φ \to P \in C$
51	4 6 7 50	fcnre	$⊢ φ \to P : T ⟶ ℝ$
52	51	adantr	$⊢ (φ \land t \in V) \to P : T ⟶ ℝ$
53	5	rabeq2i	$⊢ t \in V \leftrightarrow (t \in T \land P (t) < \frac{D}{2})$
54	53	biimpi	$⊢ t \in V \to (t \in T \land P (t) < \frac{D}{2})$
55	54	adantl	$⊢ (φ \land t \in V) \to (t \in T \land P (t) < \frac{D}{2})$
56	55	simpld	$⊢ (φ \land t \in V) \to t \in T$
57	52 56	ffvelrnd	$⊢ (φ \land t \in V) \to P (t) \in ℝ$
58	22	adantr	$⊢ (φ \land t \in V) \to \frac{D}{2} \in ℝ$
59	21	adantr	$⊢ (φ \land t \in V) \to D \in ℝ$
60	55	simprd	$⊢ (φ \land t \in V) \to P (t) < \frac{D}{2}$
61		halfpos	$⊢ D \in ℝ \to (0 < D \leftrightarrow \frac{D}{2} < D)$
62	21 61	syl	$⊢ φ \to (0 < D \leftrightarrow \frac{D}{2} < D)$
63	33 62	mpbid	$⊢ φ \to \frac{D}{2} < D$
64	63	adantr	$⊢ (φ \land t \in V) \to \frac{D}{2} < D$
65	57 58 59 60 64	lttrd	$⊢ (φ \land t \in V) \to P (t) < D$
66	65	adantr	$⊢ ((φ \land t \in V) \land \neg t \in U) \to P (t) < D$
67	21	ad2antrr	$⊢ ((φ \land t \in V) \land \neg t \in U) \to D \in ℝ$
68	57	adantr	$⊢ ((φ \land t \in V) \land \neg t \in U) \to P (t) \in ℝ$
69	19	ad2antrr	$⊢ ((φ \land t \in V) \land \neg t \in U) \to \forall t \in (T ∖ U) D \leq P (t)$
70	56	anim1i	$⊢ ((φ \land t \in V) \land \neg t \in U) \to (t \in T \land \neg t \in U)$
71		eldif	$⊢ t \in (T ∖ U) \leftrightarrow (t \in T \land \neg t \in U)$
72	70 71	sylibr	$⊢ ((φ \land t \in V) \land \neg t \in U) \to t \in (T ∖ U)$
73		rsp	$⊢ \forall t \in (T ∖ U) D \leq P (t) \to (t \in (T ∖ U) \to D \leq P (t))$
74	69 72 73	sylc	$⊢ ((φ \land t \in V) \land \neg t \in U) \to D \leq P (t)$
75	67 68 74	lensymd	$⊢ ((φ \land t \in V) \land \neg t \in U) \to \neg P (t) < D$
76	66 75	condan	$⊢ (φ \land t \in V) \to t \in U$
77	76	ex	$⊢ φ \to (t \in V \to t \in U)$
78	2 49 1 77	ssrd	$⊢ φ \to V \subseteq U$
79		nfv	$⊢ Ⅎ t e \in ℝ^{+}$
80	2 79	nfan	$⊢ Ⅎ t (φ \land e \in ℝ^{+})$
81		nfv	$⊢ Ⅎ t y \in A$
82	80 81	nfan	$⊢ Ⅎ t ((φ \land e \in ℝ^{+}) \land y \in A)$
83		nfra1	$⊢ Ⅎ t \forall t \in T (0 \leq y (t) \land y (t) \leq 1)$
84		nfra1	$⊢ Ⅎ t \forall t \in V 1 - e < y (t)$
85		nfra1	$⊢ Ⅎ t \forall t \in (T ∖ U) y (t) < e$
86	83 84 85	nf3an	$⊢ Ⅎ t (\forall t \in T (0 \leq y (t) \land y (t) \leq 1) \land \forall t \in V 1 - e < y (t) \land \forall t \in (T ∖ U) y (t) < e)$
87	82 86	nfan	$⊢ Ⅎ t (((φ \land e \in ℝ^{+}) \land y \in A) \land (\forall t \in T (0 \leq y (t) \land y (t) \leq 1) \land \forall t \in V 1 - e < y (t) \land \forall t \in (T ∖ U) y (t) < e))$
88		eqid	$⊢ (t \in T ⟼ 1 - y (t)) = (t \in T ⟼ 1 - y (t))$
89		eqid	$⊢ (t \in T ⟼ 1) = (t \in T ⟼ 1)$
90		ssrab2	$⊢ \{t \in T \| P (t) < \frac{D}{2}\} \subseteq T$
91	5 90	eqsstri	$⊢ V \subseteq T$
92		simplr	$⊢ (((φ \land e \in ℝ^{+}) \land y \in A) \land (\forall t \in T (0 \leq y (t) \land y (t) \leq 1) \land \forall t \in V 1 - e < y (t) \land \forall t \in (T ∖ U) y (t) < e)) \to y \in A$
93		simplll	$⊢ (((φ \land e \in ℝ^{+}) \land y \in A) \land (\forall t \in T (0 \leq y (t) \land y (t) \leq 1) \land \forall t \in V 1 - e < y (t) \land \forall t \in (T ∖ U) y (t) < e)) \to φ$
94	8	sselda	$⊢ (φ \land y \in A) \to y \in C$
95	4 6 7 94	fcnre	$⊢ (φ \land y \in A) \to y : T ⟶ ℝ$
96	93 92 95	syl2anc	$⊢ (((φ \land e \in ℝ^{+}) \land y \in A) \land (\forall t \in T (0 \leq y (t) \land y (t) \leq 1) \land \forall t \in V 1 - e < y (t) \land \forall t \in (T ∖ U) y (t) < e)) \to y : T ⟶ ℝ$
97	8	sselda	$⊢ (φ \land f \in A) \to f \in C$
98	4 6 7 97	fcnre	$⊢ (φ \land f \in A) \to f : T ⟶ ℝ$
99	93 98	sylan	$⊢ ((((φ \land e \in ℝ^{+}) \land y \in A) \land (\forall t \in T (0 \leq y (t) \land y (t) \leq 1) \land \forall t \in V 1 - e < y (t) \land \forall t \in (T ∖ U) y (t) < e)) \land f \in A) \to f : T ⟶ ℝ$
100	93 9	syl3an1	$⊢ ((((φ \land e \in ℝ^{+}) \land y \in A) \land (\forall t \in T (0 \leq y (t) \land y (t) \leq 1) \land \forall t \in V 1 - e < y (t) \land \forall t \in (T ∖ U) y (t) < e)) \land f \in A \land g \in A) \to (t \in T ⟼ f (t) + g (t)) \in A$
101	93 10	syl3an1	$⊢ ((((φ \land e \in ℝ^{+}) \land y \in A) \land (\forall t \in T (0 \leq y (t) \land y (t) \leq 1) \land \forall t \in V 1 - e < y (t) \land \forall t \in (T ∖ U) y (t) < e)) \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
102	93 11	sylan	$⊢ ((((φ \land e \in ℝ^{+}) \land y \in A) \land (\forall t \in T (0 \leq y (t) \land y (t) \leq 1) \land \forall t \in V 1 - e < y (t) \land \forall t \in (T ∖ U) y (t) < e)) \land a \in ℝ) \to (t \in T ⟼ a) \in A$
103		simpllr	$⊢ (((φ \land e \in ℝ^{+}) \land y \in A) \land (\forall t \in T (0 \leq y (t) \land y (t) \leq 1) \land \forall t \in V 1 - e < y (t) \land \forall t \in (T ∖ U) y (t) < e)) \to e \in ℝ^{+}$
104		simpr1	$⊢ (((φ \land e \in ℝ^{+}) \land y \in A) \land (\forall t \in T (0 \leq y (t) \land y (t) \leq 1) \land \forall t \in V 1 - e < y (t) \land \forall t \in (T ∖ U) y (t) < e)) \to \forall t \in T (0 \leq y (t) \land y (t) \leq 1)$
105		simpr2	$⊢ (((φ \land e \in ℝ^{+}) \land y \in A) \land (\forall t \in T (0 \leq y (t) \land y (t) \leq 1) \land \forall t \in V 1 - e < y (t) \land \forall t \in (T ∖ U) y (t) < e)) \to \forall t \in V 1 - e < y (t)$
106		simpr3	$⊢ (((φ \land e \in ℝ^{+}) \land y \in A) \land (\forall t \in T (0 \leq y (t) \land y (t) \leq 1) \land \forall t \in V 1 - e < y (t) \land \forall t \in (T ∖ U) y (t) < e)) \to \forall t \in (T ∖ U) y (t) < e$
107	87 88 89 91 92 96 99 100 101 102 103 104 105 106	stoweidlem41	$⊢ (((φ \land e \in ℝ^{+}) \land y \in A) \land (\forall t \in T (0 \leq y (t) \land y (t) \leq 1) \land \forall t \in V 1 - e < y (t) \land \forall t \in (T ∖ U) y (t) < e)) \to \exists x \in A (\forall t \in T (0 \leq x (t) \land x (t) \leq 1) \land \forall t \in V x (t) < e \land \forall t \in (T ∖ U) 1 - e < x (t))$
108	12	adantr	$⊢ (φ \land e \in ℝ^{+}) \to D \in ℝ^{+}$
109	13	adantr	$⊢ (φ \land e \in ℝ^{+}) \to D < 1$
110	16	adantr	$⊢ (φ \land e \in ℝ^{+}) \to P \in A$
111	51	adantr	$⊢ (φ \land e \in ℝ^{+}) \to P : T ⟶ ℝ$
112	17	adantr	$⊢ (φ \land e \in ℝ^{+}) \to \forall t \in T (0 \leq P (t) \land P (t) \leq 1)$
113	19	adantr	$⊢ (φ \land e \in ℝ^{+}) \to \forall t \in (T ∖ U) D \leq P (t)$
114	98	adantlr	$⊢ ((φ \land e \in ℝ^{+}) \land f \in A) \to f : T ⟶ ℝ$
115	9	3adant1r	$⊢ ((φ \land e \in ℝ^{+}) \land f \in A \land g \in A) \to (t \in T ⟼ f (t) + g (t)) \in A$
116	10	3adant1r	$⊢ ((φ \land e \in ℝ^{+}) \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
117	11	adantlr	$⊢ ((φ \land e \in ℝ^{+}) \land a \in ℝ) \to (t \in T ⟼ a) \in A$
118		simpr	$⊢ (φ \land e \in ℝ^{+}) \to e \in ℝ^{+}$
119	3 80 5 108 109 110 111 112 113 114 115 116 117 118	stoweidlem49	$⊢ (φ \land e \in ℝ^{+}) \to \exists y \in A (\forall t \in T (0 \leq y (t) \land y (t) \leq 1) \land \forall t \in V 1 - e < y (t) \land \forall t \in (T ∖ U) y (t) < e)$
120	107 119	r19.29a	$⊢ (φ \land e \in ℝ^{+}) \to \exists x \in A (\forall t \in T (0 \leq x (t) \land x (t) \leq 1) \land \forall t \in V x (t) < e \land \forall t \in (T ∖ U) 1 - e < x (t))$
121	120	ralrimiva	$⊢ φ \to \forall e \in ℝ^{+} \exists x \in A (\forall t \in T (0 \leq x (t) \land x (t) \leq 1) \land \forall t \in V x (t) < e \land \forall t \in (T ∖ U) 1 - e < x (t))$
122	47 78 121	jca31	$⊢ φ \to ((Z \in V \land V \subseteq U) \land \forall e \in ℝ^{+} \exists x \in A (\forall t \in T (0 \leq x (t) \land x (t) \leq 1) \land \forall t \in V x (t) < e \land \forall t \in (T ∖ U) 1 - e < x (t)))$
123		eleq2	$⊢ v = V \to (Z \in v \leftrightarrow Z \in V)$
124		sseq1	$⊢ v = V \to (v \subseteq U \leftrightarrow V \subseteq U)$
125	123 124	anbi12d	$⊢ v = V \to ((Z \in v \land v \subseteq U) \leftrightarrow (Z \in V \land V \subseteq U))$
126		nfcv	$⊢ \underline{Ⅎ} t v$
127	126 49	raleqf	$⊢ v = V \to (\forall t \in v x (t) < e \leftrightarrow \forall t \in V x (t) < e)$
128	127	3anbi2d	$⊢ v = V \to ((\forall t \in T (0 \leq x (t) \land x (t) \leq 1) \land \forall t \in v x (t) < e \land \forall t \in (T ∖ U) 1 - e < x (t)) \leftrightarrow (\forall t \in T (0 \leq x (t) \land x (t) \leq 1) \land \forall t \in V x (t) < e \land \forall t \in (T ∖ U) 1 - e < x (t)))$
129	128	rexbidv	$⊢ v = V \to (\exists x \in A (\forall t \in T (0 \leq x (t) \land x (t) \leq 1) \land \forall t \in v x (t) < e \land \forall t \in (T ∖ U) 1 - e < x (t)) \leftrightarrow \exists x \in A (\forall t \in T (0 \leq x (t) \land x (t) \leq 1) \land \forall t \in V x (t) < e \land \forall t \in (T ∖ U) 1 - e < x (t)))$
130	129	ralbidv	$⊢ v = V \to (\forall e \in ℝ^{+} \exists x \in A (\forall t \in T (0 \leq x (t) \land x (t) \leq 1) \land \forall t \in v x (t) < e \land \forall t \in (T ∖ U) 1 - e < x (t)) \leftrightarrow \forall e \in ℝ^{+} \exists x \in A (\forall t \in T (0 \leq x (t) \land x (t) \leq 1) \land \forall t \in V x (t) < e \land \forall t \in (T ∖ U) 1 - e < x (t)))$
131	125 130	anbi12d	$⊢ v = V \to (((Z \in v \land v \subseteq U) \land \forall e \in ℝ^{+} \exists x \in A (\forall t \in T (0 \leq x (t) \land x (t) \leq 1) \land \forall t \in v x (t) < e \land \forall t \in (T ∖ U) 1 - e < x (t))) \leftrightarrow ((Z \in V \land V \subseteq U) \land \forall e \in ℝ^{+} \exists x \in A (\forall t \in T (0 \leq x (t) \land x (t) \leq 1) \land \forall t \in V x (t) < e \land \forall t \in (T ∖ U) 1 - e < x (t))))$
132	131	rspcev	$⊢ (V \in J \land ((Z \in V \land V \subseteq U) \land \forall e \in ℝ^{+} \exists x \in A (\forall t \in T (0 \leq x (t) \land x (t) \leq 1) \land \forall t \in V x (t) < e \land \forall t \in (T ∖ U) 1 - e < x (t)))) \to \exists v \in J ((Z \in v \land v \subseteq U) \land \forall e \in ℝ^{+} \exists x \in A (\forall t \in T (0 \leq x (t) \land x (t) \leq 1) \land \forall t \in v x (t) < e \land \forall t \in (T ∖ U) 1 - e < x (t)))$
133	26 122 132	syl2anc	$⊢ φ \to \exists v \in J ((Z \in v \land v \subseteq U) \land \forall e \in ℝ^{+} \exists x \in A (\forall t \in T (0 \leq x (t) \land x (t) \leq 1) \land \forall t \in v x (t) < e \land \forall t \in (T ∖ U) 1 - e < x (t)))$

Metamath Proof Explorer

Theorem stoweidlem52

Proof