stoweidlem58

Description: This theorem proves Lemma 2 in BrosowskiDeutsh p. 91. Here D is used to represent the set A of Lemma 2, because here the variable A is used for the subalgebra of functions. (Contributed by Glauco Siliprandi, 20-Apr-2017)

	Ref	Expression
Hypotheses	stoweidlem58.1	$⊢ \underline{Ⅎ} t D$
	stoweidlem58.2	$⊢ \underline{Ⅎ} t U$
	stoweidlem58.3	$⊢ Ⅎ t φ$
	stoweidlem58.4	$⊢ K = topGen (ran (.))$
	stoweidlem58.5	$⊢ T = ⋃ J$
	stoweidlem58.6	$⊢ C = J Cn K$
	stoweidlem58.7	$⊢ φ \to J \in Comp$
	stoweidlem58.8	$⊢ φ \to A \subseteq C$
	stoweidlem58.9	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) + g (t)) \in A$
	stoweidlem58.10	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
	stoweidlem58.11	$⊢ (φ \land a \in ℝ) \to (t \in T ⟼ a) \in A$
	stoweidlem58.12	$⊢ (φ \land (r \in T \land t \in T \land r \neq t)) \to \exists q \in A q (r) \neq q (t)$
	stoweidlem58.13	$⊢ φ \to B \in Clsd (J)$
	stoweidlem58.14	$⊢ φ \to D \in Clsd (J)$
	stoweidlem58.15	$⊢ φ \to B \cap D = \emptyset$
	stoweidlem58.16	$⊢ U = T ∖ B$
	stoweidlem58.17	$⊢ φ \to E \in ℝ^{+}$
	stoweidlem58.18	$⊢ φ \to E < \frac{1}{3}$
Assertion	stoweidlem58	$⊢ φ \to \exists x \in A (\forall t \in T (0 \leq x (t) \land x (t) \leq 1) \land \forall t \in D x (t) < E \land \forall t \in B 1 - E < x (t))$

Proof

Step	Hyp	Ref	Expression
1		stoweidlem58.1	$⊢ \underline{Ⅎ} t D$
2		stoweidlem58.2	$⊢ \underline{Ⅎ} t U$
3		stoweidlem58.3	$⊢ Ⅎ t φ$
4		stoweidlem58.4	$⊢ K = topGen (ran (.))$
5		stoweidlem58.5	$⊢ T = ⋃ J$
6		stoweidlem58.6	$⊢ C = J Cn K$
7		stoweidlem58.7	$⊢ φ \to J \in Comp$
8		stoweidlem58.8	$⊢ φ \to A \subseteq C$
9		stoweidlem58.9	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) + g (t)) \in A$
10		stoweidlem58.10	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
11		stoweidlem58.11	$⊢ (φ \land a \in ℝ) \to (t \in T ⟼ a) \in A$
12		stoweidlem58.12	$⊢ (φ \land (r \in T \land t \in T \land r \neq t)) \to \exists q \in A q (r) \neq q (t)$
13		stoweidlem58.13	$⊢ φ \to B \in Clsd (J)$
14		stoweidlem58.14	$⊢ φ \to D \in Clsd (J)$
15		stoweidlem58.15	$⊢ φ \to B \cap D = \emptyset$
16		stoweidlem58.16	$⊢ U = T ∖ B$
17		stoweidlem58.17	$⊢ φ \to E \in ℝ^{+}$
18		stoweidlem58.18	$⊢ φ \to E < \frac{1}{3}$
19	1	nfeq1	$⊢ Ⅎ t D = \emptyset$
20	3 19	nfan	$⊢ Ⅎ t (φ \land D = \emptyset)$
21		eqid	$⊢ (t \in T ⟼ 1) = (t \in T ⟼ 1)$
22	11	adantlr	$⊢ ((φ \land D = \emptyset) \land a \in ℝ) \to (t \in T ⟼ a) \in A$
23	13	adantr	$⊢ (φ \land D = \emptyset) \to B \in Clsd (J)$
24	17	adantr	$⊢ (φ \land D = \emptyset) \to E \in ℝ^{+}$
25		simpr	$⊢ (φ \land D = \emptyset) \to D = \emptyset$
26	1 20 21 5 22 23 24 25	stoweidlem18	$⊢ (φ \land D = \emptyset) \to \exists x \in A (\forall t \in T (0 \leq x (t) \land x (t) \leq 1) \land \forall t \in D x (t) < E \land \forall t \in B 1 - E < x (t))$
27		nfcv	$⊢ \underline{Ⅎ} t \emptyset$
28	1 27	nfne	$⊢ Ⅎ t D \neq \emptyset$
29	3 28	nfan	$⊢ Ⅎ t (φ \land D \neq \emptyset)$
30		eqid	$⊢ \{h \in A \| \forall t \in T (0 \leq h (t) \land h (t) \leq 1)\} = \{h \in A \| \forall t \in T (0 \leq h (t) \land h (t) \leq 1)\}$
31		eqid	$⊢ \{w \in J \| \forall e \in ℝ^{+} \exists h \in A (\forall t \in T (0 \leq h (t) \land h (t) \leq 1) \land \forall t \in w h (t) < e \land \forall t \in (T ∖ U) 1 - e < h (t))\} = \{w \in J \| \forall e \in ℝ^{+} \exists h \in A (\forall t \in T (0 \leq h (t) \land h (t) \leq 1) \land \forall t \in w h (t) < e \land \forall t \in (T ∖ U) 1 - e < h (t))\}$
32	7	adantr	$⊢ (φ \land D \neq \emptyset) \to J \in Comp$
33	8	adantr	$⊢ (φ \land D \neq \emptyset) \to A \subseteq C$
34	9	3adant1r	$⊢ ((φ \land D \neq \emptyset) \land f \in A \land g \in A) \to (t \in T ⟼ f (t) + g (t)) \in A$
35	10	3adant1r	$⊢ ((φ \land D \neq \emptyset) \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
36	11	adantlr	$⊢ ((φ \land D \neq \emptyset) \land a \in ℝ) \to (t \in T ⟼ a) \in A$
37	12	adantlr	$⊢ ((φ \land D \neq \emptyset) \land (r \in T \land t \in T \land r \neq t)) \to \exists q \in A q (r) \neq q (t)$
38	13	adantr	$⊢ (φ \land D \neq \emptyset) \to B \in Clsd (J)$
39	14	adantr	$⊢ (φ \land D \neq \emptyset) \to D \in Clsd (J)$
40	15	adantr	$⊢ (φ \land D \neq \emptyset) \to B \cap D = \emptyset$
41		simpr	$⊢ (φ \land D \neq \emptyset) \to D \neq \emptyset$
42	17	adantr	$⊢ (φ \land D \neq \emptyset) \to E \in ℝ^{+}$
43	18	adantr	$⊢ (φ \land D \neq \emptyset) \to E < \frac{1}{3}$
44	1 2 29 30 31 4 5 6 16 32 33 34 35 36 37 38 39 40 41 42 43	stoweidlem57	$⊢ (φ \land D \neq \emptyset) \to \exists x \in A (\forall t \in T (0 \leq x (t) \land x (t) \leq 1) \land \forall t \in D x (t) < E \land \forall t \in B 1 - E < x (t))$
45	26 44	pm2.61dane	$⊢ φ \to \exists x \in A (\forall t \in T (0 \leq x (t) \land x (t) \leq 1) \land \forall t \in D x (t) < E \land \forall t \in B 1 - E < x (t))$

Metamath Proof Explorer

Theorem stoweidlem58

Proof