stoweidlem39

Description: This lemma is used to prove that there exists a function x as in the proof of Lemma 2 in BrosowskiDeutsh p. 91: assuming that r is a finite subset of W , x indexes a finite set of functions in the subalgebra (of the Stone Weierstrass theorem), such that for all i ranging in the finite indexing set, 0 ≤ x_i ≤ 1, x_i < ε / m on V(t_i), and x_i > 1 - ε / m on B . Here D is used to represent A in the paper's Lemma 2 (because A is used for the subalgebra), M is used to represent m in the paper, E is used to represent ε, and v_i is used to represent V(t_i). W is just a local definition, used to shorten statements. (Contributed by Glauco Siliprandi, 20-Apr-2017)

	Ref	Expression
Hypotheses	stoweidlem39.1	$⊢ Ⅎ h φ$
	stoweidlem39.2	$⊢ Ⅎ t φ$
	stoweidlem39.3	$⊢ Ⅎ w φ$
	stoweidlem39.4	$⊢ U = T ∖ B$
	stoweidlem39.5	$⊢ Y = \{h \in A \| \forall t \in T (0 \leq h (t) \land h (t) \leq 1)\}$
	stoweidlem39.6	$⊢ W = \{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))\}$
	stoweidlem39.7	$⊢ φ \to r \in (𝒫 W \cap Fin)$
	stoweidlem39.8	$⊢ φ \to D \subseteq ⋃ r$
	stoweidlem39.9	$⊢ φ \to D \neq \emptyset$
	stoweidlem39.10	$⊢ φ \to E \in ℝ^{+}$
	stoweidlem39.11	$⊢ φ \to B \subseteq T$
	stoweidlem39.12	$⊢ φ \to W \in V$
	stoweidlem39.13	$⊢ φ \to A \in V$
Assertion	stoweidlem39	$⊢ φ \to \exists m \in ℕ \exists v (v : (1 \dots m) ⟶ W \land D \subseteq ⋃ ran v \land \exists x (x : (1 \dots m) ⟶ Y \land \forall i \in (1 \dots m) (\forall t \in v (i) x (i) (t) < \frac{E}{m} \land \forall t \in B 1 - (\frac{E}{m}) < x (i) (t))))$

Proof

