Metamath Proof Explorer

Theorem stoweidlem51

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 stoweidlem51.1 ⊢ Ⅎ 𝑖 𝜑
stoweidlem51.2 ⊢ Ⅎ 𝑡 𝜑
stoweidlem51.3 ⊢ Ⅎ 𝑤 𝜑
stoweidlem51.4 ⊢ Ⅎ 𝑤 𝑉
stoweidlem51.5 ⊢ 𝑌 = { ℎ ∈ 𝐴 ∣ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) }
stoweidlem51.6 ⊢ 𝑃 = ( 𝑓 ∈ 𝑌 , 𝑔 ∈ 𝑌 ↦ ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) )
stoweidlem51.7 ⊢ 𝑋 = ( seq 1 ( 𝑃 , 𝑈 ) ‘ 𝑀 )
stoweidlem51.8 ⊢ 𝐹 = ( 𝑡 ∈ 𝑇 ↦ ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑡 ) ) )
stoweidlem51.9 ⊢ 𝑍 = ( 𝑡 ∈ 𝑇 ↦ ( seq 1 ( · , ( 𝐹 ‘ 𝑡 ) ) ‘ 𝑀 ) )
stoweidlem51.10 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
stoweidlem51.11 ⊢ ( 𝜑 → 𝑊 : ( 1 ... 𝑀 ) ⟶ 𝑉 )
stoweidlem51.12 ⊢ ( 𝜑 → 𝑈 : ( 1 ... 𝑀 ) ⟶ 𝑌 )
stoweidlem51.13 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑉 ) → 𝑤 ⊆ 𝑇 )
stoweidlem51.14 ⊢ ( 𝜑 → 𝐷 ⊆ ∪ ran 𝑊 )
stoweidlem51.15 ⊢ ( 𝜑 → 𝐷 ⊆ 𝑇 )
stoweidlem51.16 ⊢ ( 𝜑 → 𝐵 ⊆ 𝑇 )
stoweidlem51.17 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ∀ 𝑡 ∈ ( 𝑊 ‘ 𝑖 ) ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) )
stoweidlem51.18 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑡 ) )
stoweidlem51.19 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
stoweidlem51.20 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ )
stoweidlem51.21 ⊢ ( 𝜑 → 𝑇 ∈ V )
stoweidlem51.22 ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
stoweidlem51.23 ⊢ ( 𝜑 → 𝐸 < ( 1 / 3 ) )
Assertion stoweidlem51 ( 𝜑 → ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝐷 ( 𝑥 ‘ 𝑡 ) < 𝐸 ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − 𝐸 ) < ( 𝑥 ‘ 𝑡 ) ) ) )

Proof

