Metamath Proof Explorer

Theorem stoweidlem54

Description: There exists a function x as in the proof of Lemma 2 in BrosowskiDeutsh p. 91. Here D is used to represent A in the paper, because here A is used for the subalgebra of functions. E is used to represent ε in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem54.1 ⊢ Ⅎ i φ
stoweidlem54.2 ⊢ Ⅎ t φ
stoweidlem54.3 ⊢ Ⅎ y φ
stoweidlem54.4 ⊢ Ⅎ w φ
stoweidlem54.5 ⊢ T = ⋃ J
stoweidlem54.6 ⊢ Y = h ∈ A | ∀ t ∈ T 0 ≤ h ⁡ t ∧ h ⁡ t ≤ 1
stoweidlem54.7 ⊢ P = f ∈ Y , g ∈ Y ⟼ t ∈ T ⟼ f ⁡ t ⁢ g ⁡ t
stoweidlem54.8 ⊢ F = t ∈ T ⟼ i ∈ 1 … M ⟼ y ⁡ i ⁡ t
stoweidlem54.9 ⊢ Z = t ∈ T ⟼ seq 1 × F ⁡ t ⁡ M
stoweidlem54.10 ⊢ V = w ∈ J | ∀ e ∈ ℝ + ∃ h ∈ A ∀ t ∈ T 0 ≤ h ⁡ t ∧ h ⁡ t ≤ 1 ∧ ∀ t ∈ w h ⁡ t < e ∧ ∀ t ∈ T ∖ U 1 − e < h ⁡ t
stoweidlem54.11 ⊢ φ ∧ f ∈ A ∧ g ∈ A → t ∈ T ⟼ f ⁡ t ⁢ g ⁡ t ∈ A
stoweidlem54.12 ⊢ φ ∧ f ∈ A → f : T ⟶ ℝ
stoweidlem54.13 ⊢ φ → M ∈ ℕ
stoweidlem54.14 ⊢ φ → W : 1 … M ⟶ V
stoweidlem54.15 ⊢ φ → B ⊆ T
stoweidlem54.16 ⊢ φ → D ⊆ ⋃ ran ⁡ W
stoweidlem54.17 ⊢ φ → D ⊆ T
stoweidlem54.18 ⊢ φ → ∃ y y : 1 … M ⟶ Y ∧ ∀ i ∈ 1 … M ∀ t ∈ W ⁡ i y ⁡ i ⁡ t < E M ∧ ∀ t ∈ B 1 − E M < y ⁡ i ⁡ t
stoweidlem54.19 ⊢ φ → T ∈ V
stoweidlem54.20 ⊢ φ → E ∈ ℝ +
stoweidlem54.21 ⊢ φ → E < 1 3
Assertion stoweidlem54 ⊢ φ → ∃ x ∈ A ∀ t ∈ T 0 ≤ x ⁡ t ∧ x ⁡ t ≤ 1 ∧ ∀ t ∈ D x ⁡ t < E ∧ ∀ t ∈ B 1 − E < x ⁡ t

Proof

