# 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 ${⊢}Ⅎ{i}\phantom{\rule{.4em}{0ex}}{\phi }$
stoweidlem48.2 ${⊢}Ⅎ{t}\phantom{\rule{.4em}{0ex}}{\phi }$
stoweidlem48.3 ${⊢}{Y}=\left\{{h}\in {A}|\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {h}\left({t}\right)\wedge {h}\left({t}\right)\le 1\right)\right\}$
stoweidlem48.4 ${⊢}{P}=\left({f}\in {Y},{g}\in {Y}⟼\left({t}\in {T}⟼{f}\left({t}\right){g}\left({t}\right)\right)\right)$
stoweidlem48.5 ${⊢}{X}=seq1\left({P},{U}\right)\left({M}\right)$
stoweidlem48.6 ${⊢}{F}=\left({t}\in {T}⟼\left({i}\in \left(1\dots {M}\right)⟼{U}\left({i}\right)\left({t}\right)\right)\right)$
stoweidlem48.7 ${⊢}{Z}=\left({t}\in {T}⟼seq1\left(×,{F}\left({t}\right)\right)\left({M}\right)\right)$
stoweidlem48.8 ${⊢}{\phi }\to {M}\in ℕ$
stoweidlem48.9 ${⊢}{\phi }\to {W}:\left(1\dots {M}\right)⟶{V}$
stoweidlem48.10 ${⊢}{\phi }\to {U}:\left(1\dots {M}\right)⟶{Y}$
stoweidlem48.11 ${⊢}{\phi }\to {D}\subseteq \bigcup \mathrm{ran}{W}$
stoweidlem48.12 ${⊢}{\phi }\to {D}\subseteq {T}$
stoweidlem48.13 ${⊢}\left({\phi }\wedge {i}\in \left(1\dots {M}\right)\right)\to \forall {t}\in {W}\left({i}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)\left({t}\right)<{E}$
stoweidlem48.14 ${⊢}{\phi }\to {T}\in \mathrm{V}$
stoweidlem48.15 ${⊢}\left({\phi }\wedge {f}\in {A}\right)\to {f}:{T}⟶ℝ$
stoweidlem48.16 ${⊢}\left({\phi }\wedge {f}\in {A}\wedge {g}\in {A}\right)\to \left({t}\in {T}⟼{f}\left({t}\right){g}\left({t}\right)\right)\in {A}$
stoweidlem48.17 ${⊢}{\phi }\to {E}\in {ℝ}^{+}$
Assertion stoweidlem48 ${⊢}{\phi }\to \forall {t}\in {D}\phantom{\rule{.4em}{0ex}}{X}\left({t}\right)<{E}$

### Proof

