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

Proof

Step Hyp Ref Expression
1 stoweidlem54.1 ⊢ Ⅎ 𝑖 𝜑
2 stoweidlem54.2 ⊢ Ⅎ 𝑡 𝜑
3 stoweidlem54.3 ⊢ Ⅎ 𝑦 𝜑
4 stoweidlem54.4 ⊢ Ⅎ 𝑤 𝜑
5 stoweidlem54.5 ⊢ 𝑇 = ∪ 𝐽
6 stoweidlem54.6 ⊢ 𝑌 = { ℎ ∈ 𝐴 ∣ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) }
7 stoweidlem54.7 ⊢ 𝑃 = ( 𝑓 ∈ 𝑌 , 𝑔 ∈ 𝑌 ↦ ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) )
8 stoweidlem54.8 ⊢ 𝐹 = ( 𝑡 ∈ 𝑇 ↦ ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) )
9 stoweidlem54.9 ⊢ 𝑍 = ( 𝑡 ∈ 𝑇 ↦ ( seq 1 ( · , ( 𝐹 ‘ 𝑡 ) ) ‘ 𝑀 ) )
10 stoweidlem54.10 ⊢ 𝑉 = { 𝑤 ∈ 𝐽 ∣ ∀ 𝑒 ∈ ℝ+ ∃ ℎ ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( ℎ ‘ 𝑡 ) ) }
11 stoweidlem54.11 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
12 stoweidlem54.12 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ )
13 stoweidlem54.13 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
14 stoweidlem54.14 ⊢ ( 𝜑 → 𝑊 : ( 1 ... 𝑀 ) ⟶ 𝑉 )
15 stoweidlem54.15 ⊢ ( 𝜑 → 𝐵 ⊆ 𝑇 )
16 stoweidlem54.16 ⊢ ( 𝜑 → 𝐷 ⊆ ∪ ran 𝑊 )
17 stoweidlem54.17 ⊢ ( 𝜑 → 𝐷 ⊆ 𝑇 )
18 stoweidlem54.18 ⊢ ( 𝜑 → ∃ 𝑦 ( 𝑦 : ( 1 ... 𝑀 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ∀ 𝑡 ∈ ( 𝑊 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) ) )
19 stoweidlem54.19 ⊢ ( 𝜑 → 𝑇 ∈ V )
20 stoweidlem54.20 ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
21 stoweidlem54.21 ⊢ ( 𝜑 → 𝐸 < ( 1 / 3 ) )
22 nfv ⊢ Ⅎ 𝑦 ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝐷 ( 𝑥 ‘ 𝑡 ) < 𝐸 ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − 𝐸 ) < ( 𝑥 ‘ 𝑡 ) ) )
23 nfv ⊢ Ⅎ 𝑖 𝑦 : ( 1 ... 𝑀 ) ⟶ 𝑌
24 nfra1 ⊢ Ⅎ 𝑖 ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ∀ 𝑡 ∈ ( 𝑊 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) )
25 23 24 nfan ⊢ Ⅎ 𝑖 ( 𝑦 : ( 1 ... 𝑀 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ∀ 𝑡 ∈ ( 𝑊 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) )
26 1 25 nfan ⊢ Ⅎ 𝑖 ( 𝜑 ∧ ( 𝑦 : ( 1 ... 𝑀 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ∀ 𝑡 ∈ ( 𝑊 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) ) )
27 nfcv ⊢ Ⅎ 𝑡 𝑦
28 nfcv ⊢ Ⅎ 𝑡 ( 1 ... 𝑀 )
29 nfra1 ⊢ Ⅎ 𝑡 ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 )
30 nfcv ⊢ Ⅎ 𝑡 𝐴
31 29 30 nfrabw ⊢ Ⅎ 𝑡 { ℎ ∈ 𝐴 ∣ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) }
32 6 31 nfcxfr ⊢ Ⅎ 𝑡 𝑌
33 27 28 32 nff ⊢ Ⅎ 𝑡 𝑦 : ( 1 ... 𝑀 ) ⟶ 𝑌
34 nfra1 ⊢ Ⅎ 𝑡 ∀ 𝑡 ∈ ( 𝑊 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 )
35 nfra1 ⊢ Ⅎ 𝑡 ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 )
36 34 35 nfan ⊢ Ⅎ 𝑡 ( ∀ 𝑡 ∈ ( 𝑊 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) )
37 28 36 nfralw ⊢ Ⅎ 𝑡 ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ∀ 𝑡 ∈ ( 𝑊 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) )
38 33 37 nfan ⊢ Ⅎ 𝑡 ( 𝑦 : ( 1 ... 𝑀 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ∀ 𝑡 ∈ ( 𝑊 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) )
39 2 38 nfan ⊢ Ⅎ 𝑡 ( 𝜑 ∧ ( 𝑦 : ( 1 ... 𝑀 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ∀ 𝑡 ∈ ( 𝑊 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) ) )
40 nfv ⊢ Ⅎ 𝑤 ( 𝑦 : ( 1 ... 𝑀 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ∀ 𝑡 ∈ ( 𝑊 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) )
41 4 40 nfan ⊢ Ⅎ 𝑤 ( 𝜑 ∧ ( 𝑦 : ( 1 ... 𝑀 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ∀ 𝑡 ∈ ( 𝑊 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) ) )
42 nfrab1 ⊢ Ⅎ 𝑤 { 𝑤 ∈ 𝐽 ∣ ∀ 𝑒 ∈ ℝ+ ∃ ℎ ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( ℎ ‘ 𝑡 ) ) }
43 10 42 nfcxfr ⊢ Ⅎ 𝑤 𝑉
44 eqid ⊢ ( seq 1 ( 𝑃 , 𝑦 ) ‘ 𝑀 ) = ( seq 1 ( 𝑃 , 𝑦 ) ‘ 𝑀 )
45 13 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 : ( 1 ... 𝑀 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ∀ 𝑡 ∈ ( 𝑊 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ) → 𝑀 ∈ ℕ )
46 14 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 : ( 1 ... 𝑀 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ∀ 𝑡 ∈ ( 𝑊 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ) → 𝑊 : ( 1 ... 𝑀 ) ⟶ 𝑉 )
47 simprl ⊢ ( ( 𝜑 ∧ ( 𝑦 : ( 1 ... 𝑀 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ∀ 𝑡 ∈ ( 𝑊 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ) → 𝑦 : ( 1 ... 𝑀 ) ⟶ 𝑌 )
48 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 : ( 1 ... 𝑀 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ∀ 𝑡 ∈ ( 𝑊 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ) ∧ 𝑤 ∈ 𝑉 ) → 𝑤 ∈ 𝑉 )
49 10 reqabi ⊢ ( 𝑤 ∈ 𝑉 ↔ ( 𝑤 ∈ 𝐽 ∧ ∀ 𝑒 ∈ ℝ+ ∃ ℎ ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( ℎ ‘ 𝑡 ) ) ) )
50 49 simplbi ⊢ ( 𝑤 ∈ 𝑉 → 𝑤 ∈ 𝐽 )
51 elssuni ⊢ ( 𝑤 ∈ 𝐽 → 𝑤 ⊆ ∪ 𝐽 )
52 51 5 sseqtrrdi ⊢ ( 𝑤 ∈ 𝐽 → 𝑤 ⊆ 𝑇 )
53 48 50 52 3syl ⊢ ( ( ( 𝜑 ∧ ( 𝑦 : ( 1 ... 𝑀 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ∀ 𝑡 ∈ ( 𝑊 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ) ∧ 𝑤 ∈ 𝑉 ) → 𝑤 ⊆ 𝑇 )
54 16 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 : ( 1 ... 𝑀 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ∀ 𝑡 ∈ ( 𝑊 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ) → 𝐷 ⊆ ∪ ran 𝑊 )
55 17 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 : ( 1 ... 𝑀 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ∀ 𝑡 ∈ ( 𝑊 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ) → 𝐷 ⊆ 𝑇 )
56 15 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 : ( 1 ... 𝑀 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ∀ 𝑡 ∈ ( 𝑊 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ) → 𝐵 ⊆ 𝑇 )
57 r19.26 ⊢ ( ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ∀ 𝑡 ∈ ( 𝑊 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) ↔ ( ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ∀ 𝑡 ∈ ( 𝑊 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) )
58 57 simplbi ⊢ ( ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ∀ 𝑡 ∈ ( 𝑊 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) → ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ∀ 𝑡 ∈ ( 𝑊 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) )
59 58 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑦 : ( 1 ... 𝑀 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ∀ 𝑡 ∈ ( 𝑊 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ) → ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ∀ 𝑡 ∈ ( 𝑊 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) )
60 59 r19.21bi ⊢ ( ( ( 𝜑 ∧ ( 𝑦 : ( 1 ... 𝑀 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ∀ 𝑡 ∈ ( 𝑊 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ∀ 𝑡 ∈ ( 𝑊 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) )
61 57 simprbi ⊢ ( ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ∀ 𝑡 ∈ ( 𝑊 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) → ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) )
62 61 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑦 : ( 1 ... 𝑀 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ∀ 𝑡 ∈ ( 𝑊 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ) → ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) )
63 62 r19.21bi ⊢ ( ( ( 𝜑 ∧ ( 𝑦 : ( 1 ... 𝑀 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ∀ 𝑡 ∈ ( 𝑊 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) )
64 11 3adant1r ⊢ ( ( ( 𝜑 ∧ ( 𝑦 : ( 1 ... 𝑀 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ∀ 𝑡 ∈ ( 𝑊 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
65 12 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 : ( 1 ... 𝑀 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ∀ 𝑡 ∈ ( 𝑊 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ) ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ )
66 19 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 : ( 1 ... 𝑀 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ∀ 𝑡 ∈ ( 𝑊 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ) → 𝑇 ∈ V )
67 20 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 : ( 1 ... 𝑀 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ∀ 𝑡 ∈ ( 𝑊 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ) → 𝐸 ∈ ℝ+ )
68 21 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 : ( 1 ... 𝑀 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ∀ 𝑡 ∈ ( 𝑊 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ) → 𝐸 < ( 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 ⊢ ( ( 𝜑 ∧ ( 𝑦 : ( 1 ... 𝑀 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ∀ 𝑡 ∈ ( 𝑊 ‘ 𝑖 ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ) → ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝐷 ( 𝑥 ‘ 𝑡 ) < 𝐸 ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − 𝐸 ) < ( 𝑥 ‘ 𝑡 ) ) ) )
70 3 22 18 69 exlimdd ⊢ ( 𝜑 → ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝐷 ( 𝑥 ‘ 𝑡 ) < 𝐸 ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − 𝐸 ) < ( 𝑥 ‘ 𝑡 ) ) ) )
71 df-rex ⊢ ( ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝐷 ( 𝑥 ‘ 𝑡 ) < 𝐸 ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − 𝐸 ) < ( 𝑥 ‘ 𝑡 ) ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝐷 ( 𝑥 ‘ 𝑡 ) < 𝐸 ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − 𝐸 ) < ( 𝑥 ‘ 𝑡 ) ) ) )
72 70 71 sylibr ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝐷 ( 𝑥 ‘ 𝑡 ) < 𝐸 ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − 𝐸 ) < ( 𝑥 ‘ 𝑡 ) ) )