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