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 ⊢ ( 𝜑 → ∀ 𝑡 ∈ 𝐷 ( 𝑋 ‘ 𝑡 ) < 𝐸 )