# Metamath Proof Explorer

## Theorem stoweidlem48

Description: This lemma is used to prove that x built as in Lemma 2 of BrosowskiDeutsh p. 91, is such that x < ε on A . Here X is used to represent x in the paper, E is used to represent ε in the paper, and D is used to represent A in the paper (because A is always used to represent the subalgebra). (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem48.1 𝑖 𝜑
stoweidlem48.2 𝑡 𝜑
stoweidlem48.3 𝑌 = { 𝐴 ∣ ∀ 𝑡𝑇 ( 0 ≤ ( 𝑡 ) ∧ ( 𝑡 ) ≤ 1 ) }
stoweidlem48.4 𝑃 = ( 𝑓𝑌 , 𝑔𝑌 ↦ ( 𝑡𝑇 ↦ ( ( 𝑓𝑡 ) · ( 𝑔𝑡 ) ) ) )
stoweidlem48.5 𝑋 = ( seq 1 ( 𝑃 , 𝑈 ) ‘ 𝑀 )
stoweidlem48.6 𝐹 = ( 𝑡𝑇 ↦ ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝑈𝑖 ) ‘ 𝑡 ) ) )
stoweidlem48.7 𝑍 = ( 𝑡𝑇 ↦ ( seq 1 ( · , ( 𝐹𝑡 ) ) ‘ 𝑀 ) )
stoweidlem48.8 ( 𝜑𝑀 ∈ ℕ )
stoweidlem48.9 ( 𝜑𝑊 : ( 1 ... 𝑀 ) ⟶ 𝑉 )
stoweidlem48.10 ( 𝜑𝑈 : ( 1 ... 𝑀 ) ⟶ 𝑌 )
stoweidlem48.11 ( 𝜑𝐷 ran 𝑊 )
stoweidlem48.12 ( 𝜑𝐷𝑇 )
stoweidlem48.13 ( ( 𝜑𝑖 ∈ ( 1 ... 𝑀 ) ) → ∀ 𝑡 ∈ ( 𝑊𝑖 ) ( ( 𝑈𝑖 ) ‘ 𝑡 ) < 𝐸 )
stoweidlem48.14 ( 𝜑𝑇 ∈ V )
stoweidlem48.15 ( ( 𝜑𝑓𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ )
stoweidlem48.16 ( ( 𝜑𝑓𝐴𝑔𝐴 ) → ( 𝑡𝑇 ↦ ( ( 𝑓𝑡 ) · ( 𝑔𝑡 ) ) ) ∈ 𝐴 )
stoweidlem48.17 ( 𝜑𝐸 ∈ ℝ+ )
Assertion stoweidlem48 ( 𝜑 → ∀ 𝑡𝐷 ( 𝑋𝑡 ) < 𝐸 )

### Proof

Step Hyp Ref Expression
1 stoweidlem48.1 𝑖 𝜑
2 stoweidlem48.2 𝑡 𝜑
3 stoweidlem48.3 𝑌 = { 𝐴 ∣ ∀ 𝑡𝑇 ( 0 ≤ ( 𝑡 ) ∧ ( 𝑡 ) ≤ 1 ) }
4 stoweidlem48.4 𝑃 = ( 𝑓𝑌 , 𝑔𝑌 ↦ ( 𝑡𝑇 ↦ ( ( 𝑓𝑡 ) · ( 𝑔𝑡 ) ) ) )
5 stoweidlem48.5 𝑋 = ( seq 1 ( 𝑃 , 𝑈 ) ‘ 𝑀 )
6 stoweidlem48.6 𝐹 = ( 𝑡𝑇 ↦ ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝑈𝑖 ) ‘ 𝑡 ) ) )
7 stoweidlem48.7 𝑍 = ( 𝑡𝑇 ↦ ( seq 1 ( · , ( 𝐹𝑡 ) ) ‘ 𝑀 ) )
8 stoweidlem48.8 ( 𝜑𝑀 ∈ ℕ )
9 stoweidlem48.9 ( 𝜑𝑊 : ( 1 ... 𝑀 ) ⟶ 𝑉 )
10 stoweidlem48.10 ( 𝜑𝑈 : ( 1 ... 𝑀 ) ⟶ 𝑌 )
11 stoweidlem48.11 ( 𝜑𝐷 ran 𝑊 )
12 stoweidlem48.12 ( 𝜑𝐷𝑇 )
13 stoweidlem48.13 ( ( 𝜑𝑖 ∈ ( 1 ... 𝑀 ) ) → ∀ 𝑡 ∈ ( 𝑊𝑖 ) ( ( 𝑈𝑖 ) ‘ 𝑡 ) < 𝐸 )
14 stoweidlem48.14 ( 𝜑𝑇 ∈ V )
15 stoweidlem48.15 ( ( 𝜑𝑓𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ )
16 stoweidlem48.16 ( ( 𝜑𝑓𝐴𝑔𝐴 ) → ( 𝑡𝑇 ↦ ( ( 𝑓𝑡 ) · ( 𝑔𝑡 ) ) ) ∈ 𝐴 )
17 stoweidlem48.17 ( 𝜑𝐸 ∈ ℝ+ )
18 12 sselda ( ( 𝜑𝑡𝐷 ) → 𝑡𝑇 )
19 nfra1 𝑡𝑡𝑇 ( 0 ≤ ( 𝑡 ) ∧ ( 𝑡 ) ≤ 1 )
20 nfcv 𝑡 𝐴
21 19 20 nfrabw 𝑡 { 𝐴 ∣ ∀ 𝑡𝑇 ( 0 ≤ ( 𝑡 ) ∧ ( 𝑡 ) ≤ 1 ) }
22 3 21 nfcxfr 𝑡 𝑌
23 3 eleq2i ( 𝑓𝑌𝑓 ∈ { 𝐴 ∣ ∀ 𝑡𝑇 ( 0 ≤ ( 𝑡 ) ∧ ( 𝑡 ) ≤ 1 ) } )
24 fveq1 ( = 𝑓 → ( 𝑡 ) = ( 𝑓𝑡 ) )
25 24 breq2d ( = 𝑓 → ( 0 ≤ ( 𝑡 ) ↔ 0 ≤ ( 𝑓𝑡 ) ) )
26 24 breq1d ( = 𝑓 → ( ( 𝑡 ) ≤ 1 ↔ ( 𝑓𝑡 ) ≤ 1 ) )
27 25 26 anbi12d ( = 𝑓 → ( ( 0 ≤ ( 𝑡 ) ∧ ( 𝑡 ) ≤ 1 ) ↔ ( 0 ≤ ( 𝑓𝑡 ) ∧ ( 𝑓𝑡 ) ≤ 1 ) ) )
28 27 ralbidv ( = 𝑓 → ( ∀ 𝑡𝑇 ( 0 ≤ ( 𝑡 ) ∧ ( 𝑡 ) ≤ 1 ) ↔ ∀ 𝑡𝑇 ( 0 ≤ ( 𝑓𝑡 ) ∧ ( 𝑓𝑡 ) ≤ 1 ) ) )
29 28 elrab ( 𝑓 ∈ { 𝐴 ∣ ∀ 𝑡𝑇 ( 0 ≤ ( 𝑡 ) ∧ ( 𝑡 ) ≤ 1 ) } ↔ ( 𝑓𝐴 ∧ ∀ 𝑡𝑇 ( 0 ≤ ( 𝑓𝑡 ) ∧ ( 𝑓𝑡 ) ≤ 1 ) ) )
30 23 29 sylbb ( 𝑓𝑌 → ( 𝑓𝐴 ∧ ∀ 𝑡𝑇 ( 0 ≤ ( 𝑓𝑡 ) ∧ ( 𝑓𝑡 ) ≤ 1 ) ) )
31 30 simpld ( 𝑓𝑌𝑓𝐴 )
32 31 15 sylan2 ( ( 𝜑𝑓𝑌 ) → 𝑓 : 𝑇 ⟶ ℝ )
33 eqid ( 𝑡𝑇 ↦ ( ( 𝑓𝑡 ) · ( 𝑔𝑡 ) ) ) = ( 𝑡𝑇 ↦ ( ( 𝑓𝑡 ) · ( 𝑔𝑡 ) ) )
34 2 3 33 15 16 stoweidlem16 ( ( 𝜑𝑓𝑌𝑔𝑌 ) → ( 𝑡𝑇 ↦ ( ( 𝑓𝑡 ) · ( 𝑔𝑡 ) ) ) ∈ 𝑌 )
35 1 22 4 5 6 7 14 8 10 32 34 fmuldfeq ( ( 𝜑𝑡𝑇 ) → ( 𝑋𝑡 ) = ( 𝑍𝑡 ) )
36 18 35 syldan ( ( 𝜑𝑡𝐷 ) → ( 𝑋𝑡 ) = ( 𝑍𝑡 ) )
37 elnnuz ( 𝑀 ∈ ℕ ↔ 𝑀 ∈ ( ℤ ‘ 1 ) )
38 8 37 sylib ( 𝜑𝑀 ∈ ( ℤ ‘ 1 ) )
39 38 adantr ( ( 𝜑𝑡𝐷 ) → 𝑀 ∈ ( ℤ ‘ 1 ) )
40 nfv 𝑖 𝑡𝑇
41 1 40 nfan 𝑖 ( 𝜑𝑡𝑇 )
42 10 ffvelrnda ( ( 𝜑𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝑈𝑖 ) ∈ 𝑌 )
43 fveq1 ( = ( 𝑈𝑖 ) → ( 𝑡 ) = ( ( 𝑈𝑖 ) ‘ 𝑡 ) )
44 43 breq2d ( = ( 𝑈𝑖 ) → ( 0 ≤ ( 𝑡 ) ↔ 0 ≤ ( ( 𝑈𝑖 ) ‘ 𝑡 ) ) )
45 43 breq1d ( = ( 𝑈𝑖 ) → ( ( 𝑡 ) ≤ 1 ↔ ( ( 𝑈𝑖 ) ‘ 𝑡 ) ≤ 1 ) )
46 44 45 anbi12d ( = ( 𝑈𝑖 ) → ( ( 0 ≤ ( 𝑡 ) ∧ ( 𝑡 ) ≤ 1 ) ↔ ( 0 ≤ ( ( 𝑈𝑖 ) ‘ 𝑡 ) ∧ ( ( 𝑈𝑖 ) ‘ 𝑡 ) ≤ 1 ) ) )
47 46 ralbidv ( = ( 𝑈𝑖 ) → ( ∀ 𝑡𝑇 ( 0 ≤ ( 𝑡 ) ∧ ( 𝑡 ) ≤ 1 ) ↔ ∀ 𝑡𝑇 ( 0 ≤ ( ( 𝑈𝑖 ) ‘ 𝑡 ) ∧ ( ( 𝑈𝑖 ) ‘ 𝑡 ) ≤ 1 ) ) )
48 47 3 elrab2 ( ( 𝑈𝑖 ) ∈ 𝑌 ↔ ( ( 𝑈𝑖 ) ∈ 𝐴 ∧ ∀ 𝑡𝑇 ( 0 ≤ ( ( 𝑈𝑖 ) ‘ 𝑡 ) ∧ ( ( 𝑈𝑖 ) ‘ 𝑡 ) ≤ 1 ) ) )
49 42 48 sylib ( ( 𝜑𝑖 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝑈𝑖 ) ∈ 𝐴 ∧ ∀ 𝑡𝑇 ( 0 ≤ ( ( 𝑈𝑖 ) ‘ 𝑡 ) ∧ ( ( 𝑈𝑖 ) ‘ 𝑡 ) ≤ 1 ) ) )
50 49 simpld ( ( 𝜑𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝑈𝑖 ) ∈ 𝐴 )
51 simpl ( ( 𝜑𝑖 ∈ ( 1 ... 𝑀 ) ) → 𝜑 )
52 51 50 jca ( ( 𝜑𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝜑 ∧ ( 𝑈𝑖 ) ∈ 𝐴 ) )
53 eleq1 ( 𝑓 = ( 𝑈𝑖 ) → ( 𝑓𝐴 ↔ ( 𝑈𝑖 ) ∈ 𝐴 ) )
54 53 anbi2d ( 𝑓 = ( 𝑈𝑖 ) → ( ( 𝜑𝑓𝐴 ) ↔ ( 𝜑 ∧ ( 𝑈𝑖 ) ∈ 𝐴 ) ) )
55 feq1 ( 𝑓 = ( 𝑈𝑖 ) → ( 𝑓 : 𝑇 ⟶ ℝ ↔ ( 𝑈𝑖 ) : 𝑇 ⟶ ℝ ) )
56 54 55 imbi12d ( 𝑓 = ( 𝑈𝑖 ) → ( ( ( 𝜑𝑓𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ ) ↔ ( ( 𝜑 ∧ ( 𝑈𝑖 ) ∈ 𝐴 ) → ( 𝑈𝑖 ) : 𝑇 ⟶ ℝ ) ) )
57 56 15 vtoclg ( ( 𝑈𝑖 ) ∈ 𝐴 → ( ( 𝜑 ∧ ( 𝑈𝑖 ) ∈ 𝐴 ) → ( 𝑈𝑖 ) : 𝑇 ⟶ ℝ ) )
58 50 52 57 sylc ( ( 𝜑𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝑈𝑖 ) : 𝑇 ⟶ ℝ )
59 58 adantlr ( ( ( 𝜑𝑡𝑇 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝑈𝑖 ) : 𝑇 ⟶ ℝ )
60 simplr ( ( ( 𝜑𝑡𝑇 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → 𝑡𝑇 )
61 59 60 ffvelrnd ( ( ( 𝜑𝑡𝑇 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝑈𝑖 ) ‘ 𝑡 ) ∈ ℝ )
62 eqid ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝑈𝑖 ) ‘ 𝑡 ) ) = ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝑈𝑖 ) ‘ 𝑡 ) )
63 41 61 62 fmptdf ( ( 𝜑𝑡𝑇 ) → ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝑈𝑖 ) ‘ 𝑡 ) ) : ( 1 ... 𝑀 ) ⟶ ℝ )
64 simpr ( ( 𝜑𝑡𝑇 ) → 𝑡𝑇 )
65 ovex ( 1 ... 𝑀 ) ∈ V
66 mptexg ( ( 1 ... 𝑀 ) ∈ V → ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝑈𝑖 ) ‘ 𝑡 ) ) ∈ V )
67 65 66 mp1i ( ( 𝜑𝑡𝑇 ) → ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝑈𝑖 ) ‘ 𝑡 ) ) ∈ V )
68 6 fvmpt2 ( ( 𝑡𝑇 ∧ ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝑈𝑖 ) ‘ 𝑡 ) ) ∈ V ) → ( 𝐹𝑡 ) = ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝑈𝑖 ) ‘ 𝑡 ) ) )
69 64 67 68 syl2anc ( ( 𝜑𝑡𝑇 ) → ( 𝐹𝑡 ) = ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝑈𝑖 ) ‘ 𝑡 ) ) )
70 69 feq1d ( ( 𝜑𝑡𝑇 ) → ( ( 𝐹𝑡 ) : ( 1 ... 𝑀 ) ⟶ ℝ ↔ ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝑈𝑖 ) ‘ 𝑡 ) ) : ( 1 ... 𝑀 ) ⟶ ℝ ) )
71 63 70 mpbird ( ( 𝜑𝑡𝑇 ) → ( 𝐹𝑡 ) : ( 1 ... 𝑀 ) ⟶ ℝ )
72 18 71 syldan ( ( 𝜑𝑡𝐷 ) → ( 𝐹𝑡 ) : ( 1 ... 𝑀 ) ⟶ ℝ )
73 72 ffvelrnda ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝐹𝑡 ) ‘ 𝑘 ) ∈ ℝ )
74 remulcl ( ( 𝑘 ∈ ℝ ∧ 𝑗 ∈ ℝ ) → ( 𝑘 · 𝑗 ) ∈ ℝ )
75 74 adantl ( ( ( 𝜑𝑡𝐷 ) ∧ ( 𝑘 ∈ ℝ ∧ 𝑗 ∈ ℝ ) ) → ( 𝑘 · 𝑗 ) ∈ ℝ )
76 39 73 75 seqcl ( ( 𝜑𝑡𝐷 ) → ( seq 1 ( · , ( 𝐹𝑡 ) ) ‘ 𝑀 ) ∈ ℝ )
77 7 fvmpt2 ( ( 𝑡𝑇 ∧ ( seq 1 ( · , ( 𝐹𝑡 ) ) ‘ 𝑀 ) ∈ ℝ ) → ( 𝑍𝑡 ) = ( seq 1 ( · , ( 𝐹𝑡 ) ) ‘ 𝑀 ) )
78 18 76 77 syl2anc ( ( 𝜑𝑡𝐷 ) → ( 𝑍𝑡 ) = ( seq 1 ( · , ( 𝐹𝑡 ) ) ‘ 𝑀 ) )
79 nfcv 𝑖 𝑇
80 nfmpt1 𝑖 ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝑈𝑖 ) ‘ 𝑡 ) )
81 79 80 nfmpt 𝑖 ( 𝑡𝑇 ↦ ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝑈𝑖 ) ‘ 𝑡 ) ) )
82 6 81 nfcxfr 𝑖 𝐹
83 nfcv 𝑖 𝑡
84 82 83 nffv 𝑖 ( 𝐹𝑡 )
85 nfv 𝑖 𝑡𝐷
86 1 85 nfan 𝑖 ( 𝜑𝑡𝐷 )
87 nfcv 𝑗 seq 1 ( · , ( 𝐹𝑡 ) )
88 eqid seq 1 ( · , ( 𝐹𝑡 ) ) = seq 1 ( · , ( 𝐹𝑡 ) )
89 8 adantr ( ( 𝜑𝑡𝐷 ) → 𝑀 ∈ ℕ )
90 simpll ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → 𝜑 )
91 simpr ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → 𝑖 ∈ ( 1 ... 𝑀 ) )
92 18 adantr ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → 𝑡𝑇 )
93 49 simprd ( ( 𝜑𝑖 ∈ ( 1 ... 𝑀 ) ) → ∀ 𝑡𝑇 ( 0 ≤ ( ( 𝑈𝑖 ) ‘ 𝑡 ) ∧ ( ( 𝑈𝑖 ) ‘ 𝑡 ) ≤ 1 ) )
94 93 r19.21bi ( ( ( 𝜑𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑡𝑇 ) → ( 0 ≤ ( ( 𝑈𝑖 ) ‘ 𝑡 ) ∧ ( ( 𝑈𝑖 ) ‘ 𝑡 ) ≤ 1 ) )
95 94 simpld ( ( ( 𝜑𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑡𝑇 ) → 0 ≤ ( ( 𝑈𝑖 ) ‘ 𝑡 ) )
96 90 91 92 95 syl21anc ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → 0 ≤ ( ( 𝑈𝑖 ) ‘ 𝑡 ) )
97 69 fveq1d ( ( 𝜑𝑡𝑇 ) → ( ( 𝐹𝑡 ) ‘ 𝑖 ) = ( ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝑈𝑖 ) ‘ 𝑡 ) ) ‘ 𝑖 ) )
98 90 92 97 syl2anc ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝐹𝑡 ) ‘ 𝑖 ) = ( ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝑈𝑖 ) ‘ 𝑡 ) ) ‘ 𝑖 ) )
99 90 92 91 61 syl21anc ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝑈𝑖 ) ‘ 𝑡 ) ∈ ℝ )
100 62 fvmpt2 ( ( 𝑖 ∈ ( 1 ... 𝑀 ) ∧ ( ( 𝑈𝑖 ) ‘ 𝑡 ) ∈ ℝ ) → ( ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝑈𝑖 ) ‘ 𝑡 ) ) ‘ 𝑖 ) = ( ( 𝑈𝑖 ) ‘ 𝑡 ) )
101 91 99 100 syl2anc ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝑈𝑖 ) ‘ 𝑡 ) ) ‘ 𝑖 ) = ( ( 𝑈𝑖 ) ‘ 𝑡 ) )
102 98 101 eqtrd ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝐹𝑡 ) ‘ 𝑖 ) = ( ( 𝑈𝑖 ) ‘ 𝑡 ) )
103 96 102 breqtrrd ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → 0 ≤ ( ( 𝐹𝑡 ) ‘ 𝑖 ) )
104 94 simprd ( ( ( 𝜑𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑡𝑇 ) → ( ( 𝑈𝑖 ) ‘ 𝑡 ) ≤ 1 )
105 90 91 92 104 syl21anc ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝑈𝑖 ) ‘ 𝑡 ) ≤ 1 )
106 102 105 eqbrtrd ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝐹𝑡 ) ‘ 𝑖 ) ≤ 1 )
107 17 adantr ( ( 𝜑𝑡𝐷 ) → 𝐸 ∈ ℝ+ )
108 11 sselda ( ( 𝜑𝑡𝐷 ) → 𝑡 ran 𝑊 )
109 eluni ( 𝑡 ran 𝑊 ↔ ∃ 𝑤 ( 𝑡𝑤𝑤 ∈ ran 𝑊 ) )
110 108 109 sylib ( ( 𝜑𝑡𝐷 ) → ∃ 𝑤 ( 𝑡𝑤𝑤 ∈ ran 𝑊 ) )
111 ffn ( 𝑊 : ( 1 ... 𝑀 ) ⟶ 𝑉𝑊 Fn ( 1 ... 𝑀 ) )
112 fvelrnb ( 𝑊 Fn ( 1 ... 𝑀 ) → ( 𝑤 ∈ ran 𝑊 ↔ ∃ 𝑗 ∈ ( 1 ... 𝑀 ) ( 𝑊𝑗 ) = 𝑤 ) )
113 9 111 112 3syl ( 𝜑 → ( 𝑤 ∈ ran 𝑊 ↔ ∃ 𝑗 ∈ ( 1 ... 𝑀 ) ( 𝑊𝑗 ) = 𝑤 ) )
114 113 biimpa ( ( 𝜑𝑤 ∈ ran 𝑊 ) → ∃ 𝑗 ∈ ( 1 ... 𝑀 ) ( 𝑊𝑗 ) = 𝑤 )
115 114 adantrl ( ( 𝜑 ∧ ( 𝑡𝑤𝑤 ∈ ran 𝑊 ) ) → ∃ 𝑗 ∈ ( 1 ... 𝑀 ) ( 𝑊𝑗 ) = 𝑤 )
116 simplr ( ( ( 𝜑𝑡𝑤 ) ∧ ( 𝑊𝑗 ) = 𝑤 ) → 𝑡𝑤 )
117 simpr ( ( ( 𝜑𝑡𝑤 ) ∧ ( 𝑊𝑗 ) = 𝑤 ) → ( 𝑊𝑗 ) = 𝑤 )
118 116 117 eleqtrrd ( ( ( 𝜑𝑡𝑤 ) ∧ ( 𝑊𝑗 ) = 𝑤 ) → 𝑡 ∈ ( 𝑊𝑗 ) )
119 118 ex ( ( 𝜑𝑡𝑤 ) → ( ( 𝑊𝑗 ) = 𝑤𝑡 ∈ ( 𝑊𝑗 ) ) )
120 119 reximdv ( ( 𝜑𝑡𝑤 ) → ( ∃ 𝑗 ∈ ( 1 ... 𝑀 ) ( 𝑊𝑗 ) = 𝑤 → ∃ 𝑗 ∈ ( 1 ... 𝑀 ) 𝑡 ∈ ( 𝑊𝑗 ) ) )
121 120 adantrr ( ( 𝜑 ∧ ( 𝑡𝑤𝑤 ∈ ran 𝑊 ) ) → ( ∃ 𝑗 ∈ ( 1 ... 𝑀 ) ( 𝑊𝑗 ) = 𝑤 → ∃ 𝑗 ∈ ( 1 ... 𝑀 ) 𝑡 ∈ ( 𝑊𝑗 ) ) )
122 115 121 mpd ( ( 𝜑 ∧ ( 𝑡𝑤𝑤 ∈ ran 𝑊 ) ) → ∃ 𝑗 ∈ ( 1 ... 𝑀 ) 𝑡 ∈ ( 𝑊𝑗 ) )
123 122 ex ( 𝜑 → ( ( 𝑡𝑤𝑤 ∈ ran 𝑊 ) → ∃ 𝑗 ∈ ( 1 ... 𝑀 ) 𝑡 ∈ ( 𝑊𝑗 ) ) )
124 123 exlimdv ( 𝜑 → ( ∃ 𝑤 ( 𝑡𝑤𝑤 ∈ ran 𝑊 ) → ∃ 𝑗 ∈ ( 1 ... 𝑀 ) 𝑡 ∈ ( 𝑊𝑗 ) ) )
125 124 adantr ( ( 𝜑𝑡𝐷 ) → ( ∃ 𝑤 ( 𝑡𝑤𝑤 ∈ ran 𝑊 ) → ∃ 𝑗 ∈ ( 1 ... 𝑀 ) 𝑡 ∈ ( 𝑊𝑗 ) ) )
126 110 125 mpd ( ( 𝜑𝑡𝐷 ) → ∃ 𝑗 ∈ ( 1 ... 𝑀 ) 𝑡 ∈ ( 𝑊𝑗 ) )
127 simplll ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑡 ∈ ( 𝑊𝑗 ) ) → 𝜑 )
128 simplr ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑡 ∈ ( 𝑊𝑗 ) ) → 𝑗 ∈ ( 1 ... 𝑀 ) )
129 simpr ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑡 ∈ ( 𝑊𝑗 ) ) → 𝑡 ∈ ( 𝑊𝑗 ) )
130 nfv 𝑖 𝑗 ∈ ( 1 ... 𝑀 )
131 nfv 𝑖 𝑡 ∈ ( 𝑊𝑗 )
132 1 130 131 nf3an 𝑖 ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ∧ 𝑡 ∈ ( 𝑊𝑗 ) )
133 nfv 𝑖 ( ( 𝑈𝑗 ) ‘ 𝑡 ) < 𝐸
134 132 133 nfim 𝑖 ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ∧ 𝑡 ∈ ( 𝑊𝑗 ) ) → ( ( 𝑈𝑗 ) ‘ 𝑡 ) < 𝐸 )
135 eleq1 ( 𝑖 = 𝑗 → ( 𝑖 ∈ ( 1 ... 𝑀 ) ↔ 𝑗 ∈ ( 1 ... 𝑀 ) ) )
136 fveq2 ( 𝑖 = 𝑗 → ( 𝑊𝑖 ) = ( 𝑊𝑗 ) )
137 136 eleq2d ( 𝑖 = 𝑗 → ( 𝑡 ∈ ( 𝑊𝑖 ) ↔ 𝑡 ∈ ( 𝑊𝑗 ) ) )
138 135 137 3anbi23d ( 𝑖 = 𝑗 → ( ( 𝜑𝑖 ∈ ( 1 ... 𝑀 ) ∧ 𝑡 ∈ ( 𝑊𝑖 ) ) ↔ ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ∧ 𝑡 ∈ ( 𝑊𝑗 ) ) ) )
139 fveq2 ( 𝑖 = 𝑗 → ( 𝑈𝑖 ) = ( 𝑈𝑗 ) )
140 139 fveq1d ( 𝑖 = 𝑗 → ( ( 𝑈𝑖 ) ‘ 𝑡 ) = ( ( 𝑈𝑗 ) ‘ 𝑡 ) )
141 140 breq1d ( 𝑖 = 𝑗 → ( ( ( 𝑈𝑖 ) ‘ 𝑡 ) < 𝐸 ↔ ( ( 𝑈𝑗 ) ‘ 𝑡 ) < 𝐸 ) )
142 138 141 imbi12d ( 𝑖 = 𝑗 → ( ( ( 𝜑𝑖 ∈ ( 1 ... 𝑀 ) ∧ 𝑡 ∈ ( 𝑊𝑖 ) ) → ( ( 𝑈𝑖 ) ‘ 𝑡 ) < 𝐸 ) ↔ ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ∧ 𝑡 ∈ ( 𝑊𝑗 ) ) → ( ( 𝑈𝑗 ) ‘ 𝑡 ) < 𝐸 ) ) )
143 13 r19.21bi ( ( ( 𝜑𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑡 ∈ ( 𝑊𝑖 ) ) → ( ( 𝑈𝑖 ) ‘ 𝑡 ) < 𝐸 )
144 143 3impa ( ( 𝜑𝑖 ∈ ( 1 ... 𝑀 ) ∧ 𝑡 ∈ ( 𝑊𝑖 ) ) → ( ( 𝑈𝑖 ) ‘ 𝑡 ) < 𝐸 )
145 134 142 144 chvarfv ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ∧ 𝑡 ∈ ( 𝑊𝑗 ) ) → ( ( 𝑈𝑗 ) ‘ 𝑡 ) < 𝐸 )
146 127 128 129 145 syl3anc ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑡 ∈ ( 𝑊𝑗 ) ) → ( ( 𝑈𝑗 ) ‘ 𝑡 ) < 𝐸 )
147 146 ex ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( 𝑡 ∈ ( 𝑊𝑗 ) → ( ( 𝑈𝑗 ) ‘ 𝑡 ) < 𝐸 ) )
148 147 reximdva ( ( 𝜑𝑡𝐷 ) → ( ∃ 𝑗 ∈ ( 1 ... 𝑀 ) 𝑡 ∈ ( 𝑊𝑗 ) → ∃ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑈𝑗 ) ‘ 𝑡 ) < 𝐸 ) )
149 126 148 mpd ( ( 𝜑𝑡𝐷 ) → ∃ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑈𝑗 ) ‘ 𝑡 ) < 𝐸 )
150 86 130 nfan 𝑖 ( ( 𝜑𝑡𝐷 ) ∧ 𝑗 ∈ ( 1 ... 𝑀 ) )
151 nfcv 𝑖 𝑗
152 84 151 nffv 𝑖 ( ( 𝐹𝑡 ) ‘ 𝑗 )
153 152 nfeq1 𝑖 ( ( 𝐹𝑡 ) ‘ 𝑗 ) = ( ( 𝑈𝑗 ) ‘ 𝑡 )
154 150 153 nfim 𝑖 ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝐹𝑡 ) ‘ 𝑗 ) = ( ( 𝑈𝑗 ) ‘ 𝑡 ) )
155 135 anbi2d ( 𝑖 = 𝑗 → ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) ↔ ( ( 𝜑𝑡𝐷 ) ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ) )
156 fveq2 ( 𝑖 = 𝑗 → ( ( 𝐹𝑡 ) ‘ 𝑖 ) = ( ( 𝐹𝑡 ) ‘ 𝑗 ) )
157 156 140 eqeq12d ( 𝑖 = 𝑗 → ( ( ( 𝐹𝑡 ) ‘ 𝑖 ) = ( ( 𝑈𝑖 ) ‘ 𝑡 ) ↔ ( ( 𝐹𝑡 ) ‘ 𝑗 ) = ( ( 𝑈𝑗 ) ‘ 𝑡 ) ) )
158 155 157 imbi12d ( 𝑖 = 𝑗 → ( ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝐹𝑡 ) ‘ 𝑖 ) = ( ( 𝑈𝑖 ) ‘ 𝑡 ) ) ↔ ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝐹𝑡 ) ‘ 𝑗 ) = ( ( 𝑈𝑗 ) ‘ 𝑡 ) ) ) )
159 154 158 102 chvarfv ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝐹𝑡 ) ‘ 𝑗 ) = ( ( 𝑈𝑗 ) ‘ 𝑡 ) )
160 159 breq1d ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( ( 𝐹𝑡 ) ‘ 𝑗 ) < 𝐸 ↔ ( ( 𝑈𝑗 ) ‘ 𝑡 ) < 𝐸 ) )
161 160 biimprd ( ( ( 𝜑𝑡𝐷 ) ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( ( 𝑈𝑗 ) ‘ 𝑡 ) < 𝐸 → ( ( 𝐹𝑡 ) ‘ 𝑗 ) < 𝐸 ) )
162 161 reximdva ( ( 𝜑𝑡𝐷 ) → ( ∃ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑈𝑗 ) ‘ 𝑡 ) < 𝐸 → ∃ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝐹𝑡 ) ‘ 𝑗 ) < 𝐸 ) )
163 149 162 mpd ( ( 𝜑𝑡𝐷 ) → ∃ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝐹𝑡 ) ‘ 𝑗 ) < 𝐸 )
164 84 86 87 88 89 72 103 106 107 163 fmul01lt1 ( ( 𝜑𝑡𝐷 ) → ( seq 1 ( · , ( 𝐹𝑡 ) ) ‘ 𝑀 ) < 𝐸 )
165 78 164 eqbrtrd ( ( 𝜑𝑡𝐷 ) → ( 𝑍𝑡 ) < 𝐸 )
166 36 165 eqbrtrd ( ( 𝜑𝑡𝐷 ) → ( 𝑋𝑡 ) < 𝐸 )
167 166 ex ( 𝜑 → ( 𝑡𝐷 → ( 𝑋𝑡 ) < 𝐸 ) )
168 2 167 ralrimi ( 𝜑 → ∀ 𝑡𝐷 ( 𝑋𝑡 ) < 𝐸 )