Step Hyp Ref Expression
1 stoweidlem48.1 ${⊢}Ⅎ{i}\phantom{\rule{.4em}{0ex}}{\phi }$
2 stoweidlem48.2 ${⊢}Ⅎ{t}\phantom{\rule{.4em}{0ex}}{\phi }$
3 stoweidlem48.3 ${⊢}{Y}=\left\{{h}\in {A}|\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {h}\left({t}\right)\wedge {h}\left({t}\right)\le 1\right)\right\}$
4 stoweidlem48.4 ${⊢}{P}=\left({f}\in {Y},{g}\in {Y}⟼\left({t}\in {T}⟼{f}\left({t}\right){g}\left({t}\right)\right)\right)$
5 stoweidlem48.5 ${⊢}{X}=seq1\left({P},{U}\right)\left({M}\right)$
6 stoweidlem48.6 ${⊢}{F}=\left({t}\in {T}⟼\left({i}\in \left(1\dots {M}\right)⟼{U}\left({i}\right)\left({t}\right)\right)\right)$
7 stoweidlem48.7 ${⊢}{Z}=\left({t}\in {T}⟼seq1\left(×,{F}\left({t}\right)\right)\left({M}\right)\right)$
8 stoweidlem48.8 ${⊢}{\phi }\to {M}\in ℕ$
9 stoweidlem48.9 ${⊢}{\phi }\to {W}:\left(1\dots {M}\right)⟶{V}$
10 stoweidlem48.10 ${⊢}{\phi }\to {U}:\left(1\dots {M}\right)⟶{Y}$
11 stoweidlem48.11 ${⊢}{\phi }\to {D}\subseteq \bigcup \mathrm{ran}{W}$
12 stoweidlem48.12 ${⊢}{\phi }\to {D}\subseteq {T}$
13 stoweidlem48.13 ${⊢}\left({\phi }\wedge {i}\in \left(1\dots {M}\right)\right)\to \forall {t}\in {W}\left({i}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)\left({t}\right)<{E}$
14 stoweidlem48.14 ${⊢}{\phi }\to {T}\in \mathrm{V}$
15 stoweidlem48.15 ${⊢}\left({\phi }\wedge {f}\in {A}\right)\to {f}:{T}⟶ℝ$
16 stoweidlem48.16 ${⊢}\left({\phi }\wedge {f}\in {A}\wedge {g}\in {A}\right)\to \left({t}\in {T}⟼{f}\left({t}\right){g}\left({t}\right)\right)\in {A}$
17 stoweidlem48.17 ${⊢}{\phi }\to {E}\in {ℝ}^{+}$
18 12 sselda ${⊢}\left({\phi }\wedge {t}\in {D}\right)\to {t}\in {T}$
19 nfra1 ${⊢}Ⅎ{t}\phantom{\rule{.4em}{0ex}}\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {h}\left({t}\right)\wedge {h}\left({t}\right)\le 1\right)$
20 nfcv ${⊢}\underset{_}{Ⅎ}{t}\phantom{\rule{.4em}{0ex}}{A}$
21 19 20 nfrabw ${⊢}\underset{_}{Ⅎ}{t}\phantom{\rule{.4em}{0ex}}\left\{{h}\in {A}|\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {h}\left({t}\right)\wedge {h}\left({t}\right)\le 1\right)\right\}$
22 3 21 nfcxfr ${⊢}\underset{_}{Ⅎ}{t}\phantom{\rule{.4em}{0ex}}{Y}$
23 3 eleq2i ${⊢}{f}\in {Y}↔{f}\in \left\{{h}\in {A}|\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {h}\left({t}\right)\wedge {h}\left({t}\right)\le 1\right)\right\}$
24 fveq1 ${⊢}{h}={f}\to {h}\left({t}\right)={f}\left({t}\right)$
25 24 breq2d ${⊢}{h}={f}\to \left(0\le {h}\left({t}\right)↔0\le {f}\left({t}\right)\right)$
26 24 breq1d ${⊢}{h}={f}\to \left({h}\left({t}\right)\le 1↔{f}\left({t}\right)\le 1\right)$
27 25 26 anbi12d ${⊢}{h}={f}\to \left(\left(0\le {h}\left({t}\right)\wedge {h}\left({t}\right)\le 1\right)↔\left(0\le {f}\left({t}\right)\wedge {f}\left({t}\right)\le 1\right)\right)$
28 27 ralbidv ${⊢}{h}={f}\to \left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {h}\left({t}\right)\wedge {h}\left({t}\right)\le 1\right)↔\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {f}\left({t}\right)\wedge {f}\left({t}\right)\le 1\right)\right)$
29 28 elrab ${⊢}{f}\in \left\{{h}\in {A}|\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {h}\left({t}\right)\wedge {h}\left({t}\right)\le 1\right)\right\}↔\left({f}\in {A}\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {f}\left({t}\right)\wedge {f}\left({t}\right)\le 1\right)\right)$
30 23 29 sylbb ${⊢}{f}\in {Y}\to \left({f}\in {A}\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {f}\left({t}\right)\wedge {f}\left({t}\right)\le 1\right)\right)$
31 30 simpld ${⊢}{f}\in {Y}\to {f}\in {A}$
32 31 15 sylan2 ${⊢}\left({\phi }\wedge {f}\in {Y}\right)\to {f}:{T}⟶ℝ$
33 eqid ${⊢}\left({t}\in {T}⟼{f}\left({t}\right){g}\left({t}\right)\right)=\left({t}\in {T}⟼{f}\left({t}\right){g}\left({t}\right)\right)$
34 2 3 33 15 16 stoweidlem16 ${⊢}\left({\phi }\wedge {f}\in {Y}\wedge {g}\in {Y}\right)\to \left({t}\in {T}⟼{f}\left({t}\right){g}\left({t}\right)\right)\in {Y}$
35 1 22 4 5 6 7 14 8 10 32 34 fmuldfeq ${⊢}\left({\phi }\wedge {t}\in {T}\right)\to {X}\left({t}\right)={Z}\left({t}\right)$
36 18 35 syldan ${⊢}\left({\phi }\wedge {t}\in {D}\right)\to {X}\left({t}\right)={Z}\left({t}\right)$
37 elnnuz ${⊢}{M}\in ℕ↔{M}\in {ℤ}_{\ge 1}$
38 8 37 sylib ${⊢}{\phi }\to {M}\in {ℤ}_{\ge 1}$
39 38 adantr ${⊢}\left({\phi }\wedge {t}\in {D}\right)\to {M}\in {ℤ}_{\ge 1}$
40 nfv ${⊢}Ⅎ{i}\phantom{\rule{.4em}{0ex}}{t}\in {T}$
41 1 40 nfan ${⊢}Ⅎ{i}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {t}\in {T}\right)$
42 10 ffvelrnda ${⊢}\left({\phi }\wedge {i}\in \left(1\dots {M}\right)\right)\to {U}\left({i}\right)\in {Y}$
43 fveq1 ${⊢}{h}={U}\left({i}\right)\to {h}\left({t}\right)={U}\left({i}\right)\left({t}\right)$
44 43 breq2d ${⊢}{h}={U}\left({i}\right)\to \left(0\le {h}\left({t}\right)↔0\le {U}\left({i}\right)\left({t}\right)\right)$
45 43 breq1d ${⊢}{h}={U}\left({i}\right)\to \left({h}\left({t}\right)\le 1↔{U}\left({i}\right)\left({t}\right)\le 1\right)$
46 44 45 anbi12d ${⊢}{h}={U}\left({i}\right)\to \left(\left(0\le {h}\left({t}\right)\wedge {h}\left({t}\right)\le 1\right)↔\left(0\le {U}\left({i}\right)\left({t}\right)\wedge {U}\left({i}\right)\left({t}\right)\le 1\right)\right)$
47 46 ralbidv ${⊢}{h}={U}\left({i}\right)\to \left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {h}\left({t}\right)\wedge {h}\left({t}\right)\le 1\right)↔\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {U}\left({i}\right)\left({t}\right)\wedge {U}\left({i}\right)\left({t}\right)\le 1\right)\right)$
48 47 3 elrab2 ${⊢}{U}\left({i}\right)\in {Y}↔\left({U}\left({i}\right)\in {A}\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {U}\left({i}\right)\left({t}\right)\wedge {U}\left({i}\right)\left({t}\right)\le 1\right)\right)$
49 42 48 sylib ${⊢}\left({\phi }\wedge {i}\in \left(1\dots {M}\right)\right)\to \left({U}\left({i}\right)\in {A}\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {U}\left({i}\right)\left({t}\right)\wedge {U}\left({i}\right)\left({t}\right)\le 1\right)\right)$
50 49 simpld ${⊢}\left({\phi }\wedge {i}\in \left(1\dots {M}\right)\right)\to {U}\left({i}\right)\in {A}$
51 simpl ${⊢}\left({\phi }\wedge {i}\in \left(1\dots {M}\right)\right)\to {\phi }$
52 51 50 jca ${⊢}\left({\phi }\wedge {i}\in \left(1\dots {M}\right)\right)\to \left({\phi }\wedge {U}\left({i}\right)\in {A}\right)$
53 eleq1 ${⊢}{f}={U}\left({i}\right)\to \left({f}\in {A}↔{U}\left({i}\right)\in {A}\right)$
54 53 anbi2d ${⊢}{f}={U}\left({i}\right)\to \left(\left({\phi }\wedge {f}\in {A}\right)↔\left({\phi }\wedge {U}\left({i}\right)\in {A}\right)\right)$
55 feq1 ${⊢}{f}={U}\left({i}\right)\to \left({f}:{T}⟶ℝ↔{U}\left({i}\right):{T}⟶ℝ\right)$
56 54 55 imbi12d ${⊢}{f}={U}\left({i}\right)\to \left(\left(\left({\phi }\wedge {f}\in {A}\right)\to {f}:{T}⟶ℝ\right)↔\left(\left({\phi }\wedge {U}\left({i}\right)\in {A}\right)\to {U}\left({i}\right):{T}⟶ℝ\right)\right)$
57 56 15 vtoclg ${⊢}{U}\left({i}\right)\in {A}\to \left(\left({\phi }\wedge {U}\left({i}\right)\in {A}\right)\to {U}\left({i}\right):{T}⟶ℝ\right)$
58 50 52 57 sylc ${⊢}\left({\phi }\wedge {i}\in \left(1\dots {M}\right)\right)\to {U}\left({i}\right):{T}⟶ℝ$
59 58 adantlr ${⊢}\left(\left({\phi }\wedge {t}\in {T}\right)\wedge {i}\in \left(1\dots {M}\right)\right)\to {U}\left({i}\right):{T}⟶ℝ$
60 simplr ${⊢}\left(\left({\phi }\wedge {t}\in {T}\right)\wedge {i}\in \left(1\dots {M}\right)\right)\to {t}\in {T}$
61 59 60 ffvelrnd ${⊢}\left(\left({\phi }\wedge {t}\in {T}\right)\wedge {i}\in \left(1\dots {M}\right)\right)\to {U}\left({i}\right)\left({t}\right)\in ℝ$
62 eqid ${⊢}\left({i}\in \left(1\dots {M}\right)⟼{U}\left({i}\right)\left({t}\right)\right)=\left({i}\in \left(1\dots {M}\right)⟼{U}\left({i}\right)\left({t}\right)\right)$
63 41 61 62 fmptdf ${⊢}\left({\phi }\wedge {t}\in {T}\right)\to \left({i}\in \left(1\dots {M}\right)⟼{U}\left({i}\right)\left({t}\right)\right):\left(1\dots {M}\right)⟶ℝ$
64 simpr ${⊢}\left({\phi }\wedge {t}\in {T}\right)\to {t}\in {T}$
65 ovex ${⊢}\left(1\dots {M}\right)\in \mathrm{V}$
66 mptexg ${⊢}\left(1\dots {M}\right)\in \mathrm{V}\to \left({i}\in \left(1\dots {M}\right)⟼{U}\left({i}\right)\left({t}\right)\right)\in \mathrm{V}$
67 65 66 mp1i ${⊢}\left({\phi }\wedge {t}\in {T}\right)\to \left({i}\in \left(1\dots {M}\right)⟼{U}\left({i}\right)\left({t}\right)\right)\in \mathrm{V}$
68 6 fvmpt2 ${⊢}\left({t}\in {T}\wedge \left({i}\in \left(1\dots {M}\right)⟼{U}\left({i}\right)\left({t}\right)\right)\in \mathrm{V}\right)\to {F}\left({t}\right)=\left({i}\in \left(1\dots {M}\right)⟼{U}\left({i}\right)\left({t}\right)\right)$
69 64 67 68 syl2anc ${⊢}\left({\phi }\wedge {t}\in {T}\right)\to {F}\left({t}\right)=\left({i}\in \left(1\dots {M}\right)⟼{U}\left({i}\right)\left({t}\right)\right)$
70 69 feq1d ${⊢}\left({\phi }\wedge {t}\in {T}\right)\to \left({F}\left({t}\right):\left(1\dots {M}\right)⟶ℝ↔\left({i}\in \left(1\dots {M}\right)⟼{U}\left({i}\right)\left({t}\right)\right):\left(1\dots {M}\right)⟶ℝ\right)$
71 63 70 mpbird ${⊢}\left({\phi }\wedge {t}\in {T}\right)\to {F}\left({t}\right):\left(1\dots {M}\right)⟶ℝ$
72 18 71 syldan ${⊢}\left({\phi }\wedge {t}\in {D}\right)\to {F}\left({t}\right):\left(1\dots {M}\right)⟶ℝ$
73 72 ffvelrnda ${⊢}\left(\left({\phi }\wedge {t}\in {D}\right)\wedge {k}\in \left(1\dots {M}\right)\right)\to {F}\left({t}\right)\left({k}\right)\in ℝ$
74 remulcl ${⊢}\left({k}\in ℝ\wedge {j}\in ℝ\right)\to {k}{j}\in ℝ$
75 74 adantl ${⊢}\left(\left({\phi }\wedge {t}\in {D}\right)\wedge \left({k}\in ℝ\wedge {j}\in ℝ\right)\right)\to {k}{j}\in ℝ$
76 39 73 75 seqcl ${⊢}\left({\phi }\wedge {t}\in {D}\right)\to seq1\left(×,{F}\left({t}\right)\right)\left({M}\right)\in ℝ$
77 7 fvmpt2 ${⊢}\left({t}\in {T}\wedge seq1\left(×,{F}\left({t}\right)\right)\left({M}\right)\in ℝ\right)\to {Z}\left({t}\right)=seq1\left(×,{F}\left({t}\right)\right)\left({M}\right)$
78 18 76 77 syl2anc ${⊢}\left({\phi }\wedge {t}\in {D}\right)\to {Z}\left({t}\right)=seq1\left(×,{F}\left({t}\right)\right)\left({M}\right)$
79 nfcv ${⊢}\underset{_}{Ⅎ}{i}\phantom{\rule{.4em}{0ex}}{T}$
80 nfmpt1 ${⊢}\underset{_}{Ⅎ}{i}\phantom{\rule{.4em}{0ex}}\left({i}\in \left(1\dots {M}\right)⟼{U}\left({i}\right)\left({t}\right)\right)$
81 79 80 nfmpt ${⊢}\underset{_}{Ⅎ}{i}\phantom{\rule{.4em}{0ex}}\left({t}\in {T}⟼\left({i}\in \left(1\dots {M}\right)⟼{U}\left({i}\right)\left({t}\right)\right)\right)$
82 6 81 nfcxfr ${⊢}\underset{_}{Ⅎ}{i}\phantom{\rule{.4em}{0ex}}{F}$
83 nfcv ${⊢}\underset{_}{Ⅎ}{i}\phantom{\rule{.4em}{0ex}}{t}$
84 82 83 nffv ${⊢}\underset{_}{Ⅎ}{i}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)$
85 nfv ${⊢}Ⅎ{i}\phantom{\rule{.4em}{0ex}}{t}\in {D}$
86 1 85 nfan ${⊢}Ⅎ{i}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {t}\in {D}\right)$
87 nfcv ${⊢}\underset{_}{Ⅎ}{j}\phantom{\rule{.4em}{0ex}}seq1\left(×,{F}\left({t}\right)\right)$
88 eqid ${⊢}seq1\left(×,{F}\left({t}\right)\right)=seq1\left(×,{F}\left({t}\right)\right)$
89 8 adantr ${⊢}\left({\phi }\wedge {t}\in {D}\right)\to {M}\in ℕ$
90 simpll ${⊢}\left(\left({\phi }\wedge {t}\in {D}\right)\wedge {i}\in \left(1\dots {M}\right)\right)\to {\phi }$
91 simpr ${⊢}\left(\left({\phi }\wedge {t}\in {D}\right)\wedge {i}\in \left(1\dots {M}\right)\right)\to {i}\in \left(1\dots {M}\right)$
92 18 adantr ${⊢}\left(\left({\phi }\wedge {t}\in {D}\right)\wedge {i}\in \left(1\dots {M}\right)\right)\to {t}\in {T}$
93 49 simprd ${⊢}\left({\phi }\wedge {i}\in \left(1\dots {M}\right)\right)\to \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {U}\left({i}\right)\left({t}\right)\wedge {U}\left({i}\right)\left({t}\right)\le 1\right)$
94 93 r19.21bi ${⊢}\left(\left({\phi }\wedge {i}\in \left(1\dots {M}\right)\right)\wedge {t}\in {T}\right)\to \left(0\le {U}\left({i}\right)\left({t}\right)\wedge {U}\left({i}\right)\left({t}\right)\le 1\right)$
95 94 simpld ${⊢}\left(\left({\phi }\wedge {i}\in \left(1\dots {M}\right)\right)\wedge {t}\in {T}\right)\to 0\le {U}\left({i}\right)\left({t}\right)$
96 90 91 92 95 syl21anc ${⊢}\left(\left({\phi }\wedge {t}\in {D}\right)\wedge {i}\in \left(1\dots {M}\right)\right)\to 0\le {U}\left({i}\right)\left({t}\right)$
97 69 fveq1d ${⊢}\left({\phi }\wedge {t}\in {T}\right)\to {F}\left({t}\right)\left({i}\right)=\left({i}\in \left(1\dots {M}\right)⟼{U}\left({i}\right)\left({t}\right)\right)\left({i}\right)$
98 90 92 97 syl2anc ${⊢}\left(\left({\phi }\wedge {t}\in {D}\right)\wedge {i}\in \left(1\dots {M}\right)\right)\to {F}\left({t}\right)\left({i}\right)=\left({i}\in \left(1\dots {M}\right)⟼{U}\left({i}\right)\left({t}\right)\right)\left({i}\right)$
99 90 92 91 61 syl21anc ${⊢}\left(\left({\phi }\wedge {t}\in {D}\right)\wedge {i}\in \left(1\dots {M}\right)\right)\to {U}\left({i}\right)\left({t}\right)\in ℝ$
100 62 fvmpt2 ${⊢}\left({i}\in \left(1\dots {M}\right)\wedge {U}\left({i}\right)\left({t}\right)\in ℝ\right)\to \left({i}\in \left(1\dots {M}\right)⟼{U}\left({i}\right)\left({t}\right)\right)\left({i}\right)={U}\left({i}\right)\left({t}\right)$
101 91 99 100 syl2anc ${⊢}\left(\left({\phi }\wedge {t}\in {D}\right)\wedge {i}\in \left(1\dots {M}\right)\right)\to \left({i}\in \left(1\dots {M}\right)⟼{U}\left({i}\right)\left({t}\right)\right)\left({i}\right)={U}\left({i}\right)\left({t}\right)$
102 98 101 eqtrd ${⊢}\left(\left({\phi }\wedge {t}\in {D}\right)\wedge {i}\in \left(1\dots {M}\right)\right)\to {F}\left({t}\right)\left({i}\right)={U}\left({i}\right)\left({t}\right)$
103 96 102 breqtrrd ${⊢}\left(\left({\phi }\wedge {t}\in {D}\right)\wedge {i}\in \left(1\dots {M}\right)\right)\to 0\le {F}\left({t}\right)\left({i}\right)$
104 94 simprd ${⊢}\left(\left({\phi }\wedge {i}\in \left(1\dots {M}\right)\right)\wedge {t}\in {T}\right)\to {U}\left({i}\right)\left({t}\right)\le 1$
105 90 91 92 104 syl21anc ${⊢}\left(\left({\phi }\wedge {t}\in {D}\right)\wedge {i}\in \left(1\dots {M}\right)\right)\to {U}\left({i}\right)\left({t}\right)\le 1$
106 102 105 eqbrtrd ${⊢}\left(\left({\phi }\wedge {t}\in {D}\right)\wedge {i}\in \left(1\dots {M}\right)\right)\to {F}\left({t}\right)\left({i}\right)\le 1$
107 17 adantr ${⊢}\left({\phi }\wedge {t}\in {D}\right)\to {E}\in {ℝ}^{+}$
108 11 sselda ${⊢}\left({\phi }\wedge {t}\in {D}\right)\to {t}\in \bigcup \mathrm{ran}{W}$
109 eluni ${⊢}{t}\in \bigcup \mathrm{ran}{W}↔\exists {w}\phantom{\rule{.4em}{0ex}}\left({t}\in {w}\wedge {w}\in \mathrm{ran}{W}\right)$
110 108 109 sylib ${⊢}\left({\phi }\wedge {t}\in {D}\right)\to \exists {w}\phantom{\rule{.4em}{0ex}}\left({t}\in {w}\wedge {w}\in \mathrm{ran}{W}\right)$
111 ffn ${⊢}{W}:\left(1\dots {M}\right)⟶{V}\to {W}Fn\left(1\dots {M}\right)$
112 fvelrnb ${⊢}{W}Fn\left(1\dots {M}\right)\to \left({w}\in \mathrm{ran}{W}↔\exists {j}\in \left(1\dots {M}\right)\phantom{\rule{.4em}{0ex}}{W}\left({j}\right)={w}\right)$
113 9 111 112 3syl ${⊢}{\phi }\to \left({w}\in \mathrm{ran}{W}↔\exists {j}\in \left(1\dots {M}\right)\phantom{\rule{.4em}{0ex}}{W}\left({j}\right)={w}\right)$
114 113 biimpa ${⊢}\left({\phi }\wedge {w}\in \mathrm{ran}{W}\right)\to \exists {j}\in \left(1\dots {M}\right)\phantom{\rule{.4em}{0ex}}{W}\left({j}\right)={w}$
115 114 adantrl ${⊢}\left({\phi }\wedge \left({t}\in {w}\wedge {w}\in \mathrm{ran}{W}\right)\right)\to \exists {j}\in \left(1\dots {M}\right)\phantom{\rule{.4em}{0ex}}{W}\left({j}\right)={w}$
116 simplr ${⊢}\left(\left({\phi }\wedge {t}\in {w}\right)\wedge {W}\left({j}\right)={w}\right)\to {t}\in {w}$
117 simpr ${⊢}\left(\left({\phi }\wedge {t}\in {w}\right)\wedge {W}\left({j}\right)={w}\right)\to {W}\left({j}\right)={w}$
118 116 117 eleqtrrd ${⊢}\left(\left({\phi }\wedge {t}\in {w}\right)\wedge {W}\left({j}\right)={w}\right)\to {t}\in {W}\left({j}\right)$
119 118 ex ${⊢}\left({\phi }\wedge {t}\in {w}\right)\to \left({W}\left({j}\right)={w}\to {t}\in {W}\left({j}\right)\right)$
120 119 reximdv ${⊢}\left({\phi }\wedge {t}\in {w}\right)\to \left(\exists {j}\in \left(1\dots {M}\right)\phantom{\rule{.4em}{0ex}}{W}\left({j}\right)={w}\to \exists {j}\in \left(1\dots {M}\right)\phantom{\rule{.4em}{0ex}}{t}\in {W}\left({j}\right)\right)$
121 120 adantrr ${⊢}\left({\phi }\wedge \left({t}\in {w}\wedge {w}\in \mathrm{ran}{W}\right)\right)\to \left(\exists {j}\in \left(1\dots {M}\right)\phantom{\rule{.4em}{0ex}}{W}\left({j}\right)={w}\to \exists {j}\in \left(1\dots {M}\right)\phantom{\rule{.4em}{0ex}}{t}\in {W}\left({j}\right)\right)$
122 115 121 mpd ${⊢}\left({\phi }\wedge \left({t}\in {w}\wedge {w}\in \mathrm{ran}{W}\right)\right)\to \exists {j}\in \left(1\dots {M}\right)\phantom{\rule{.4em}{0ex}}{t}\in {W}\left({j}\right)$
123 122 ex ${⊢}{\phi }\to \left(\left({t}\in {w}\wedge {w}\in \mathrm{ran}{W}\right)\to \exists {j}\in \left(1\dots {M}\right)\phantom{\rule{.4em}{0ex}}{t}\in {W}\left({j}\right)\right)$
124 123 exlimdv ${⊢}{\phi }\to \left(\exists {w}\phantom{\rule{.4em}{0ex}}\left({t}\in {w}\wedge {w}\in \mathrm{ran}{W}\right)\to \exists {j}\in \left(1\dots {M}\right)\phantom{\rule{.4em}{0ex}}{t}\in {W}\left({j}\right)\right)$
125 124 adantr ${⊢}\left({\phi }\wedge {t}\in {D}\right)\to \left(\exists {w}\phantom{\rule{.4em}{0ex}}\left({t}\in {w}\wedge {w}\in \mathrm{ran}{W}\right)\to \exists {j}\in \left(1\dots {M}\right)\phantom{\rule{.4em}{0ex}}{t}\in {W}\left({j}\right)\right)$
126 110 125 mpd ${⊢}\left({\phi }\wedge {t}\in {D}\right)\to \exists {j}\in \left(1\dots {M}\right)\phantom{\rule{.4em}{0ex}}{t}\in {W}\left({j}\right)$
127 simplll ${⊢}\left(\left(\left({\phi }\wedge {t}\in {D}\right)\wedge {j}\in \left(1\dots {M}\right)\right)\wedge {t}\in {W}\left({j}\right)\right)\to {\phi }$
128 simplr ${⊢}\left(\left(\left({\phi }\wedge {t}\in {D}\right)\wedge {j}\in \left(1\dots {M}\right)\right)\wedge {t}\in {W}\left({j}\right)\right)\to {j}\in \left(1\dots {M}\right)$
129 simpr ${⊢}\left(\left(\left({\phi }\wedge {t}\in {D}\right)\wedge {j}\in \left(1\dots {M}\right)\right)\wedge {t}\in {W}\left({j}\right)\right)\to {t}\in {W}\left({j}\right)$
130 nfv ${⊢}Ⅎ{i}\phantom{\rule{.4em}{0ex}}{j}\in \left(1\dots {M}\right)$
131 nfv ${⊢}Ⅎ{i}\phantom{\rule{.4em}{0ex}}{t}\in {W}\left({j}\right)$
132 1 130 131 nf3an ${⊢}Ⅎ{i}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\wedge {t}\in {W}\left({j}\right)\right)$
133 nfv ${⊢}Ⅎ{i}\phantom{\rule{.4em}{0ex}}{U}\left({j}\right)\left({t}\right)<{E}$
134 132 133 nfim ${⊢}Ⅎ{i}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\wedge {t}\in {W}\left({j}\right)\right)\to {U}\left({j}\right)\left({t}\right)<{E}\right)$
135 eleq1 ${⊢}{i}={j}\to \left({i}\in \left(1\dots {M}\right)↔{j}\in \left(1\dots {M}\right)\right)$
136 fveq2 ${⊢}{i}={j}\to {W}\left({i}\right)={W}\left({j}\right)$
137 136 eleq2d ${⊢}{i}={j}\to \left({t}\in {W}\left({i}\right)↔{t}\in {W}\left({j}\right)\right)$
138 135 137 3anbi23d ${⊢}{i}={j}\to \left(\left({\phi }\wedge {i}\in \left(1\dots {M}\right)\wedge {t}\in {W}\left({i}\right)\right)↔\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\wedge {t}\in {W}\left({j}\right)\right)\right)$
139 fveq2 ${⊢}{i}={j}\to {U}\left({i}\right)={U}\left({j}\right)$
140 139 fveq1d ${⊢}{i}={j}\to {U}\left({i}\right)\left({t}\right)={U}\left({j}\right)\left({t}\right)$
141 140 breq1d ${⊢}{i}={j}\to \left({U}\left({i}\right)\left({t}\right)<{E}↔{U}\left({j}\right)\left({t}\right)<{E}\right)$
142 138 141 imbi12d ${⊢}{i}={j}\to \left(\left(\left({\phi }\wedge {i}\in \left(1\dots {M}\right)\wedge {t}\in {W}\left({i}\right)\right)\to {U}\left({i}\right)\left({t}\right)<{E}\right)↔\left(\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\wedge {t}\in {W}\left({j}\right)\right)\to {U}\left({j}\right)\left({t}\right)<{E}\right)\right)$
143 13 r19.21bi ${⊢}\left(\left({\phi }\wedge {i}\in \left(1\dots {M}\right)\right)\wedge {t}\in {W}\left({i}\right)\right)\to {U}\left({i}\right)\left({t}\right)<{E}$
144 143 3impa ${⊢}\left({\phi }\wedge {i}\in \left(1\dots {M}\right)\wedge {t}\in {W}\left({i}\right)\right)\to {U}\left({i}\right)\left({t}\right)<{E}$
145 134 142 144 chvarfv ${⊢}\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\wedge {t}\in {W}\left({j}\right)\right)\to {U}\left({j}\right)\left({t}\right)<{E}$
146 127 128 129 145 syl3anc ${⊢}\left(\left(\left({\phi }\wedge {t}\in {D}\right)\wedge {j}\in \left(1\dots {M}\right)\right)\wedge {t}\in {W}\left({j}\right)\right)\to {U}\left({j}\right)\left({t}\right)<{E}$
147 146 ex ${⊢}\left(\left({\phi }\wedge {t}\in {D}\right)\wedge {j}\in \left(1\dots {M}\right)\right)\to \left({t}\in {W}\left({j}\right)\to {U}\left({j}\right)\left({t}\right)<{E}\right)$
148 147 reximdva ${⊢}\left({\phi }\wedge {t}\in {D}\right)\to \left(\exists {j}\in \left(1\dots {M}\right)\phantom{\rule{.4em}{0ex}}{t}\in {W}\left({j}\right)\to \exists {j}\in \left(1\dots {M}\right)\phantom{\rule{.4em}{0ex}}{U}\left({j}\right)\left({t}\right)<{E}\right)$
149 126 148 mpd ${⊢}\left({\phi }\wedge {t}\in {D}\right)\to \exists {j}\in \left(1\dots {M}\right)\phantom{\rule{.4em}{0ex}}{U}\left({j}\right)\left({t}\right)<{E}$
150 86 130 nfan ${⊢}Ⅎ{i}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge {t}\in {D}\right)\wedge {j}\in \left(1\dots {M}\right)\right)$
151 nfcv ${⊢}\underset{_}{Ⅎ}{i}\phantom{\rule{.4em}{0ex}}{j}$
152 84 151 nffv ${⊢}\underset{_}{Ⅎ}{i}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)\left({j}\right)$
153 152 nfeq1 ${⊢}Ⅎ{i}\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)\left({j}\right)={U}\left({j}\right)\left({t}\right)$
154 150 153 nfim ${⊢}Ⅎ{i}\phantom{\rule{.4em}{0ex}}\left(\left(\left({\phi }\wedge {t}\in {D}\right)\wedge {j}\in \left(1\dots {M}\right)\right)\to {F}\left({t}\right)\left({j}\right)={U}\left({j}\right)\left({t}\right)\right)$
155 135 anbi2d ${⊢}{i}={j}\to \left(\left(\left({\phi }\wedge {t}\in {D}\right)\wedge {i}\in \left(1\dots {M}\right)\right)↔\left(\left({\phi }\wedge {t}\in {D}\right)\wedge {j}\in \left(1\dots {M}\right)\right)\right)$
156 fveq2 ${⊢}{i}={j}\to {F}\left({t}\right)\left({i}\right)={F}\left({t}\right)\left({j}\right)$
157 156 140 eqeq12d ${⊢}{i}={j}\to \left({F}\left({t}\right)\left({i}\right)={U}\left({i}\right)\left({t}\right)↔{F}\left({t}\right)\left({j}\right)={U}\left({j}\right)\left({t}\right)\right)$
158 155 157 imbi12d ${⊢}{i}={j}\to \left(\left(\left(\left({\phi }\wedge {t}\in {D}\right)\wedge {i}\in \left(1\dots {M}\right)\right)\to {F}\left({t}\right)\left({i}\right)={U}\left({i}\right)\left({t}\right)\right)↔\left(\left(\left({\phi }\wedge {t}\in {D}\right)\wedge {j}\in \left(1\dots {M}\right)\right)\to {F}\left({t}\right)\left({j}\right)={U}\left({j}\right)\left({t}\right)\right)\right)$
159 154 158 102 chvarfv ${⊢}\left(\left({\phi }\wedge {t}\in {D}\right)\wedge {j}\in \left(1\dots {M}\right)\right)\to {F}\left({t}\right)\left({j}\right)={U}\left({j}\right)\left({t}\right)$
160 159 breq1d ${⊢}\left(\left({\phi }\wedge {t}\in {D}\right)\wedge {j}\in \left(1\dots {M}\right)\right)\to \left({F}\left({t}\right)\left({j}\right)<{E}↔{U}\left({j}\right)\left({t}\right)<{E}\right)$
161 160 biimprd ${⊢}\left(\left({\phi }\wedge {t}\in {D}\right)\wedge {j}\in \left(1\dots {M}\right)\right)\to \left({U}\left({j}\right)\left({t}\right)<{E}\to {F}\left({t}\right)\left({j}\right)<{E}\right)$
162 161 reximdva ${⊢}\left({\phi }\wedge {t}\in {D}\right)\to \left(\exists {j}\in \left(1\dots {M}\right)\phantom{\rule{.4em}{0ex}}{U}\left({j}\right)\left({t}\right)<{E}\to \exists {j}\in \left(1\dots {M}\right)\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)\left({j}\right)<{E}\right)$
163 149 162 mpd ${⊢}\left({\phi }\wedge {t}\in {D}\right)\to \exists {j}\in \left(1\dots {M}\right)\phantom{\rule{.4em}{0ex}}{F}\left({t}\right)\left({j}\right)<{E}$
164 84 86 87 88 89 72 103 106 107 163 fmul01lt1 ${⊢}\left({\phi }\wedge {t}\in {D}\right)\to seq1\left(×,{F}\left({t}\right)\right)\left({M}\right)<{E}$
165 78 164 eqbrtrd ${⊢}\left({\phi }\wedge {t}\in {D}\right)\to {Z}\left({t}\right)<{E}$
166 36 165 eqbrtrd ${⊢}\left({\phi }\wedge {t}\in {D}\right)\to {X}\left({t}\right)<{E}$
167 166 ex ${⊢}{\phi }\to \left({t}\in {D}\to {X}\left({t}\right)<{E}\right)$
168 2 167 ralrimi ${⊢}{\phi }\to \forall {t}\in {D}\phantom{\rule{.4em}{0ex}}{X}\left({t}\right)<{E}$