Step Hyp Ref Expression
1 stoweidlem51.1 ⊢ Ⅎ 𝑖 𝜑
2 stoweidlem51.2 ⊢ Ⅎ 𝑡 𝜑
3 stoweidlem51.3 ⊢ Ⅎ 𝑤 𝜑
4 stoweidlem51.4 ⊢ Ⅎ 𝑤 𝑉
5 stoweidlem51.5 ⊢ 𝑌 = { ℎ ∈ 𝐴 ∣ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) }
6 stoweidlem51.6 ⊢ 𝑃 = ( 𝑓 ∈ 𝑌 , 𝑔 ∈ 𝑌 ↦ ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) )
7 stoweidlem51.7 ⊢ 𝑋 = ( seq 1 ( 𝑃 , 𝑈 ) ‘ 𝑀 )
8 stoweidlem51.8 ⊢ 𝐹 = ( 𝑡 ∈ 𝑇 ↦ ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑡 ) ) )
9 stoweidlem51.9 ⊢ 𝑍 = ( 𝑡 ∈ 𝑇 ↦ ( seq 1 ( · , ( 𝐹 ‘ 𝑡 ) ) ‘ 𝑀 ) )
10 stoweidlem51.10 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
11 stoweidlem51.11 ⊢ ( 𝜑 → 𝑊 : ( 1 ... 𝑀 ) ⟶ 𝑉 )
12 stoweidlem51.12 ⊢ ( 𝜑 → 𝑈 : ( 1 ... 𝑀 ) ⟶ 𝑌 )
13 stoweidlem51.13 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑉 ) → 𝑤 ⊆ 𝑇 )
14 stoweidlem51.14 ⊢ ( 𝜑 → 𝐷 ⊆ ∪ ran 𝑊 )
15 stoweidlem51.15 ⊢ ( 𝜑 → 𝐷 ⊆ 𝑇 )
16 stoweidlem51.16 ⊢ ( 𝜑 → 𝐵 ⊆ 𝑇 )
17 stoweidlem51.17 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ∀ 𝑡 ∈ ( 𝑊 ‘ 𝑖 ) ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) )
18 stoweidlem51.18 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑡 ) )
19 stoweidlem51.19 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
20 stoweidlem51.20 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ )
21 stoweidlem51.21 ⊢ ( 𝜑 → 𝑇 ∈ V )
22 stoweidlem51.22 ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
23 stoweidlem51.23 ⊢ ( 𝜑 → 𝐸 < ( 1 / 3 ) )
24 ssrab2 ⊢ { ℎ ∈ 𝐴 ∣ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) } ⊆ 𝐴
25 5 24 eqsstri ⊢ 𝑌 ⊆ 𝐴
26 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
27 10 nnzd ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
28 10 nnge1d ⊢ ( 𝜑 → 1 ≤ 𝑀 )
29 10 nnred ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
30 29 leidd ⊢ ( 𝜑 → 𝑀 ≤ 𝑀 )
31 26 27 27 28 30 elfzd ⊢ ( 𝜑 → 𝑀 ∈ ( 1 ... 𝑀 ) )
32 eqid ⊢ ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) )
33 2 5 32 20 19 stoweidlem16 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝑌 )
34 6 7 31 12 33 21 fmulcl ⊢ ( 𝜑 → 𝑋 ∈ 𝑌 )
35 25 34 sselid ⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
36 5 eleq2i ⊢ ( 𝑋 ∈ 𝑌 ↔ 𝑋 ∈ { ℎ ∈ 𝐴 ∣ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) } )
37 nfcv ⊢ Ⅎ ℎ 1
38 nfrab1 ⊢ Ⅎ ℎ { ℎ ∈ 𝐴 ∣ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) }
39 5 38 nfcxfr ⊢ Ⅎ ℎ 𝑌
40 nfcv ⊢ Ⅎ ℎ ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) )
41 39 39 40 nfmpo ⊢ Ⅎ ℎ ( 𝑓 ∈ 𝑌 , 𝑔 ∈ 𝑌 ↦ ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) )
42 6 41 nfcxfr ⊢ Ⅎ ℎ 𝑃
43 nfcv ⊢ Ⅎ ℎ 𝑈
44 37 42 43 nfseq ⊢ Ⅎ ℎ seq 1 ( 𝑃 , 𝑈 )
45 nfcv ⊢ Ⅎ ℎ 𝑀
46 44 45 nffv ⊢ Ⅎ ℎ ( seq 1 ( 𝑃 , 𝑈 ) ‘ 𝑀 )
47 7 46 nfcxfr ⊢ Ⅎ ℎ 𝑋
48 nfcv ⊢ Ⅎ ℎ 𝐴
49 nfcv ⊢ Ⅎ ℎ 𝑇
50 nfcv ⊢ Ⅎ ℎ 0
51 nfcv ⊢ Ⅎ ℎ ≤
52 nfcv ⊢ Ⅎ ℎ 𝑡
53 47 52 nffv ⊢ Ⅎ ℎ ( 𝑋 ‘ 𝑡 )
54 50 51 53 nfbr ⊢ Ⅎ ℎ 0 ≤ ( 𝑋 ‘ 𝑡 )
55 53 51 37 nfbr ⊢ Ⅎ ℎ ( 𝑋 ‘ 𝑡 ) ≤ 1
56 54 55 nfan ⊢ Ⅎ ℎ ( 0 ≤ ( 𝑋 ‘ 𝑡 ) ∧ ( 𝑋 ‘ 𝑡 ) ≤ 1 )
57 49 56 nfralw ⊢ Ⅎ ℎ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑋 ‘ 𝑡 ) ∧ ( 𝑋 ‘ 𝑡 ) ≤ 1 )
58 nfcv ⊢ Ⅎ 𝑡 1
59 nfra1 ⊢ Ⅎ 𝑡 ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 )
60 nfcv ⊢ Ⅎ 𝑡 𝐴
61 59 60 nfrabw ⊢ Ⅎ 𝑡 { ℎ ∈ 𝐴 ∣ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) }
62 5 61 nfcxfr ⊢ Ⅎ 𝑡 𝑌
63 nfmpt1 ⊢ Ⅎ 𝑡 ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) )
64 62 62 63 nfmpo ⊢ Ⅎ 𝑡 ( 𝑓 ∈ 𝑌 , 𝑔 ∈ 𝑌 ↦ ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) )
65 6 64 nfcxfr ⊢ Ⅎ 𝑡 𝑃
66 nfcv ⊢ Ⅎ 𝑡 𝑈
67 58 65 66 nfseq ⊢ Ⅎ 𝑡 seq 1 ( 𝑃 , 𝑈 )
68 nfcv ⊢ Ⅎ 𝑡 𝑀
69 67 68 nffv ⊢ Ⅎ 𝑡 ( seq 1 ( 𝑃 , 𝑈 ) ‘ 𝑀 )
70 7 69 nfcxfr ⊢ Ⅎ 𝑡 𝑋
71 70 nfeq2 ⊢ Ⅎ 𝑡 ℎ = 𝑋
72 fveq1 ⊢ ( ℎ = 𝑋 → ( ℎ ‘ 𝑡 ) = ( 𝑋 ‘ 𝑡 ) )
73 72 breq2d ⊢ ( ℎ = 𝑋 → ( 0 ≤ ( ℎ ‘ 𝑡 ) ↔ 0 ≤ ( 𝑋 ‘ 𝑡 ) ) )
74 72 breq1d ⊢ ( ℎ = 𝑋 → ( ( ℎ ‘ 𝑡 ) ≤ 1 ↔ ( 𝑋 ‘ 𝑡 ) ≤ 1 ) )
75 73 74 anbi12d ⊢ ( ℎ = 𝑋 → ( ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ↔ ( 0 ≤ ( 𝑋 ‘ 𝑡 ) ∧ ( 𝑋 ‘ 𝑡 ) ≤ 1 ) ) )
76 71 75 ralbid ⊢ ( ℎ = 𝑋 → ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ↔ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑋 ‘ 𝑡 ) ∧ ( 𝑋 ‘ 𝑡 ) ≤ 1 ) ) )
77 47 48 57 76 elrabf ⊢ ( 𝑋 ∈ { ℎ ∈ 𝐴 ∣ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) } ↔ ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑋 ‘ 𝑡 ) ∧ ( 𝑋 ‘ 𝑡 ) ≤ 1 ) ) )
78 36 77 bitri ⊢ ( 𝑋 ∈ 𝑌 ↔ ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑋 ‘ 𝑡 ) ∧ ( 𝑋 ‘ 𝑡 ) ≤ 1 ) ) )
79 34 78 sylib ⊢ ( 𝜑 → ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑋 ‘ 𝑡 ) ∧ ( 𝑋 ‘ 𝑡 ) ≤ 1 ) ) )
80 79 simprd ⊢ ( 𝜑 → ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑋 ‘ 𝑡 ) ∧ ( 𝑋 ‘ 𝑡 ) ≤ 1 ) )
81 nfv ⊢ Ⅎ 𝑡 𝑖 ∈ ( 1 ... 𝑀 )
82 2 81 nfan ⊢ Ⅎ 𝑡 ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) )
83 12 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝑈 ‘ 𝑖 ) ∈ 𝑌 )
84 fveq1 ⊢ ( ℎ = ( 𝑈 ‘ 𝑖 ) → ( ℎ ‘ 𝑡 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑡 ) )
85 84 breq2d ⊢ ( ℎ = ( 𝑈 ‘ 𝑖 ) → ( 0 ≤ ( ℎ ‘ 𝑡 ) ↔ 0 ≤ ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑡 ) ) )
86 84 breq1d ⊢ ( ℎ = ( 𝑈 ‘ 𝑖 ) → ( ( ℎ ‘ 𝑡 ) ≤ 1 ↔ ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑡 ) ≤ 1 ) )
87 85 86 anbi12d ⊢ ( ℎ = ( 𝑈 ‘ 𝑖 ) → ( ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ↔ ( 0 ≤ ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑡 ) ∧ ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑡 ) ≤ 1 ) ) )
88 87 ralbidv ⊢ ( ℎ = ( 𝑈 ‘ 𝑖 ) → ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ↔ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑡 ) ∧ ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑡 ) ≤ 1 ) ) )
89 88 5 elrab2 ⊢ ( ( 𝑈 ‘ 𝑖 ) ∈ 𝑌 ↔ ( ( 𝑈 ‘ 𝑖 ) ∈ 𝐴 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑡 ) ∧ ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑡 ) ≤ 1 ) ) )
90 89 simplbi ⊢ ( ( 𝑈 ‘ 𝑖 ) ∈ 𝑌 → ( 𝑈 ‘ 𝑖 ) ∈ 𝐴 )
91 83 90 syl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝑈 ‘ 𝑖 ) ∈ 𝐴 )
92 eleq1 ⊢ ( 𝑓 = ( 𝑈 ‘ 𝑖 ) → ( 𝑓 ∈ 𝐴 ↔ ( 𝑈 ‘ 𝑖 ) ∈ 𝐴 ) )
93 92 anbi2d ⊢ ( 𝑓 = ( 𝑈 ‘ 𝑖 ) → ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) ↔ ( 𝜑 ∧ ( 𝑈 ‘ 𝑖 ) ∈ 𝐴 ) ) )
94 feq1 ⊢ ( 𝑓 = ( 𝑈 ‘ 𝑖 ) → ( 𝑓 : 𝑇 ⟶ ℝ ↔ ( 𝑈 ‘ 𝑖 ) : 𝑇 ⟶ ℝ ) )
95 93 94 imbi12d ⊢ ( 𝑓 = ( 𝑈 ‘ 𝑖 ) → ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ ) ↔ ( ( 𝜑 ∧ ( 𝑈 ‘ 𝑖 ) ∈ 𝐴 ) → ( 𝑈 ‘ 𝑖 ) : 𝑇 ⟶ ℝ ) ) )
96 20 a1i ⊢ ( 𝑓 ∈ 𝐴 → ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ ) )
97 95 96 vtoclga ⊢ ( ( 𝑈 ‘ 𝑖 ) ∈ 𝐴 → ( ( 𝜑 ∧ ( 𝑈 ‘ 𝑖 ) ∈ 𝐴 ) → ( 𝑈 ‘ 𝑖 ) : 𝑇 ⟶ ℝ ) )
98 97 anabsi7 ⊢ ( ( 𝜑 ∧ ( 𝑈 ‘ 𝑖 ) ∈ 𝐴 ) → ( 𝑈 ‘ 𝑖 ) : 𝑇 ⟶ ℝ )
99 91 98 syldan ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝑈 ‘ 𝑖 ) : 𝑇 ⟶ ℝ )
100 99 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑡 ∈ ( 𝑊 ‘ 𝑖 ) ) → ( 𝑈 ‘ 𝑖 ) : 𝑇 ⟶ ℝ )
101 11 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝑊 ‘ 𝑖 ) ∈ 𝑉 )
102 simpl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → 𝜑 )
103 102 101 jca ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝜑 ∧ ( 𝑊 ‘ 𝑖 ) ∈ 𝑉 ) )
104 4 nfel2 ⊢ Ⅎ 𝑤 ( 𝑊 ‘ 𝑖 ) ∈ 𝑉
105 3 104 nfan ⊢ Ⅎ 𝑤 ( 𝜑 ∧ ( 𝑊 ‘ 𝑖 ) ∈ 𝑉 )
106 nfv ⊢ Ⅎ 𝑤 ( 𝑊 ‘ 𝑖 ) ⊆ 𝑇
107 105 106 nfim ⊢ Ⅎ 𝑤 ( ( 𝜑 ∧ ( 𝑊 ‘ 𝑖 ) ∈ 𝑉 ) → ( 𝑊 ‘ 𝑖 ) ⊆ 𝑇 )
108 eleq1 ⊢ ( 𝑤 = ( 𝑊 ‘ 𝑖 ) → ( 𝑤 ∈ 𝑉 ↔ ( 𝑊 ‘ 𝑖 ) ∈ 𝑉 ) )
109 108 anbi2d ⊢ ( 𝑤 = ( 𝑊 ‘ 𝑖 ) → ( ( 𝜑 ∧ 𝑤 ∈ 𝑉 ) ↔ ( 𝜑 ∧ ( 𝑊 ‘ 𝑖 ) ∈ 𝑉 ) ) )
110 sseq1 ⊢ ( 𝑤 = ( 𝑊 ‘ 𝑖 ) → ( 𝑤 ⊆ 𝑇 ↔ ( 𝑊 ‘ 𝑖 ) ⊆ 𝑇 ) )
111 109 110 imbi12d ⊢ ( 𝑤 = ( 𝑊 ‘ 𝑖 ) → ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑉 ) → 𝑤 ⊆ 𝑇 ) ↔ ( ( 𝜑 ∧ ( 𝑊 ‘ 𝑖 ) ∈ 𝑉 ) → ( 𝑊 ‘ 𝑖 ) ⊆ 𝑇 ) ) )
112 107 111 13 vtoclg1f ⊢ ( ( 𝑊 ‘ 𝑖 ) ∈ 𝑉 → ( ( 𝜑 ∧ ( 𝑊 ‘ 𝑖 ) ∈ 𝑉 ) → ( 𝑊 ‘ 𝑖 ) ⊆ 𝑇 ) )
113 101 103 112 sylc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝑊 ‘ 𝑖 ) ⊆ 𝑇 )
114 113 sselda ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑡 ∈ ( 𝑊 ‘ 𝑖 ) ) → 𝑡 ∈ 𝑇 )
115 100 114 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑡 ∈ ( 𝑊 ‘ 𝑖 ) ) → ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑡 ) ∈ ℝ )
116 22 rpred ⊢ ( 𝜑 → 𝐸 ∈ ℝ )
117 116 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑡 ∈ ( 𝑊 ‘ 𝑖 ) ) → 𝐸 ∈ ℝ )
118 29 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑡 ∈ ( 𝑊 ‘ 𝑖 ) ) → 𝑀 ∈ ℝ )
119 10 nnne0d ⊢ ( 𝜑 → 𝑀 ≠ 0 )
120 119 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑡 ∈ ( 𝑊 ‘ 𝑖 ) ) → 𝑀 ≠ 0 )
121 117 118 120 redivcld ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑡 ∈ ( 𝑊 ‘ 𝑖 ) ) → ( 𝐸 / 𝑀 ) ∈ ℝ )
122 17 r19.21bi ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑡 ∈ ( 𝑊 ‘ 𝑖 ) ) → ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) )
123 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
124 0lt1 ⊢ 0 < 1
125 124 a1i ⊢ ( 𝜑 → 0 < 1 )
126 10 nngt0d ⊢ ( 𝜑 → 0 < 𝑀 )
127 22 rpregt0d ⊢ ( 𝜑 → ( 𝐸 ∈ ℝ ∧ 0 < 𝐸 ) )
128 lediv2 ⊢ ( ( ( 1 ∈ ℝ ∧ 0 < 1 ) ∧ ( 𝑀 ∈ ℝ ∧ 0 < 𝑀 ) ∧ ( 𝐸 ∈ ℝ ∧ 0 < 𝐸 ) ) → ( 1 ≤ 𝑀 ↔ ( 𝐸 / 𝑀 ) ≤ ( 𝐸 / 1 ) ) )
129 123 125 29 126 127 128 syl221anc ⊢ ( 𝜑 → ( 1 ≤ 𝑀 ↔ ( 𝐸 / 𝑀 ) ≤ ( 𝐸 / 1 ) ) )
130 28 129 mpbid ⊢ ( 𝜑 → ( 𝐸 / 𝑀 ) ≤ ( 𝐸 / 1 ) )
131 22 rpcnd ⊢ ( 𝜑 → 𝐸 ∈ ℂ )
132 131 div1d ⊢ ( 𝜑 → ( 𝐸 / 1 ) = 𝐸 )
133 130 132 breqtrd ⊢ ( 𝜑 → ( 𝐸 / 𝑀 ) ≤ 𝐸 )
134 133 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑡 ∈ ( 𝑊 ‘ 𝑖 ) ) → ( 𝐸 / 𝑀 ) ≤ 𝐸 )
135 115 121 117 122 134 ltletrd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑡 ∈ ( 𝑊 ‘ 𝑖 ) ) → ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑡 ) < 𝐸 )
136 135 ex ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝑡 ∈ ( 𝑊 ‘ 𝑖 ) → ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑡 ) < 𝐸 ) )
137 82 136 ralrimi ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ∀ 𝑡 ∈ ( 𝑊 ‘ 𝑖 ) ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑡 ) < 𝐸 )
138 1 2 5 6 7 8 9 10 11 12 14 15 137 21 20 19 22 stoweidlem48 ⊢ ( 𝜑 → ∀ 𝑡 ∈ 𝐷 ( 𝑋 ‘ 𝑡 ) < 𝐸 )
139 25 sseli ⊢ ( 𝑓 ∈ 𝑌 → 𝑓 ∈ 𝐴 )
140 139 20 sylan2 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑌 ) → 𝑓 : 𝑇 ⟶ ℝ )
141 1 2 62 6 7 8 9 10 12 18 22 23 140 33 21 16 stoweidlem42 ⊢ ( 𝜑 → ∀ 𝑡 ∈ 𝐵 ( 1 − 𝐸 ) < ( 𝑋 ‘ 𝑡 ) )
142 80 138 141 3jca ⊢ ( 𝜑 → ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑋 ‘ 𝑡 ) ∧ ( 𝑋 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝐷 ( 𝑋 ‘ 𝑡 ) < 𝐸 ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − 𝐸 ) < ( 𝑋 ‘ 𝑡 ) ) )
143 35 142 jca ⊢ ( 𝜑 → ( 𝑋 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑋 ‘ 𝑡 ) ∧ ( 𝑋 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝐷 ( 𝑋 ‘ 𝑡 ) < 𝐸 ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − 𝐸 ) < ( 𝑋 ‘ 𝑡 ) ) ) )
144 eleq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ∈ 𝐴 ↔ 𝑋 ∈ 𝐴 ) )
145 70 nfeq2 ⊢ Ⅎ 𝑡 𝑥 = 𝑋
146 fveq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ‘ 𝑡 ) = ( 𝑋 ‘ 𝑡 ) )
147 146 breq2d ⊢ ( 𝑥 = 𝑋 → ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ↔ 0 ≤ ( 𝑋 ‘ 𝑡 ) ) )
148 146 breq1d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 ‘ 𝑡 ) ≤ 1 ↔ ( 𝑋 ‘ 𝑡 ) ≤ 1 ) )
149 147 148 anbi12d ⊢ ( 𝑥 = 𝑋 → ( ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ↔ ( 0 ≤ ( 𝑋 ‘ 𝑡 ) ∧ ( 𝑋 ‘ 𝑡 ) ≤ 1 ) ) )
150 145 149 ralbid ⊢ ( 𝑥 = 𝑋 → ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ↔ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑋 ‘ 𝑡 ) ∧ ( 𝑋 ‘ 𝑡 ) ≤ 1 ) ) )
151 146 breq1d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 ‘ 𝑡 ) < 𝐸 ↔ ( 𝑋 ‘ 𝑡 ) < 𝐸 ) )
152 145 151 ralbid ⊢ ( 𝑥 = 𝑋 → ( ∀ 𝑡 ∈ 𝐷 ( 𝑥 ‘ 𝑡 ) < 𝐸 ↔ ∀ 𝑡 ∈ 𝐷 ( 𝑋 ‘ 𝑡 ) < 𝐸 ) )
153 146 breq2d ⊢ ( 𝑥 = 𝑋 → ( ( 1 − 𝐸 ) < ( 𝑥 ‘ 𝑡 ) ↔ ( 1 − 𝐸 ) < ( 𝑋 ‘ 𝑡 ) ) )
154 145 153 ralbid ⊢ ( 𝑥 = 𝑋 → ( ∀ 𝑡 ∈ 𝐵 ( 1 − 𝐸 ) < ( 𝑥 ‘ 𝑡 ) ↔ ∀ 𝑡 ∈ 𝐵 ( 1 − 𝐸 ) < ( 𝑋 ‘ 𝑡 ) ) )
155 150 152 154 3anbi123d ⊢ ( 𝑥 = 𝑋 → ( ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝐷 ( 𝑥 ‘ 𝑡 ) < 𝐸 ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − 𝐸 ) < ( 𝑥 ‘ 𝑡 ) ) ↔ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑋 ‘ 𝑡 ) ∧ ( 𝑋 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝐷 ( 𝑋 ‘ 𝑡 ) < 𝐸 ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − 𝐸 ) < ( 𝑋 ‘ 𝑡 ) ) ) )
156 144 155 anbi12d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝐷 ( 𝑥 ‘ 𝑡 ) < 𝐸 ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − 𝐸 ) < ( 𝑥 ‘ 𝑡 ) ) ) ↔ ( 𝑋 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑋 ‘ 𝑡 ) ∧ ( 𝑋 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝐷 ( 𝑋 ‘ 𝑡 ) < 𝐸 ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − 𝐸 ) < ( 𝑋 ‘ 𝑡 ) ) ) ) )
157 156 spcegv ⊢ ( 𝑋 ∈ 𝐴 → ( ( 𝑋 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑋 ‘ 𝑡 ) ∧ ( 𝑋 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝐷 ( 𝑋 ‘ 𝑡 ) < 𝐸 ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − 𝐸 ) < ( 𝑋 ‘ 𝑡 ) ) ) → ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝐷 ( 𝑥 ‘ 𝑡 ) < 𝐸 ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − 𝐸 ) < ( 𝑥 ‘ 𝑡 ) ) ) ) )
158 35 143 157 sylc ⊢ ( 𝜑 → ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝐷 ( 𝑥 ‘ 𝑡 ) < 𝐸 ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − 𝐸 ) < ( 𝑥 ‘ 𝑡 ) ) ) )