Step	Hyp	Ref	Expression
1		stoweidlem39.1	$⊢ Ⅎ h φ$
2		stoweidlem39.2	$⊢ Ⅎ t φ$
3		stoweidlem39.3	$⊢ Ⅎ w φ$
4		stoweidlem39.4	$⊢ U = T ∖ B$
5		stoweidlem39.5	$⊢ Y = \{h \in A \| \forall t \in T (0 \leq h (t) \land h (t) \leq 1)\}$
6		stoweidlem39.6	$⊢ W = \{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))\}$
7		stoweidlem39.7	$⊢ φ \to r \in (𝒫 W \cap Fin)$
8		stoweidlem39.8	$⊢ φ \to D \subseteq ⋃ r$
9		stoweidlem39.9	$⊢ φ \to D \neq \emptyset$
10		stoweidlem39.10	$⊢ φ \to E \in ℝ^{+}$
11		stoweidlem39.11	$⊢ φ \to B \subseteq T$
12		stoweidlem39.12	$⊢ φ \to W \in V$
13		stoweidlem39.13	$⊢ φ \to A \in V$
14	8 9	jca	$⊢ φ \to (D \subseteq ⋃ r \land D \neq \emptyset)$
15		ssn0	$⊢ (D \subseteq ⋃ r \land D \neq \emptyset) \to ⋃ r \neq \emptyset$
16		unieq	$⊢ r = \emptyset \to ⋃ r = ⋃ \emptyset$
17		uni0	$⊢ ⋃ \emptyset = \emptyset$
18	16 17	eqtrdi	$⊢ r = \emptyset \to ⋃ r = \emptyset$
19	18	necon3i	$⊢ ⋃ r \neq \emptyset \to r \neq \emptyset$
20	14 15 19	3syl	$⊢ φ \to r \neq \emptyset$
21	20	neneqd	$⊢ φ \to \neg r = \emptyset$
22		elinel2	$⊢ r \in (𝒫 W \cap Fin) \to r \in Fin$
23	7 22	syl	$⊢ φ \to r \in Fin$
24		fz1f1o	$⊢ r \in Fin \to (r = \emptyset \lor (\|r\| \in ℕ \land \exists v v : (1 \dots \|r\|) \underset{1-1 onto}{⟶} r))$
25		pm2.53	$⊢ (r = \emptyset \lor (\|r\| \in ℕ \land \exists v v : (1 \dots \|r\|) \underset{1-1 onto}{⟶} r)) \to (\neg r = \emptyset \to (\|r\| \in ℕ \land \exists v v : (1 \dots \|r\|) \underset{1-1 onto}{⟶} r))$
26	23 24 25	3syl	$⊢ φ \to (\neg r = \emptyset \to (\|r\| \in ℕ \land \exists v v : (1 \dots \|r\|) \underset{1-1 onto}{⟶} r))$
27	21 26	mpd	$⊢ φ \to (\|r\| \in ℕ \land \exists v v : (1 \dots \|r\|) \underset{1-1 onto}{⟶} r)$
28		oveq2	$⊢ m = \|r\| \to (1 \dots m) = (1 \dots \|r\|)$
29	28	f1oeq2d	$⊢ m = \|r\| \to (v : (1 \dots m) \underset{1-1 onto}{⟶} r \leftrightarrow v : (1 \dots \|r\|) \underset{1-1 onto}{⟶} r)$
30	29	exbidv	$⊢ m = \|r\| \to (\exists v v : (1 \dots m) \underset{1-1 onto}{⟶} r \leftrightarrow \exists v v : (1 \dots \|r\|) \underset{1-1 onto}{⟶} r)$
31	30	rspcev	$⊢ (\|r\| \in ℕ \land \exists v v : (1 \dots \|r\|) \underset{1-1 onto}{⟶} r) \to \exists m \in ℕ \exists v v : (1 \dots m) \underset{1-1 onto}{⟶} r$
32	27 31	syl	$⊢ φ \to \exists m \in ℕ \exists v v : (1 \dots m) \underset{1-1 onto}{⟶} r$
33		f1of	$⊢ v : (1 \dots m) \underset{1-1 onto}{⟶} r \to v : (1 \dots m) ⟶ r$
34	33	adantl	$⊢ ((φ \land m \in ℕ) \land v : (1 \dots m) \underset{1-1 onto}{⟶} r) \to v : (1 \dots m) ⟶ r$
35		simpll	$⊢ ((φ \land m \in ℕ) \land v : (1 \dots m) \underset{1-1 onto}{⟶} r) \to φ$
36		elinel1	$⊢ r \in (𝒫 W \cap Fin) \to r \in 𝒫 W$
37	36	elpwid	$⊢ r \in (𝒫 W \cap Fin) \to r \subseteq W$
38	35 7 37	3syl	$⊢ ((φ \land m \in ℕ) \land v : (1 \dots m) \underset{1-1 onto}{⟶} r) \to r \subseteq W$
39	34 38	fssd	$⊢ ((φ \land m \in ℕ) \land v : (1 \dots m) \underset{1-1 onto}{⟶} r) \to v : (1 \dots m) ⟶ W$
40	8	ad2antrr	$⊢ ((φ \land m \in ℕ) \land v : (1 \dots m) \underset{1-1 onto}{⟶} r) \to D \subseteq ⋃ r$
41		dff1o2	$⊢ v : (1 \dots m) \underset{1-1 onto}{⟶} r \leftrightarrow (v Fn (1 \dots m) \land Fun v^{-1} \land ran v = r)$
42	41	simp3bi	$⊢ v : (1 \dots m) \underset{1-1 onto}{⟶} r \to ran v = r$
43	42	unieqd	$⊢ v : (1 \dots m) \underset{1-1 onto}{⟶} r \to ⋃ ran v = ⋃ r$
44	43	adantl	$⊢ ((φ \land m \in ℕ) \land v : (1 \dots m) \underset{1-1 onto}{⟶} r) \to ⋃ ran v = ⋃ r$
45	40 44	sseqtrrd	$⊢ ((φ \land m \in ℕ) \land v : (1 \dots m) \underset{1-1 onto}{⟶} r) \to D \subseteq ⋃ ran v$
46		nfv	$⊢ Ⅎ h m \in ℕ$
47	1 46	nfan	$⊢ Ⅎ h (φ \land m \in ℕ)$
48		nfv	$⊢ Ⅎ h v : (1 \dots m) \underset{1-1 onto}{⟶} r$
49	47 48	nfan	$⊢ Ⅎ h ((φ \land m \in ℕ) \land v : (1 \dots m) \underset{1-1 onto}{⟶} r)$
50		nfv	$⊢ Ⅎ t m \in ℕ$
51	2 50	nfan	$⊢ Ⅎ t (φ \land m \in ℕ)$
52		nfv	$⊢ Ⅎ t v : (1 \dots m) \underset{1-1 onto}{⟶} r$
53	51 52	nfan	$⊢ Ⅎ t ((φ \land m \in ℕ) \land v : (1 \dots m) \underset{1-1 onto}{⟶} r)$
54		nfv	$⊢ Ⅎ w m \in ℕ$
55	3 54	nfan	$⊢ Ⅎ w (φ \land m \in ℕ)$
56		nfv	$⊢ Ⅎ w v : (1 \dots m) \underset{1-1 onto}{⟶} r$
57	55 56	nfan	$⊢ Ⅎ w ((φ \land m \in ℕ) \land v : (1 \dots m) \underset{1-1 onto}{⟶} r)$
58		eqid	$⊢ (w \in r ⟼ \{h \in A \| (\forall t \in T (0 \leq h (t) \land h (t) \leq 1) \land \forall t \in w h (t) < \frac{E}{m} \land \forall t \in (T ∖ U) 1 - (\frac{E}{m}) < h (t))\}) = (w \in r ⟼ \{h \in A \| (\forall t \in T (0 \leq h (t) \land h (t) \leq 1) \land \forall t \in w h (t) < \frac{E}{m} \land \forall t \in (T ∖ U) 1 - (\frac{E}{m}) < h (t))\})$
59		simplr	$⊢ ((φ \land m \in ℕ) \land v : (1 \dots m) \underset{1-1 onto}{⟶} r) \to m \in ℕ$
60		simpr	$⊢ ((φ \land m \in ℕ) \land v : (1 \dots m) \underset{1-1 onto}{⟶} r) \to v : (1 \dots m) \underset{1-1 onto}{⟶} r$
61	10	ad2antrr	$⊢ ((φ \land m \in ℕ) \land v : (1 \dots m) \underset{1-1 onto}{⟶} r) \to E \in ℝ^{+}$
62	11	sselda	$⊢ (φ \land b \in B) \to b \in T$
63		notnot	$⊢ b \in B \to \neg \neg b \in B$
64	63	intnand	$⊢ b \in B \to \neg (b \in T \land \neg b \in B)$
65	64	adantl	$⊢ (φ \land b \in B) \to \neg (b \in T \land \neg b \in B)$
66		eldif	$⊢ b \in (T ∖ B) \leftrightarrow (b \in T \land \neg b \in B)$
67	65 66	sylnibr	$⊢ (φ \land b \in B) \to \neg b \in (T ∖ B)$
68	4	eleq2i	$⊢ b \in U \leftrightarrow b \in (T ∖ B)$
69	67 68	sylnibr	$⊢ (φ \land b \in B) \to \neg b \in U$
70	62 69	eldifd	$⊢ (φ \land b \in B) \to b \in (T ∖ U)$
71	70	ralrimiva	$⊢ φ \to \forall b \in B b \in (T ∖ U)$
72		dfss3	$⊢ B \subseteq T ∖ U \leftrightarrow \forall b \in B b \in (T ∖ U)$
73	71 72	sylibr	$⊢ φ \to B \subseteq T ∖ U$
74	73	ad2antrr	$⊢ ((φ \land m \in ℕ) \land v : (1 \dots m) \underset{1-1 onto}{⟶} r) \to B \subseteq T ∖ U$
75	12	ad2antrr	$⊢ ((φ \land m \in ℕ) \land v : (1 \dots m) \underset{1-1 onto}{⟶} r) \to W \in V$
76	13	ad2antrr	$⊢ ((φ \land m \in ℕ) \land v : (1 \dots m) \underset{1-1 onto}{⟶} r) \to A \in V$
77	23	ad2antrr	$⊢ ((φ \land m \in ℕ) \land v : (1 \dots m) \underset{1-1 onto}{⟶} r) \to r \in Fin$
78		mptfi	$⊢ r \in Fin \to (w \in r ⟼ \{h \in A \| (\forall t \in T (0 \leq h (t) \land h (t) \leq 1) \land \forall t \in w h (t) < \frac{E}{m} \land \forall t \in (T ∖ U) 1 - (\frac{E}{m}) < h (t))\}) \in Fin$
79		rnfi	$⊢ (w \in r ⟼ \{h \in A \| (\forall t \in T (0 \leq h (t) \land h (t) \leq 1) \land \forall t \in w h (t) < \frac{E}{m} \land \forall t \in (T ∖ U) 1 - (\frac{E}{m}) < h (t))\}) \in Fin \to ran (w \in r ⟼ \{h \in A \| (\forall t \in T (0 \leq h (t) \land h (t) \leq 1) \land \forall t \in w h (t) < \frac{E}{m} \land \forall t \in (T ∖ U) 1 - (\frac{E}{m}) < h (t))\}) \in Fin$
80	77 78 79	3syl	$⊢ ((φ \land m \in ℕ) \land v : (1 \dots m) \underset{1-1 onto}{⟶} r) \to ran (w \in r ⟼ \{h \in A \| (\forall t \in T (0 \leq h (t) \land h (t) \leq 1) \land \forall t \in w h (t) < \frac{E}{m} \land \forall t \in (T ∖ U) 1 - (\frac{E}{m}) < h (t))\}) \in Fin$
81	49 53 57 5 6 58 38 59 60 61 74 75 76 80	stoweidlem31	$⊢ ((φ \land m \in ℕ) \land v : (1 \dots m) \underset{1-1 onto}{⟶} r) \to \exists x (x : (1 \dots m) ⟶ Y \land \forall i \in (1 \dots m) (\forall t \in v (i) x (i) (t) < \frac{E}{m} \land \forall t \in B 1 - (\frac{E}{m}) < x (i) (t)))$
82	39 45 81	3jca	$⊢ ((φ \land m \in ℕ) \land v : (1 \dots m) \underset{1-1 onto}{⟶} r) \to (v : (1 \dots m) ⟶ W \land D \subseteq ⋃ ran v \land \exists x (x : (1 \dots m) ⟶ Y \land \forall i \in (1 \dots m) (\forall t \in v (i) x (i) (t) < \frac{E}{m} \land \forall t \in B 1 - (\frac{E}{m}) < x (i) (t))))$
83	82	ex	$⊢ (φ \land m \in ℕ) \to (v : (1 \dots m) \underset{1-1 onto}{⟶} r \to (v : (1 \dots m) ⟶ W \land D \subseteq ⋃ ran v \land \exists x (x : (1 \dots m) ⟶ Y \land \forall i \in (1 \dots m) (\forall t \in v (i) x (i) (t) < \frac{E}{m} \land \forall t \in B 1 - (\frac{E}{m}) < x (i) (t)))))$
84	83	eximdv	$⊢ (φ \land m \in ℕ) \to (\exists v v : (1 \dots m) \underset{1-1 onto}{⟶} r \to \exists v (v : (1 \dots m) ⟶ W \land D \subseteq ⋃ ran v \land \exists x (x : (1 \dots m) ⟶ Y \land \forall i \in (1 \dots m) (\forall t \in v (i) x (i) (t) < \frac{E}{m} \land \forall t \in B 1 - (\frac{E}{m}) < x (i) (t)))))$
85	84	reximdva	$⊢ φ \to (\exists m \in ℕ \exists v v : (1 \dots m) \underset{1-1 onto}{⟶} r \to \exists m \in ℕ \exists v (v : (1 \dots m) ⟶ W \land D \subseteq ⋃ ran v \land \exists x (x : (1 \dots m) ⟶ Y \land \forall i \in (1 \dots m) (\forall t \in v (i) x (i) (t) < \frac{E}{m} \land \forall t \in B 1 - (\frac{E}{m}) < x (i) (t)))))$
86	32 85	mpd	$⊢ φ \to \exists m \in ℕ \exists v (v : (1 \dots m) ⟶ W \land D \subseteq ⋃ ran v \land \exists x (x : (1 \dots m) ⟶ Y \land \forall i \in (1 \dots m) (\forall t \in v (i) x (i) (t) < \frac{E}{m} \land \forall t \in B 1 - (\frac{E}{m}) < x (i) (t))))$

Metamath Proof Explorer

Theorem stoweidlem39

Proof