Step Hyp Ref Expression
1 stoweidlem54.1 ⊢ Ⅎ i φ
2 stoweidlem54.2 ⊢ Ⅎ t φ
3 stoweidlem54.3 ⊢ Ⅎ y φ
4 stoweidlem54.4 ⊢ Ⅎ w φ
5 stoweidlem54.5 ⊢ T = ⋃ J
6 stoweidlem54.6 ⊢ Y = h ∈ A | ∀ t ∈ T 0 ≤ h ⁡ t ∧ h ⁡ t ≤ 1
7 stoweidlem54.7 ⊢ P = f ∈ Y , g ∈ Y ⟼ t ∈ T ⟼ f ⁡ t ⁢ g ⁡ t
8 stoweidlem54.8 ⊢ F = t ∈ T ⟼ i ∈ 1 … M ⟼ y ⁡ i ⁡ t
9 stoweidlem54.9 ⊢ Z = t ∈ T ⟼ seq 1 × F ⁡ t ⁡ M
10 stoweidlem54.10 ⊢ V = w ∈ J | ∀ e ∈ ℝ + ∃ h ∈ A ∀ t ∈ T 0 ≤ h ⁡ t ∧ h ⁡ t ≤ 1 ∧ ∀ t ∈ w h ⁡ t < e ∧ ∀ t ∈ T ∖ U 1 − e < h ⁡ t
11 stoweidlem54.11 ⊢ φ ∧ f ∈ A ∧ g ∈ A → t ∈ T ⟼ f ⁡ t ⁢ g ⁡ t ∈ A
12 stoweidlem54.12 ⊢ φ ∧ f ∈ A → f : T ⟶ ℝ
13 stoweidlem54.13 ⊢ φ → M ∈ ℕ
14 stoweidlem54.14 ⊢ φ → W : 1 … M ⟶ V
15 stoweidlem54.15 ⊢ φ → B ⊆ T
16 stoweidlem54.16 ⊢ φ → D ⊆ ⋃ ran ⁡ W
17 stoweidlem54.17 ⊢ φ → D ⊆ T
18 stoweidlem54.18 ⊢ φ → ∃ y y : 1 … M ⟶ Y ∧ ∀ i ∈ 1 … M ∀ t ∈ W ⁡ i y ⁡ i ⁡ t < E M ∧ ∀ t ∈ B 1 − E M < y ⁡ i ⁡ t
19 stoweidlem54.19 ⊢ φ → T ∈ V
20 stoweidlem54.20 ⊢ φ → E ∈ ℝ +
21 stoweidlem54.21 ⊢ φ → E < 1 3
22 nfv ⊢ Ⅎ y ∃ x x ∈ A ∧ ∀ t ∈ T 0 ≤ x ⁡ t ∧ x ⁡ t ≤ 1 ∧ ∀ t ∈ D x ⁡ t < E ∧ ∀ t ∈ B 1 − E < x ⁡ t
23 nfv ⊢ Ⅎ i y : 1 … M ⟶ Y
24 nfra1 ⊢ Ⅎ i ∀ i ∈ 1 … M ∀ t ∈ W ⁡ i y ⁡ i ⁡ t < E M ∧ ∀ t ∈ B 1 − E M < y ⁡ i ⁡ t
25 23 24 nfan ⊢ Ⅎ i y : 1 … M ⟶ Y ∧ ∀ i ∈ 1 … M ∀ t ∈ W ⁡ i y ⁡ i ⁡ t < E M ∧ ∀ t ∈ B 1 − E M < y ⁡ i ⁡ t
26 1 25 nfan ⊢ Ⅎ i φ ∧ y : 1 … M ⟶ Y ∧ ∀ i ∈ 1 … M ∀ t ∈ W ⁡ i y ⁡ i ⁡ t < E M ∧ ∀ t ∈ B 1 − E M < y ⁡ i ⁡ t
27 nfcv ⊢ Ⅎ _ t y
28 nfcv ⊢ Ⅎ _ t 1 … M
29 nfra1 ⊢ Ⅎ t ∀ t ∈ T 0 ≤ h ⁡ t ∧ h ⁡ t ≤ 1
30 nfcv ⊢ Ⅎ _ t A
31 29 30 nfrabw ⊢ Ⅎ _ t h ∈ A | ∀ t ∈ T 0 ≤ h ⁡ t ∧ h ⁡ t ≤ 1
32 6 31 nfcxfr ⊢ Ⅎ _ t Y
33 27 28 32 nff ⊢ Ⅎ t y : 1 … M ⟶ Y
34 nfra1 ⊢ Ⅎ t ∀ t ∈ W ⁡ i y ⁡ i ⁡ t < E M
35 nfra1 ⊢ Ⅎ t ∀ t ∈ B 1 − E M < y ⁡ i ⁡ t
36 34 35 nfan ⊢ Ⅎ t ∀ t ∈ W ⁡ i y ⁡ i ⁡ t < E M ∧ ∀ t ∈ B 1 − E M < y ⁡ i ⁡ t
37 28 36 nfralw ⊢ Ⅎ t ∀ i ∈ 1 … M ∀ t ∈ W ⁡ i y ⁡ i ⁡ t < E M ∧ ∀ t ∈ B 1 − E M < y ⁡ i ⁡ t
38 33 37 nfan ⊢ Ⅎ t y : 1 … M ⟶ Y ∧ ∀ i ∈ 1 … M ∀ t ∈ W ⁡ i y ⁡ i ⁡ t < E M ∧ ∀ t ∈ B 1 − E M < y ⁡ i ⁡ t
39 2 38 nfan ⊢ Ⅎ t φ ∧ y : 1 … M ⟶ Y ∧ ∀ i ∈ 1 … M ∀ t ∈ W ⁡ i y ⁡ i ⁡ t < E M ∧ ∀ t ∈ B 1 − E M < y ⁡ i ⁡ t
40 nfv ⊢ Ⅎ w y : 1 … M ⟶ Y ∧ ∀ i ∈ 1 … M ∀ t ∈ W ⁡ i y ⁡ i ⁡ t < E M ∧ ∀ t ∈ B 1 − E M < y ⁡ i ⁡ t
41 4 40 nfan ⊢ Ⅎ w φ ∧ y : 1 … M ⟶ Y ∧ ∀ i ∈ 1 … M ∀ t ∈ W ⁡ i y ⁡ i ⁡ t < E M ∧ ∀ t ∈ B 1 − E M < y ⁡ i ⁡ t
42 nfrab1 ⊢ Ⅎ _ w w ∈ J | ∀ e ∈ ℝ + ∃ h ∈ A ∀ t ∈ T 0 ≤ h ⁡ t ∧ h ⁡ t ≤ 1 ∧ ∀ t ∈ w h ⁡ t < e ∧ ∀ t ∈ T ∖ U 1 − e < h ⁡ t
43 10 42 nfcxfr ⊢ Ⅎ _ w V
44 eqid ⊢ seq 1 P y ⁡ M = seq 1 P y ⁡ M
45 13 adantr ⊢ φ ∧ y : 1 … M ⟶ Y ∧ ∀ i ∈ 1 … M ∀ t ∈ W ⁡ i y ⁡ i ⁡ t < E M ∧ ∀ t ∈ B 1 − E M < y ⁡ i ⁡ t → M ∈ ℕ
46 14 adantr ⊢ φ ∧ y : 1 … M ⟶ Y ∧ ∀ i ∈ 1 … M ∀ t ∈ W ⁡ i y ⁡ i ⁡ t < E M ∧ ∀ t ∈ B 1 − E M < y ⁡ i ⁡ t → W : 1 … M ⟶ V
47 simprl ⊢ φ ∧ y : 1 … M ⟶ Y ∧ ∀ i ∈ 1 … M ∀ t ∈ W ⁡ i y ⁡ i ⁡ t < E M ∧ ∀ t ∈ B 1 − E M < y ⁡ i ⁡ t → y : 1 … M ⟶ Y
48 simpr ⊢ φ ∧ y : 1 … M ⟶ Y ∧ ∀ i ∈ 1 … M ∀ t ∈ W ⁡ i y ⁡ i ⁡ t < E M ∧ ∀ t ∈ B 1 − E M < y ⁡ i ⁡ t ∧ w ∈ V → w ∈ V
49 10 rabeq2i ⊢ w ∈ V ↔ w ∈ J ∧ ∀ e ∈ ℝ + ∃ h ∈ A ∀ t ∈ T 0 ≤ h ⁡ t ∧ h ⁡ t ≤ 1 ∧ ∀ t ∈ w h ⁡ t < e ∧ ∀ t ∈ T ∖ U 1 − e < h ⁡ t
50 49 simplbi ⊢ w ∈ V → w ∈ J
51 elssuni ⊢ w ∈ J → w ⊆ ⋃ J
52 51 5 sseqtrrdi ⊢ w ∈ J → w ⊆ T
53 48 50 52 3syl ⊢ φ ∧ y : 1 … M ⟶ Y ∧ ∀ i ∈ 1 … M ∀ t ∈ W ⁡ i y ⁡ i ⁡ t < E M ∧ ∀ t ∈ B 1 − E M < y ⁡ i ⁡ t ∧ w ∈ V → w ⊆ T
54 16 adantr ⊢ φ ∧ y : 1 … M ⟶ Y ∧ ∀ i ∈ 1 … M ∀ t ∈ W ⁡ i y ⁡ i ⁡ t < E M ∧ ∀ t ∈ B 1 − E M < y ⁡ i ⁡ t → D ⊆ ⋃ ran ⁡ W
55 17 adantr ⊢ φ ∧ y : 1 … M ⟶ Y ∧ ∀ i ∈ 1 … M ∀ t ∈ W ⁡ i y ⁡ i ⁡ t < E M ∧ ∀ t ∈ B 1 − E M < y ⁡ i ⁡ t → D ⊆ T
56 15 adantr ⊢ φ ∧ y : 1 … M ⟶ Y ∧ ∀ i ∈ 1 … M ∀ t ∈ W ⁡ i y ⁡ i ⁡ t < E M ∧ ∀ t ∈ B 1 − E M < y ⁡ i ⁡ t → B ⊆ T
57 r19.26 ⊢ ∀ i ∈ 1 … M ∀ t ∈ W ⁡ i y ⁡ i ⁡ t < E M ∧ ∀ t ∈ B 1 − E M < y ⁡ i ⁡ t ↔ ∀ i ∈ 1 … M ∀ t ∈ W ⁡ i y ⁡ i ⁡ t < E M ∧ ∀ i ∈ 1 … M ∀ t ∈ B 1 − E M < y ⁡ i ⁡ t
58 57 simplbi ⊢ ∀ i ∈ 1 … M ∀ t ∈ W ⁡ i y ⁡ i ⁡ t < E M ∧ ∀ t ∈ B 1 − E M < y ⁡ i ⁡ t → ∀ i ∈ 1 … M ∀ t ∈ W ⁡ i y ⁡ i ⁡ t < E M
59 58 ad2antll ⊢ φ ∧ y : 1 … M ⟶ Y ∧ ∀ i ∈ 1 … M ∀ t ∈ W ⁡ i y ⁡ i ⁡ t < E M ∧ ∀ t ∈ B 1 − E M < y ⁡ i ⁡ t → ∀ i ∈ 1 … M ∀ t ∈ W ⁡ i y ⁡ i ⁡ t < E M
60 59 r19.21bi ⊢ φ ∧ y : 1 … M ⟶ Y ∧ ∀ i ∈ 1 … M ∀ t ∈ W ⁡ i y ⁡ i ⁡ t < E M ∧ ∀ t ∈ B 1 − E M < y ⁡ i ⁡ t ∧ i ∈ 1 … M → ∀ t ∈ W ⁡ i y ⁡ i ⁡ t < E M
61 57 simprbi ⊢ ∀ i ∈ 1 … M ∀ t ∈ W ⁡ i y ⁡ i ⁡ t < E M ∧ ∀ t ∈ B 1 − E M < y ⁡ i ⁡ t → ∀ i ∈ 1 … M ∀ t ∈ B 1 − E M < y ⁡ i ⁡ t
62 61 ad2antll ⊢ φ ∧ y : 1 … M ⟶ Y ∧ ∀ i ∈ 1 … M ∀ t ∈ W ⁡ i y ⁡ i ⁡ t < E M ∧ ∀ t ∈ B 1 − E M < y ⁡ i ⁡ t → ∀ i ∈ 1 … M ∀ t ∈ B 1 − E M < y ⁡ i ⁡ t
63 62 r19.21bi ⊢ φ ∧ y : 1 … M ⟶ Y ∧ ∀ i ∈ 1 … M ∀ t ∈ W ⁡ i y ⁡ i ⁡ t < E M ∧ ∀ t ∈ B 1 − E M < y ⁡ i ⁡ t ∧ i ∈ 1 … M → ∀ t ∈ B 1 − E M < y ⁡ i ⁡ t
64 11 3adant1r ⊢ φ ∧ y : 1 … M ⟶ Y ∧ ∀ i ∈ 1 … M ∀ t ∈ W ⁡ i y ⁡ i ⁡ t < E M ∧ ∀ t ∈ B 1 − E M < y ⁡ i ⁡ t ∧ f ∈ A ∧ g ∈ A → t ∈ T ⟼ f ⁡ t ⁢ g ⁡ t ∈ A
65 12 adantlr ⊢ φ ∧ y : 1 … M ⟶ Y ∧ ∀ i ∈ 1 … M ∀ t ∈ W ⁡ i y ⁡ i ⁡ t < E M ∧ ∀ t ∈ B 1 − E M < y ⁡ i ⁡ t ∧ f ∈ A → f : T ⟶ ℝ
66 19 adantr ⊢ φ ∧ y : 1 … M ⟶ Y ∧ ∀ i ∈ 1 … M ∀ t ∈ W ⁡ i y ⁡ i ⁡ t < E M ∧ ∀ t ∈ B 1 − E M < y ⁡ i ⁡ t → T ∈ V
67 20 adantr ⊢ φ ∧ y : 1 … M ⟶ Y ∧ ∀ i ∈ 1 … M ∀ t ∈ W ⁡ i y ⁡ i ⁡ t < E M ∧ ∀ t ∈ B 1 − E M < y ⁡ i ⁡ t → E ∈ ℝ +
68 21 adantr ⊢ φ ∧ y : 1 … M ⟶ Y ∧ ∀ i ∈ 1 … M ∀ t ∈ W ⁡ i y ⁡ i ⁡ t < E M ∧ ∀ t ∈ B 1 − E M < y ⁡ i ⁡ t → E < 1 3
69 26 39 41 43 6 7 44 8 9 45 46 47 53 54 55 56 60 63 64 65 66 67 68 stoweidlem51 ⊢ φ ∧ y : 1 … M ⟶ Y ∧ ∀ i ∈ 1 … M ∀ t ∈ W ⁡ i y ⁡ i ⁡ t < E M ∧ ∀ t ∈ B 1 − E M < y ⁡ i ⁡ t → ∃ x x ∈ A ∧ ∀ t ∈ T 0 ≤ x ⁡ t ∧ x ⁡ t ≤ 1 ∧ ∀ t ∈ D x ⁡ t < E ∧ ∀ t ∈ B 1 − E < x ⁡ t
70 3 22 18 69 exlimdd ⊢ φ → ∃ x x ∈ A ∧ ∀ t ∈ T 0 ≤ x ⁡ t ∧ x ⁡ t ≤ 1 ∧ ∀ t ∈ D x ⁡ t < E ∧ ∀ t ∈ B 1 − E < x ⁡ t
71 df-rex ⊢ ∃ x ∈ A ∀ t ∈ T 0 ≤ x ⁡ t ∧ x ⁡ t ≤ 1 ∧ ∀ t ∈ D x ⁡ t < E ∧ ∀ t ∈ B 1 − E < x ⁡ t ↔ ∃ x x ∈ A ∧ ∀ t ∈ T 0 ≤ x ⁡ t ∧ x ⁡ t ≤ 1 ∧ ∀ t ∈ D x ⁡ t < E ∧ ∀ t ∈ B 1 − E < x ⁡ t
72 70 71 sylibr ⊢ φ → ∃ x ∈ A ∀ t ∈ T 0 ≤ x ⁡ t ∧ x ⁡ t ≤ 1 ∧ ∀ t ∈ D x ⁡ t < E ∧ ∀ t ∈ B 1 − E < x ⁡ t