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∈T0≤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⟼seq1×F⁡t⁡M
stoweidlem54.10 ⊢V=w∈J|∀e∈ℝ+∃h∈A∀t∈T0≤h⁡t∧h⁡t≤1∧∀t∈wh⁡t<e∧∀t∈T∖U1−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 ⊢φ→∃yy:1…M⟶Y∧∀i∈1…M∀t∈W⁡iy⁡i⁡t<EM∧∀t∈B1−EM<y⁡i⁡t
stoweidlem54.19 ⊢φ→T∈V
stoweidlem54.20 ⊢φ→E∈ℝ+
stoweidlem54.21 ⊢φ→E<13
Assertion stoweidlem54 ⊢φ→∃x∈A∀t∈T0≤x⁡t∧x⁡t≤1∧∀t∈Dx⁡t<E∧∀t∈B1−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∈T0≤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⟼seq1×F⁡t⁡M
10 stoweidlem54.10 ⊢V=w∈J|∀e∈ℝ+∃h∈A∀t∈T0≤h⁡t∧h⁡t≤1∧∀t∈wh⁡t<e∧∀t∈T∖U1−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 ⊢φ→∃yy:1…M⟶Y∧∀i∈1…M∀t∈W⁡iy⁡i⁡t<EM∧∀t∈B1−EM<y⁡i⁡t
19 stoweidlem54.19 ⊢φ→T∈V
20 stoweidlem54.20 ⊢φ→E∈ℝ+
21 stoweidlem54.21 ⊢φ→E<13
22 nfv ⊢Ⅎy∃xx∈A∧∀t∈T0≤x⁡t∧x⁡t≤1∧∀t∈Dx⁡t<E∧∀t∈B1−E<x⁡t
23 nfv ⊢Ⅎiy:1…M⟶Y
24 nfra1 ⊢Ⅎi∀i∈1…M∀t∈W⁡iy⁡i⁡t<EM∧∀t∈B1−EM<y⁡i⁡t
25 23 24 nfan ⊢Ⅎiy:1…M⟶Y∧∀i∈1…M∀t∈W⁡iy⁡i⁡t<EM∧∀t∈B1−EM<y⁡i⁡t
26 1 25 nfan ⊢Ⅎiφ∧y:1…M⟶Y∧∀i∈1…M∀t∈W⁡iy⁡i⁡t<EM∧∀t∈B1−EM<y⁡i⁡t
27 nfcv ⊢Ⅎ_ty
28 nfcv ⊢Ⅎ_t1…M
29 nfra1 ⊢Ⅎt∀t∈T0≤h⁡t∧h⁡t≤1
30 nfcv ⊢Ⅎ_tA
31 29 30 nfrabw ⊢Ⅎ_th∈A|∀t∈T0≤h⁡t∧h⁡t≤1
32 6 31 nfcxfr ⊢Ⅎ_tY
33 27 28 32 nff ⊢Ⅎty:1…M⟶Y
34 nfra1 ⊢Ⅎt∀t∈W⁡iy⁡i⁡t<EM
35 nfra1 ⊢Ⅎt∀t∈B1−EM<y⁡i⁡t
36 34 35 nfan ⊢Ⅎt∀t∈W⁡iy⁡i⁡t<EM∧∀t∈B1−EM<y⁡i⁡t
37 28 36 nfralw ⊢Ⅎt∀i∈1…M∀t∈W⁡iy⁡i⁡t<EM∧∀t∈B1−EM<y⁡i⁡t
38 33 37 nfan ⊢Ⅎty:1…M⟶Y∧∀i∈1…M∀t∈W⁡iy⁡i⁡t<EM∧∀t∈B1−EM<y⁡i⁡t
39 2 38 nfan ⊢Ⅎtφ∧y:1…M⟶Y∧∀i∈1…M∀t∈W⁡iy⁡i⁡t<EM∧∀t∈B1−EM<y⁡i⁡t
40 nfv ⊢Ⅎwy:1…M⟶Y∧∀i∈1…M∀t∈W⁡iy⁡i⁡t<EM∧∀t∈B1−EM<y⁡i⁡t
41 4 40 nfan ⊢Ⅎwφ∧y:1…M⟶Y∧∀i∈1…M∀t∈W⁡iy⁡i⁡t<EM∧∀t∈B1−EM<y⁡i⁡t
42 nfrab1 ⊢Ⅎ_ww∈J|∀e∈ℝ+∃h∈A∀t∈T0≤h⁡t∧h⁡t≤1∧∀t∈wh⁡t<e∧∀t∈T∖U1−e<h⁡t
43 10 42 nfcxfr ⊢Ⅎ_wV
44 eqid ⊢seq1Py⁡M=seq1Py⁡M
45 13 adantr ⊢φ∧y:1…M⟶Y∧∀i∈1…M∀t∈W⁡iy⁡i⁡t<EM∧∀t∈B1−EM<y⁡i⁡t→M∈ℕ
46 14 adantr ⊢φ∧y:1…M⟶Y∧∀i∈1…M∀t∈W⁡iy⁡i⁡t<EM∧∀t∈B1−EM<y⁡i⁡t→W:1…M⟶V
47 simprl ⊢φ∧y:1…M⟶Y∧∀i∈1…M∀t∈W⁡iy⁡i⁡t<EM∧∀t∈B1−EM<y⁡i⁡t→y:1…M⟶Y
48 simpr ⊢φ∧y:1…M⟶Y∧∀i∈1…M∀t∈W⁡iy⁡i⁡t<EM∧∀t∈B1−EM<y⁡i⁡t∧w∈V→w∈V
49 10 reqabi ⊢w∈V↔w∈J∧∀e∈ℝ+∃h∈A∀t∈T0≤h⁡t∧h⁡t≤1∧∀t∈wh⁡t<e∧∀t∈T∖U1−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⁡iy⁡i⁡t<EM∧∀t∈B1−EM<y⁡i⁡t∧w∈V→w⊆T
54 16 adantr ⊢φ∧y:1…M⟶Y∧∀i∈1…M∀t∈W⁡iy⁡i⁡t<EM∧∀t∈B1−EM<y⁡i⁡t→D⊆⋃ran⁡W
55 17 adantr ⊢φ∧y:1…M⟶Y∧∀i∈1…M∀t∈W⁡iy⁡i⁡t<EM∧∀t∈B1−EM<y⁡i⁡t→D⊆T
56 15 adantr ⊢φ∧y:1…M⟶Y∧∀i∈1…M∀t∈W⁡iy⁡i⁡t<EM∧∀t∈B1−EM<y⁡i⁡t→B⊆T
57 r19.26 ⊢∀i∈1…M∀t∈W⁡iy⁡i⁡t<EM∧∀t∈B1−EM<y⁡i⁡t↔∀i∈1…M∀t∈W⁡iy⁡i⁡t<EM∧∀i∈1…M∀t∈B1−EM<y⁡i⁡t
58 57 simplbi ⊢∀i∈1…M∀t∈W⁡iy⁡i⁡t<EM∧∀t∈B1−EM<y⁡i⁡t→∀i∈1…M∀t∈W⁡iy⁡i⁡t<EM
59 58 ad2antll ⊢φ∧y:1…M⟶Y∧∀i∈1…M∀t∈W⁡iy⁡i⁡t<EM∧∀t∈B1−EM<y⁡i⁡t→∀i∈1…M∀t∈W⁡iy⁡i⁡t<EM
60 59 r19.21bi ⊢φ∧y:1…M⟶Y∧∀i∈1…M∀t∈W⁡iy⁡i⁡t<EM∧∀t∈B1−EM<y⁡i⁡t∧i∈1…M→∀t∈W⁡iy⁡i⁡t<EM
61 57 simprbi ⊢∀i∈1…M∀t∈W⁡iy⁡i⁡t<EM∧∀t∈B1−EM<y⁡i⁡t→∀i∈1…M∀t∈B1−EM<y⁡i⁡t
62 61 ad2antll ⊢φ∧y:1…M⟶Y∧∀i∈1…M∀t∈W⁡iy⁡i⁡t<EM∧∀t∈B1−EM<y⁡i⁡t→∀i∈1…M∀t∈B1−EM<y⁡i⁡t
63 62 r19.21bi ⊢φ∧y:1…M⟶Y∧∀i∈1…M∀t∈W⁡iy⁡i⁡t<EM∧∀t∈B1−EM<y⁡i⁡t∧i∈1…M→∀t∈B1−EM<y⁡i⁡t
64 11 3adant1r ⊢φ∧y:1…M⟶Y∧∀i∈1…M∀t∈W⁡iy⁡i⁡t<EM∧∀t∈B1−EM<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⁡iy⁡i⁡t<EM∧∀t∈B1−EM<y⁡i⁡t∧f∈A→f:T⟶ℝ
66 19 adantr ⊢φ∧y:1…M⟶Y∧∀i∈1…M∀t∈W⁡iy⁡i⁡t<EM∧∀t∈B1−EM<y⁡i⁡t→T∈V
67 20 adantr ⊢φ∧y:1…M⟶Y∧∀i∈1…M∀t∈W⁡iy⁡i⁡t<EM∧∀t∈B1−EM<y⁡i⁡t→E∈ℝ+
68 21 adantr ⊢φ∧y:1…M⟶Y∧∀i∈1…M∀t∈W⁡iy⁡i⁡t<EM∧∀t∈B1−EM<y⁡i⁡t→E<13
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⁡iy⁡i⁡t<EM∧∀t∈B1−EM<y⁡i⁡t→∃xx∈A∧∀t∈T0≤x⁡t∧x⁡t≤1∧∀t∈Dx⁡t<E∧∀t∈B1−E<x⁡t
70 3 22 18 69 exlimdd ⊢φ→∃xx∈A∧∀t∈T0≤x⁡t∧x⁡t≤1∧∀t∈Dx⁡t<E∧∀t∈B1−E<x⁡t
71 df-rex ⊢∃x∈A∀t∈T0≤x⁡t∧x⁡t≤1∧∀t∈Dx⁡t<E∧∀t∈B1−E<x⁡t↔∃xx∈A∧∀t∈T0≤x⁡t∧x⁡t≤1∧∀t∈Dx⁡t<E∧∀t∈B1−E<x⁡t
72 70 71 sylibr ⊢φ→∃x∈A∀t∈T0≤x⁡t∧x⁡t≤1∧∀t∈Dx⁡t<E∧∀t∈B1−E<x⁡t