# Metamath Proof Explorer

## Theorem hoicvr

Description: I is a countable set of half-open intervals that covers the whole multidimensional reals. See Definition 1135 (b) of Fremlin1 p. 29. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypotheses hoicvr.2 ${⊢}{I}=\left({j}\in ℕ⟼\left({x}\in {X}⟼⟨-{j},{j}⟩\right)\right)$
hoicvr.3 ${⊢}{\phi }\to {X}\in \mathrm{Fin}$
Assertion hoicvr ${⊢}{\phi }\to {ℝ}^{{X}}\subseteq \bigcup _{{j}\in ℕ}\underset{{i}\in {X}}{⨉}\left(\left[.\right)\circ {I}\left({j}\right)\right)\left({i}\right)$

### Proof

Step Hyp Ref Expression
1 hoicvr.2 ${⊢}{I}=\left({j}\in ℕ⟼\left({x}\in {X}⟼⟨-{j},{j}⟩\right)\right)$
2 hoicvr.3 ${⊢}{\phi }\to {X}\in \mathrm{Fin}$
3 reex ${⊢}ℝ\in \mathrm{V}$
4 mapdm0 ${⊢}ℝ\in \mathrm{V}\to {ℝ}^{\varnothing }=\left\{\varnothing \right\}$
5 3 4 ax-mp ${⊢}{ℝ}^{\varnothing }=\left\{\varnothing \right\}$
6 5 a1i ${⊢}{X}=\varnothing \to {ℝ}^{\varnothing }=\left\{\varnothing \right\}$
7 oveq2 ${⊢}{X}=\varnothing \to {ℝ}^{{X}}={ℝ}^{\varnothing }$
8 ixpeq1 ${⊢}{X}=\varnothing \to \underset{{i}\in {X}}{⨉}\left(\left[.\right)\circ {I}\left({j}\right)\right)\left({i}\right)=\underset{{i}\in \varnothing }{⨉}\left(\left[.\right)\circ {I}\left({j}\right)\right)\left({i}\right)$
9 8 iuneq2d ${⊢}{X}=\varnothing \to \bigcup _{{j}\in ℕ}\underset{{i}\in {X}}{⨉}\left(\left[.\right)\circ {I}\left({j}\right)\right)\left({i}\right)=\bigcup _{{j}\in ℕ}\underset{{i}\in \varnothing }{⨉}\left(\left[.\right)\circ {I}\left({j}\right)\right)\left({i}\right)$
10 ixp0x ${⊢}\underset{{i}\in \varnothing }{⨉}\left(\left[.\right)\circ {I}\left({j}\right)\right)\left({i}\right)=\left\{\varnothing \right\}$
11 10 a1i ${⊢}{j}\in ℕ\to \underset{{i}\in \varnothing }{⨉}\left(\left[.\right)\circ {I}\left({j}\right)\right)\left({i}\right)=\left\{\varnothing \right\}$
12 11 iuneq2i ${⊢}\bigcup _{{j}\in ℕ}\underset{{i}\in \varnothing }{⨉}\left(\left[.\right)\circ {I}\left({j}\right)\right)\left({i}\right)=\bigcup _{{j}\in ℕ}\left\{\varnothing \right\}$
13 1nn ${⊢}1\in ℕ$
14 13 ne0ii ${⊢}ℕ\ne \varnothing$
15 iunconst ${⊢}ℕ\ne \varnothing \to \bigcup _{{j}\in ℕ}\left\{\varnothing \right\}=\left\{\varnothing \right\}$
16 14 15 ax-mp ${⊢}\bigcup _{{j}\in ℕ}\left\{\varnothing \right\}=\left\{\varnothing \right\}$
17 12 16 eqtri ${⊢}\bigcup _{{j}\in ℕ}\underset{{i}\in \varnothing }{⨉}\left(\left[.\right)\circ {I}\left({j}\right)\right)\left({i}\right)=\left\{\varnothing \right\}$
18 17 a1i ${⊢}{X}=\varnothing \to \bigcup _{{j}\in ℕ}\underset{{i}\in \varnothing }{⨉}\left(\left[.\right)\circ {I}\left({j}\right)\right)\left({i}\right)=\left\{\varnothing \right\}$
19 9 18 eqtrd ${⊢}{X}=\varnothing \to \bigcup _{{j}\in ℕ}\underset{{i}\in {X}}{⨉}\left(\left[.\right)\circ {I}\left({j}\right)\right)\left({i}\right)=\left\{\varnothing \right\}$
20 6 7 19 3eqtr4d ${⊢}{X}=\varnothing \to {ℝ}^{{X}}=\bigcup _{{j}\in ℕ}\underset{{i}\in {X}}{⨉}\left(\left[.\right)\circ {I}\left({j}\right)\right)\left({i}\right)$
21 eqimss ${⊢}{ℝ}^{{X}}=\bigcup _{{j}\in ℕ}\underset{{i}\in {X}}{⨉}\left(\left[.\right)\circ {I}\left({j}\right)\right)\left({i}\right)\to {ℝ}^{{X}}\subseteq \bigcup _{{j}\in ℕ}\underset{{i}\in {X}}{⨉}\left(\left[.\right)\circ {I}\left({j}\right)\right)\left({i}\right)$
22 20 21 syl ${⊢}{X}=\varnothing \to {ℝ}^{{X}}\subseteq \bigcup _{{j}\in ℕ}\underset{{i}\in {X}}{⨉}\left(\left[.\right)\circ {I}\left({j}\right)\right)\left({i}\right)$
23 22 adantl ${⊢}\left({\phi }\wedge {X}=\varnothing \right)\to {ℝ}^{{X}}\subseteq \bigcup _{{j}\in ℕ}\underset{{i}\in {X}}{⨉}\left(\left[.\right)\circ {I}\left({j}\right)\right)\left({i}\right)$
24 simpll ${⊢}\left(\left({\phi }\wedge ¬{X}=\varnothing \right)\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\to {\phi }$
25 simpr ${⊢}\left(\left({\phi }\wedge ¬{X}=\varnothing \right)\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\to {f}\in \left({ℝ}^{{X}}\right)$
26 simplr ${⊢}\left(\left({\phi }\wedge ¬{X}=\varnothing \right)\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\to ¬{X}=\varnothing$
27 rncoss ${⊢}\mathrm{ran}\left(\mathrm{abs}\circ {f}\right)\subseteq \mathrm{ran}\mathrm{abs}$
28 absf ${⊢}\mathrm{abs}:ℂ⟶ℝ$
29 frn ${⊢}\mathrm{abs}:ℂ⟶ℝ\to \mathrm{ran}\mathrm{abs}\subseteq ℝ$
30 28 29 ax-mp ${⊢}\mathrm{ran}\mathrm{abs}\subseteq ℝ$
31 27 30 sstri ${⊢}\mathrm{ran}\left(\mathrm{abs}\circ {f}\right)\subseteq ℝ$
32 31 a1i ${⊢}\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge ¬{X}=\varnothing \right)\to \mathrm{ran}\left(\mathrm{abs}\circ {f}\right)\subseteq ℝ$
33 ltso ${⊢}<\mathrm{Or}ℝ$
34 33 a1i ${⊢}\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge ¬{X}=\varnothing \right)\to <\mathrm{Or}ℝ$
35 28 a1i ${⊢}\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\to \mathrm{abs}:ℂ⟶ℝ$
36 elmapi ${⊢}{f}\in \left({ℝ}^{{X}}\right)\to {f}:{X}⟶ℝ$
37 36 adantl ${⊢}\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\to {f}:{X}⟶ℝ$
38 ax-resscn ${⊢}ℝ\subseteq ℂ$
39 38 a1i ${⊢}\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\to ℝ\subseteq ℂ$
40 37 39 fssd ${⊢}\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\to {f}:{X}⟶ℂ$
41 fco ${⊢}\left(\mathrm{abs}:ℂ⟶ℝ\wedge {f}:{X}⟶ℂ\right)\to \left(\mathrm{abs}\circ {f}\right):{X}⟶ℝ$
42 35 40 41 syl2anc ${⊢}\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\to \left(\mathrm{abs}\circ {f}\right):{X}⟶ℝ$
43 2 adantr ${⊢}\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\to {X}\in \mathrm{Fin}$
44 rnffi ${⊢}\left(\left(\mathrm{abs}\circ {f}\right):{X}⟶ℝ\wedge {X}\in \mathrm{Fin}\right)\to \mathrm{ran}\left(\mathrm{abs}\circ {f}\right)\in \mathrm{Fin}$
45 42 43 44 syl2anc ${⊢}\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\to \mathrm{ran}\left(\mathrm{abs}\circ {f}\right)\in \mathrm{Fin}$
46 45 adantr ${⊢}\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge ¬{X}=\varnothing \right)\to \mathrm{ran}\left(\mathrm{abs}\circ {f}\right)\in \mathrm{Fin}$
47 36 frnd ${⊢}{f}\in \left({ℝ}^{{X}}\right)\to \mathrm{ran}{f}\subseteq ℝ$
48 28 fdmi ${⊢}\mathrm{dom}\mathrm{abs}=ℂ$
49 48 eqcomi ${⊢}ℂ=\mathrm{dom}\mathrm{abs}$
50 38 49 sseqtri ${⊢}ℝ\subseteq \mathrm{dom}\mathrm{abs}$
51 50 a1i ${⊢}{f}\in \left({ℝ}^{{X}}\right)\to ℝ\subseteq \mathrm{dom}\mathrm{abs}$
52 47 51 sstrd ${⊢}{f}\in \left({ℝ}^{{X}}\right)\to \mathrm{ran}{f}\subseteq \mathrm{dom}\mathrm{abs}$
53 dmcosseq ${⊢}\mathrm{ran}{f}\subseteq \mathrm{dom}\mathrm{abs}\to \mathrm{dom}\left(\mathrm{abs}\circ {f}\right)=\mathrm{dom}{f}$
54 52 53 syl ${⊢}{f}\in \left({ℝ}^{{X}}\right)\to \mathrm{dom}\left(\mathrm{abs}\circ {f}\right)=\mathrm{dom}{f}$
55 36 fdmd ${⊢}{f}\in \left({ℝ}^{{X}}\right)\to \mathrm{dom}{f}={X}$
56 54 55 eqtrd ${⊢}{f}\in \left({ℝ}^{{X}}\right)\to \mathrm{dom}\left(\mathrm{abs}\circ {f}\right)={X}$
57 56 adantr ${⊢}\left({f}\in \left({ℝ}^{{X}}\right)\wedge ¬{X}=\varnothing \right)\to \mathrm{dom}\left(\mathrm{abs}\circ {f}\right)={X}$
58 neqne ${⊢}¬{X}=\varnothing \to {X}\ne \varnothing$
59 58 adantl ${⊢}\left({f}\in \left({ℝ}^{{X}}\right)\wedge ¬{X}=\varnothing \right)\to {X}\ne \varnothing$
60 57 59 eqnetrd ${⊢}\left({f}\in \left({ℝ}^{{X}}\right)\wedge ¬{X}=\varnothing \right)\to \mathrm{dom}\left(\mathrm{abs}\circ {f}\right)\ne \varnothing$
61 60 neneqd ${⊢}\left({f}\in \left({ℝ}^{{X}}\right)\wedge ¬{X}=\varnothing \right)\to ¬\mathrm{dom}\left(\mathrm{abs}\circ {f}\right)=\varnothing$
62 dm0rn0 ${⊢}\mathrm{dom}\left(\mathrm{abs}\circ {f}\right)=\varnothing ↔\mathrm{ran}\left(\mathrm{abs}\circ {f}\right)=\varnothing$
63 61 62 sylnib ${⊢}\left({f}\in \left({ℝ}^{{X}}\right)\wedge ¬{X}=\varnothing \right)\to ¬\mathrm{ran}\left(\mathrm{abs}\circ {f}\right)=\varnothing$
64 63 neqned ${⊢}\left({f}\in \left({ℝ}^{{X}}\right)\wedge ¬{X}=\varnothing \right)\to \mathrm{ran}\left(\mathrm{abs}\circ {f}\right)\ne \varnothing$
65 64 adantll ${⊢}\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge ¬{X}=\varnothing \right)\to \mathrm{ran}\left(\mathrm{abs}\circ {f}\right)\ne \varnothing$
66 fisupcl ${⊢}\left(<\mathrm{Or}ℝ\wedge \left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right)\in \mathrm{Fin}\wedge \mathrm{ran}\left(\mathrm{abs}\circ {f}\right)\ne \varnothing \wedge \mathrm{ran}\left(\mathrm{abs}\circ {f}\right)\subseteq ℝ\right)\right)\to sup\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right),ℝ,<\right)\in \mathrm{ran}\left(\mathrm{abs}\circ {f}\right)$
67 34 46 65 32 66 syl13anc ${⊢}\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge ¬{X}=\varnothing \right)\to sup\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right),ℝ,<\right)\in \mathrm{ran}\left(\mathrm{abs}\circ {f}\right)$
68 32 67 sseldd ${⊢}\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge ¬{X}=\varnothing \right)\to sup\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right),ℝ,<\right)\in ℝ$
69 arch ${⊢}sup\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right),ℝ,<\right)\in ℝ\to \exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}sup\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right),ℝ,<\right)<{j}$
70 68 69 syl ${⊢}\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge ¬{X}=\varnothing \right)\to \exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}sup\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right),ℝ,<\right)<{j}$
71 37 ffnd ${⊢}\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\to {f}Fn{X}$
72 71 ad2antrr ${⊢}\left(\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge ¬{X}=\varnothing \right)\wedge sup\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right),ℝ,<\right)<{j}\right)\to {f}Fn{X}$
73 72 adantlr ${⊢}\left(\left(\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge ¬{X}=\varnothing \right)\wedge {j}\in ℕ\right)\wedge sup\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right),ℝ,<\right)<{j}\right)\to {f}Fn{X}$
74 simplll ${⊢}\left(\left(\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge {j}\in ℕ\right)\wedge sup\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right),ℝ,<\right)<{j}\right)\wedge {i}\in {X}\right)\to \left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)$
75 id ${⊢}{j}\in ℕ\to {j}\in ℕ$
76 75 ad3antlr ${⊢}\left(\left(\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge {j}\in ℕ\right)\wedge sup\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right),ℝ,<\right)<{j}\right)\wedge {i}\in {X}\right)\to {j}\in ℕ$
77 simplr ${⊢}\left(\left(\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge {j}\in ℕ\right)\wedge sup\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right),ℝ,<\right)<{j}\right)\wedge {i}\in {X}\right)\to sup\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right),ℝ,<\right)<{j}$
78 simpr ${⊢}\left(\left(\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge {j}\in ℕ\right)\wedge sup\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right),ℝ,<\right)<{j}\right)\wedge {i}\in {X}\right)\to {i}\in {X}$
79 simp2 ${⊢}\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge {j}\in ℕ\wedge sup\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right),ℝ,<\right)<{j}\right)\to {j}\in ℕ$
80 zssre ${⊢}ℤ\subseteq ℝ$
81 ressxr ${⊢}ℝ\subseteq {ℝ}^{*}$
82 80 81 sstri ${⊢}ℤ\subseteq {ℝ}^{*}$
83 nnnegz ${⊢}{j}\in ℕ\to -{j}\in ℤ$
84 82 83 sseldi ${⊢}{j}\in ℕ\to -{j}\in {ℝ}^{*}$
85 84 adantr ${⊢}\left({j}\in ℕ\wedge {i}\in {X}\right)\to -{j}\in {ℝ}^{*}$
86 79 85 sylan ${⊢}\left(\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge {j}\in ℕ\wedge sup\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right),ℝ,<\right)<{j}\right)\wedge {i}\in {X}\right)\to -{j}\in {ℝ}^{*}$
87 75 nnxrd ${⊢}{j}\in ℕ\to {j}\in {ℝ}^{*}$
88 87 adantr ${⊢}\left({j}\in ℕ\wedge {i}\in {X}\right)\to {j}\in {ℝ}^{*}$
89 79 88 sylan ${⊢}\left(\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge {j}\in ℕ\wedge sup\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right),ℝ,<\right)<{j}\right)\wedge {i}\in {X}\right)\to {j}\in {ℝ}^{*}$
90 36 3ad2ant1 ${⊢}\left({f}\in \left({ℝ}^{{X}}\right)\wedge {j}\in ℕ\wedge sup\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right),ℝ,<\right)<{j}\right)\to {f}:{X}⟶ℝ$
91 81 a1i ${⊢}\left({f}\in \left({ℝ}^{{X}}\right)\wedge {j}\in ℕ\wedge sup\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right),ℝ,<\right)<{j}\right)\to ℝ\subseteq {ℝ}^{*}$
92 90 91 fssd ${⊢}\left({f}\in \left({ℝ}^{{X}}\right)\wedge {j}\in ℕ\wedge sup\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right),ℝ,<\right)<{j}\right)\to {f}:{X}⟶{ℝ}^{*}$
93 92 3adant1l ${⊢}\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge {j}\in ℕ\wedge sup\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right),ℝ,<\right)<{j}\right)\to {f}:{X}⟶{ℝ}^{*}$
94 93 ffvelrnda ${⊢}\left(\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge {j}\in ℕ\wedge sup\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right),ℝ,<\right)<{j}\right)\wedge {i}\in {X}\right)\to {f}\left({i}\right)\in {ℝ}^{*}$
95 nnre ${⊢}{j}\in ℕ\to {j}\in ℝ$
96 95 adantr ${⊢}\left({j}\in ℕ\wedge {i}\in {X}\right)\to {j}\in ℝ$
97 96 3ad2antl2 ${⊢}\left(\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge {j}\in ℕ\wedge sup\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right),ℝ,<\right)<{j}\right)\wedge {i}\in {X}\right)\to {j}\in ℝ$
98 97 renegcld ${⊢}\left(\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge {j}\in ℕ\wedge sup\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right),ℝ,<\right)<{j}\right)\wedge {i}\in {X}\right)\to -{j}\in ℝ$
99 37 ffvelrnda ${⊢}\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge {i}\in {X}\right)\to {f}\left({i}\right)\in ℝ$
100 99 3ad2antl1 ${⊢}\left(\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge {j}\in ℕ\wedge sup\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right),ℝ,<\right)<{j}\right)\wedge {i}\in {X}\right)\to {f}\left({i}\right)\in ℝ$
101 100 renegcld ${⊢}\left(\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge {j}\in ℕ\wedge sup\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right),ℝ,<\right)<{j}\right)\wedge {i}\in {X}\right)\to -{f}\left({i}\right)\in ℝ$
102 simpll ${⊢}\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge {i}\in {X}\right)\to {\phi }$
103 simplr ${⊢}\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge {i}\in {X}\right)\to {f}\in \left({ℝ}^{{X}}\right)$
104 n0i ${⊢}{i}\in {X}\to ¬{X}=\varnothing$
105 104 adantl ${⊢}\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge {i}\in {X}\right)\to ¬{X}=\varnothing$
106 102 103 105 68 syl21anc ${⊢}\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge {i}\in {X}\right)\to sup\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right),ℝ,<\right)\in ℝ$
107 106 3ad2antl1 ${⊢}\left(\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge {j}\in ℕ\wedge sup\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right),ℝ,<\right)<{j}\right)\wedge {i}\in {X}\right)\to sup\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right),ℝ,<\right)\in ℝ$
108 36 ffvelrnda ${⊢}\left({f}\in \left({ℝ}^{{X}}\right)\wedge {i}\in {X}\right)\to {f}\left({i}\right)\in ℝ$
109 38 108 sseldi ${⊢}\left({f}\in \left({ℝ}^{{X}}\right)\wedge {i}\in {X}\right)\to {f}\left({i}\right)\in ℂ$
110 109 abscld ${⊢}\left({f}\in \left({ℝ}^{{X}}\right)\wedge {i}\in {X}\right)\to \left|{f}\left({i}\right)\right|\in ℝ$
111 110 adantll ${⊢}\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge {i}\in {X}\right)\to \left|{f}\left({i}\right)\right|\in ℝ$
112 111 3ad2antl1 ${⊢}\left(\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge {j}\in ℕ\wedge sup\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right),ℝ,<\right)<{j}\right)\wedge {i}\in {X}\right)\to \left|{f}\left({i}\right)\right|\in ℝ$
113 108 renegcld ${⊢}\left({f}\in \left({ℝ}^{{X}}\right)\wedge {i}\in {X}\right)\to -{f}\left({i}\right)\in ℝ$
114 113 leabsd ${⊢}\left({f}\in \left({ℝ}^{{X}}\right)\wedge {i}\in {X}\right)\to -{f}\left({i}\right)\le \left|-{f}\left({i}\right)\right|$
115 109 absnegd ${⊢}\left({f}\in \left({ℝ}^{{X}}\right)\wedge {i}\in {X}\right)\to \left|-{f}\left({i}\right)\right|=\left|{f}\left({i}\right)\right|$
116 114 115 breqtrd ${⊢}\left({f}\in \left({ℝ}^{{X}}\right)\wedge {i}\in {X}\right)\to -{f}\left({i}\right)\le \left|{f}\left({i}\right)\right|$
117 116 adantll ${⊢}\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge {i}\in {X}\right)\to -{f}\left({i}\right)\le \left|{f}\left({i}\right)\right|$
118 117 3ad2antl1 ${⊢}\left(\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge {j}\in ℕ\wedge sup\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right),ℝ,<\right)<{j}\right)\wedge {i}\in {X}\right)\to -{f}\left({i}\right)\le \left|{f}\left({i}\right)\right|$
119 31 a1i ${⊢}\left(\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge {j}\in ℕ\wedge sup\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right),ℝ,<\right)<{j}\right)\wedge {i}\in {X}\right)\to \mathrm{ran}\left(\mathrm{abs}\circ {f}\right)\subseteq ℝ$
120 105 65 syldan ${⊢}\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge {i}\in {X}\right)\to \mathrm{ran}\left(\mathrm{abs}\circ {f}\right)\ne \varnothing$
121 120 3ad2antl1 ${⊢}\left(\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge {j}\in ℕ\wedge sup\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right),ℝ,<\right)<{j}\right)\wedge {i}\in {X}\right)\to \mathrm{ran}\left(\mathrm{abs}\circ {f}\right)\ne \varnothing$
122 fimaxre2 ${⊢}\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right)\subseteq ℝ\wedge \mathrm{ran}\left(\mathrm{abs}\circ {f}\right)\in \mathrm{Fin}\right)\to \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{ran}\left(\mathrm{abs}\circ {f}\right)\phantom{\rule{.4em}{0ex}}{z}\le {y}$
123 31 45 122 sylancr ${⊢}\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\to \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{ran}\left(\mathrm{abs}\circ {f}\right)\phantom{\rule{.4em}{0ex}}{z}\le {y}$
124 123 adantr ${⊢}\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge {i}\in {X}\right)\to \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{ran}\left(\mathrm{abs}\circ {f}\right)\phantom{\rule{.4em}{0ex}}{z}\le {y}$
125 124 3ad2antl1 ${⊢}\left(\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge {j}\in ℕ\wedge sup\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right),ℝ,<\right)<{j}\right)\wedge {i}\in {X}\right)\to \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{ran}\left(\mathrm{abs}\circ {f}\right)\phantom{\rule{.4em}{0ex}}{z}\le {y}$
126 elmapfun ${⊢}{f}\in \left({ℝ}^{{X}}\right)\to \mathrm{Fun}{f}$
127 126 adantr ${⊢}\left({f}\in \left({ℝ}^{{X}}\right)\wedge {i}\in {X}\right)\to \mathrm{Fun}{f}$
128 simpr ${⊢}\left({f}\in \left({ℝ}^{{X}}\right)\wedge {i}\in {X}\right)\to {i}\in {X}$
129 55 eqcomd ${⊢}{f}\in \left({ℝ}^{{X}}\right)\to {X}=\mathrm{dom}{f}$
130 129 adantr ${⊢}\left({f}\in \left({ℝ}^{{X}}\right)\wedge {i}\in {X}\right)\to {X}=\mathrm{dom}{f}$
131 128 130 eleqtrd ${⊢}\left({f}\in \left({ℝ}^{{X}}\right)\wedge {i}\in {X}\right)\to {i}\in \mathrm{dom}{f}$
132 fvco ${⊢}\left(\mathrm{Fun}{f}\wedge {i}\in \mathrm{dom}{f}\right)\to \left(\mathrm{abs}\circ {f}\right)\left({i}\right)=\left|{f}\left({i}\right)\right|$
133 127 131 132 syl2anc ${⊢}\left({f}\in \left({ℝ}^{{X}}\right)\wedge {i}\in {X}\right)\to \left(\mathrm{abs}\circ {f}\right)\left({i}\right)=\left|{f}\left({i}\right)\right|$
134 133 eqcomd ${⊢}\left({f}\in \left({ℝ}^{{X}}\right)\wedge {i}\in {X}\right)\to \left|{f}\left({i}\right)\right|=\left(\mathrm{abs}\circ {f}\right)\left({i}\right)$
135 absfun ${⊢}\mathrm{Fun}\mathrm{abs}$
136 135 a1i ${⊢}{f}\in \left({ℝ}^{{X}}\right)\to \mathrm{Fun}\mathrm{abs}$
137 funco ${⊢}\left(\mathrm{Fun}\mathrm{abs}\wedge \mathrm{Fun}{f}\right)\to \mathrm{Fun}\left(\mathrm{abs}\circ {f}\right)$
138 136 126 137 syl2anc ${⊢}{f}\in \left({ℝ}^{{X}}\right)\to \mathrm{Fun}\left(\mathrm{abs}\circ {f}\right)$
139 138 adantr ${⊢}\left({f}\in \left({ℝ}^{{X}}\right)\wedge {i}\in {X}\right)\to \mathrm{Fun}\left(\mathrm{abs}\circ {f}\right)$
140 109 49 eleqtrdi ${⊢}\left({f}\in \left({ℝ}^{{X}}\right)\wedge {i}\in {X}\right)\to {f}\left({i}\right)\in \mathrm{dom}\mathrm{abs}$
141 dmfco ${⊢}\left(\mathrm{Fun}{f}\wedge {i}\in \mathrm{dom}{f}\right)\to \left({i}\in \mathrm{dom}\left(\mathrm{abs}\circ {f}\right)↔{f}\left({i}\right)\in \mathrm{dom}\mathrm{abs}\right)$
142 127 131 141 syl2anc ${⊢}\left({f}\in \left({ℝ}^{{X}}\right)\wedge {i}\in {X}\right)\to \left({i}\in \mathrm{dom}\left(\mathrm{abs}\circ {f}\right)↔{f}\left({i}\right)\in \mathrm{dom}\mathrm{abs}\right)$
143 140 142 mpbird ${⊢}\left({f}\in \left({ℝ}^{{X}}\right)\wedge {i}\in {X}\right)\to {i}\in \mathrm{dom}\left(\mathrm{abs}\circ {f}\right)$
144 fvelrn ${⊢}\left(\mathrm{Fun}\left(\mathrm{abs}\circ {f}\right)\wedge {i}\in \mathrm{dom}\left(\mathrm{abs}\circ {f}\right)\right)\to \left(\mathrm{abs}\circ {f}\right)\left({i}\right)\in \mathrm{ran}\left(\mathrm{abs}\circ {f}\right)$
145 139 143 144 syl2anc ${⊢}\left({f}\in \left({ℝ}^{{X}}\right)\wedge {i}\in {X}\right)\to \left(\mathrm{abs}\circ {f}\right)\left({i}\right)\in \mathrm{ran}\left(\mathrm{abs}\circ {f}\right)$
146 134 145 eqeltrd ${⊢}\left({f}\in \left({ℝ}^{{X}}\right)\wedge {i}\in {X}\right)\to \left|{f}\left({i}\right)\right|\in \mathrm{ran}\left(\mathrm{abs}\circ {f}\right)$
147 146 adantll ${⊢}\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge {i}\in {X}\right)\to \left|{f}\left({i}\right)\right|\in \mathrm{ran}\left(\mathrm{abs}\circ {f}\right)$
148 147 3ad2antl1 ${⊢}\left(\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge {j}\in ℕ\wedge sup\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right),ℝ,<\right)<{j}\right)\wedge {i}\in {X}\right)\to \left|{f}\left({i}\right)\right|\in \mathrm{ran}\left(\mathrm{abs}\circ {f}\right)$
149 suprub ${⊢}\left(\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right)\subseteq ℝ\wedge \mathrm{ran}\left(\mathrm{abs}\circ {f}\right)\ne \varnothing \wedge \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{ran}\left(\mathrm{abs}\circ {f}\right)\phantom{\rule{.4em}{0ex}}{z}\le {y}\right)\wedge \left|{f}\left({i}\right)\right|\in \mathrm{ran}\left(\mathrm{abs}\circ {f}\right)\right)\to \left|{f}\left({i}\right)\right|\le sup\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right),ℝ,<\right)$
150 119 121 125 148 149 syl31anc ${⊢}\left(\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge {j}\in ℕ\wedge sup\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right),ℝ,<\right)<{j}\right)\wedge {i}\in {X}\right)\to \left|{f}\left({i}\right)\right|\le sup\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right),ℝ,<\right)$
151 101 112 107 118 150 letrd ${⊢}\left(\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge {j}\in ℕ\wedge sup\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right),ℝ,<\right)<{j}\right)\wedge {i}\in {X}\right)\to -{f}\left({i}\right)\le sup\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right),ℝ,<\right)$
152 simpl3 ${⊢}\left(\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge {j}\in ℕ\wedge sup\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right),ℝ,<\right)<{j}\right)\wedge {i}\in {X}\right)\to sup\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right),ℝ,<\right)<{j}$
153 101 107 97 151 152 lelttrd ${⊢}\left(\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge {j}\in ℕ\wedge sup\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right),ℝ,<\right)<{j}\right)\wedge {i}\in {X}\right)\to -{f}\left({i}\right)<{j}$
154 101 97 ltnegd ${⊢}\left(\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge {j}\in ℕ\wedge sup\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right),ℝ,<\right)<{j}\right)\wedge {i}\in {X}\right)\to \left(-{f}\left({i}\right)<{j}↔-{j}<-\left(-{f}\left({i}\right)\right)\right)$
155 153 154 mpbid ${⊢}\left(\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge {j}\in ℕ\wedge sup\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right),ℝ,<\right)<{j}\right)\wedge {i}\in {X}\right)\to -{j}<-\left(-{f}\left({i}\right)\right)$
156 38 100 sseldi ${⊢}\left(\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge {j}\in ℕ\wedge sup\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right),ℝ,<\right)<{j}\right)\wedge {i}\in {X}\right)\to {f}\left({i}\right)\in ℂ$
157 156 negnegd ${⊢}\left(\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge {j}\in ℕ\wedge sup\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right),ℝ,<\right)<{j}\right)\wedge {i}\in {X}\right)\to -\left(-{f}\left({i}\right)\right)={f}\left({i}\right)$
158 155 157 breqtrd ${⊢}\left(\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge {j}\in ℕ\wedge sup\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right),ℝ,<\right)<{j}\right)\wedge {i}\in {X}\right)\to -{j}<{f}\left({i}\right)$
159 98 100 158 ltled ${⊢}\left(\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge {j}\in ℕ\wedge sup\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right),ℝ,<\right)<{j}\right)\wedge {i}\in {X}\right)\to -{j}\le {f}\left({i}\right)$
160 100 leabsd ${⊢}\left(\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge {j}\in ℕ\wedge sup\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right),ℝ,<\right)<{j}\right)\wedge {i}\in {X}\right)\to {f}\left({i}\right)\le \left|{f}\left({i}\right)\right|$
161 100 112 107 160 150 letrd ${⊢}\left(\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge {j}\in ℕ\wedge sup\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right),ℝ,<\right)<{j}\right)\wedge {i}\in {X}\right)\to {f}\left({i}\right)\le sup\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right),ℝ,<\right)$
162 100 107 97 161 152 lelttrd ${⊢}\left(\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge {j}\in ℕ\wedge sup\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right),ℝ,<\right)<{j}\right)\wedge {i}\in {X}\right)\to {f}\left({i}\right)<{j}$
163 86 89 94 159 162 elicod ${⊢}\left(\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge {j}\in ℕ\wedge sup\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right),ℝ,<\right)<{j}\right)\wedge {i}\in {X}\right)\to {f}\left({i}\right)\in \left[-{j},{j}\right)$
164 74 76 77 78 163 syl31anc ${⊢}\left(\left(\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge {j}\in ℕ\right)\wedge sup\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right),ℝ,<\right)<{j}\right)\wedge {i}\in {X}\right)\to {f}\left({i}\right)\in \left[-{j},{j}\right)$
165 164 adantl3r ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge ¬{X}=\varnothing \right)\wedge {j}\in ℕ\right)\wedge sup\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right),ℝ,<\right)<{j}\right)\wedge {i}\in {X}\right)\to {f}\left({i}\right)\in \left[-{j},{j}\right)$
166 simpr ${⊢}\left({\phi }\wedge {j}\in ℕ\right)\to {j}\in ℕ$
167 mptexg ${⊢}{X}\in \mathrm{Fin}\to \left({x}\in {X}⟼⟨-{j},{j}⟩\right)\in \mathrm{V}$
168 2 167 syl ${⊢}{\phi }\to \left({x}\in {X}⟼⟨-{j},{j}⟩\right)\in \mathrm{V}$
169 168 adantr ${⊢}\left({\phi }\wedge {j}\in ℕ\right)\to \left({x}\in {X}⟼⟨-{j},{j}⟩\right)\in \mathrm{V}$
170 1 fvmpt2 ${⊢}\left({j}\in ℕ\wedge \left({x}\in {X}⟼⟨-{j},{j}⟩\right)\in \mathrm{V}\right)\to {I}\left({j}\right)=\left({x}\in {X}⟼⟨-{j},{j}⟩\right)$
171 166 169 170 syl2anc ${⊢}\left({\phi }\wedge {j}\in ℕ\right)\to {I}\left({j}\right)=\left({x}\in {X}⟼⟨-{j},{j}⟩\right)$
172 171 fveq1d ${⊢}\left({\phi }\wedge {j}\in ℕ\right)\to {I}\left({j}\right)\left({i}\right)=\left({x}\in {X}⟼⟨-{j},{j}⟩\right)\left({i}\right)$
173 172 3adant3 ${⊢}\left({\phi }\wedge {j}\in ℕ\wedge {i}\in {X}\right)\to {I}\left({j}\right)\left({i}\right)=\left({x}\in {X}⟼⟨-{j},{j}⟩\right)\left({i}\right)$
174 eqidd ${⊢}{i}\in {X}\to \left({x}\in {X}⟼⟨-{j},{j}⟩\right)=\left({x}\in {X}⟼⟨-{j},{j}⟩\right)$
175 eqid ${⊢}⟨-{j},{j}⟩=⟨-{j},{j}⟩$
176 175 a1i ${⊢}\left({i}\in {X}\wedge {x}={i}\right)\to ⟨-{j},{j}⟩=⟨-{j},{j}⟩$
177 id ${⊢}{i}\in {X}\to {i}\in {X}$
178 opex ${⊢}⟨-{j},{j}⟩\in \mathrm{V}$
179 178 a1i ${⊢}{i}\in {X}\to ⟨-{j},{j}⟩\in \mathrm{V}$
180 174 176 177 179 fvmptd ${⊢}{i}\in {X}\to \left({x}\in {X}⟼⟨-{j},{j}⟩\right)\left({i}\right)=⟨-{j},{j}⟩$
181 180 3ad2ant3 ${⊢}\left({\phi }\wedge {j}\in ℕ\wedge {i}\in {X}\right)\to \left({x}\in {X}⟼⟨-{j},{j}⟩\right)\left({i}\right)=⟨-{j},{j}⟩$
182 173 181 eqtrd ${⊢}\left({\phi }\wedge {j}\in ℕ\wedge {i}\in {X}\right)\to {I}\left({j}\right)\left({i}\right)=⟨-{j},{j}⟩$
183 182 fveq2d ${⊢}\left({\phi }\wedge {j}\in ℕ\wedge {i}\in {X}\right)\to {1}^{st}\left({I}\left({j}\right)\left({i}\right)\right)={1}^{st}\left(⟨-{j},{j}⟩\right)$
184 negex ${⊢}-{j}\in \mathrm{V}$
185 vex ${⊢}{j}\in \mathrm{V}$
186 184 185 op1st ${⊢}{1}^{st}\left(⟨-{j},{j}⟩\right)=-{j}$
187 186 a1i ${⊢}\left({\phi }\wedge {j}\in ℕ\wedge {i}\in {X}\right)\to {1}^{st}\left(⟨-{j},{j}⟩\right)=-{j}$
188 183 187 eqtrd ${⊢}\left({\phi }\wedge {j}\in ℕ\wedge {i}\in {X}\right)\to {1}^{st}\left({I}\left({j}\right)\left({i}\right)\right)=-{j}$
189 182 fveq2d ${⊢}\left({\phi }\wedge {j}\in ℕ\wedge {i}\in {X}\right)\to {2}^{nd}\left({I}\left({j}\right)\left({i}\right)\right)={2}^{nd}\left(⟨-{j},{j}⟩\right)$
190 184 185 op2nd ${⊢}{2}^{nd}\left(⟨-{j},{j}⟩\right)={j}$
191 190 a1i ${⊢}\left({\phi }\wedge {j}\in ℕ\wedge {i}\in {X}\right)\to {2}^{nd}\left(⟨-{j},{j}⟩\right)={j}$
192 189 191 eqtrd ${⊢}\left({\phi }\wedge {j}\in ℕ\wedge {i}\in {X}\right)\to {2}^{nd}\left({I}\left({j}\right)\left({i}\right)\right)={j}$
193 188 192 oveq12d ${⊢}\left({\phi }\wedge {j}\in ℕ\wedge {i}\in {X}\right)\to \left[{1}^{st}\left({I}\left({j}\right)\left({i}\right)\right),{2}^{nd}\left({I}\left({j}\right)\left({i}\right)\right)\right)=\left[-{j},{j}\right)$
194 193 eqcomd ${⊢}\left({\phi }\wedge {j}\in ℕ\wedge {i}\in {X}\right)\to \left[-{j},{j}\right)=\left[{1}^{st}\left({I}\left({j}\right)\left({i}\right)\right),{2}^{nd}\left({I}\left({j}\right)\left({i}\right)\right)\right)$
195 194 3adant1r ${⊢}\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge {j}\in ℕ\wedge {i}\in {X}\right)\to \left[-{j},{j}\right)=\left[{1}^{st}\left({I}\left({j}\right)\left({i}\right)\right),{2}^{nd}\left({I}\left({j}\right)\left({i}\right)\right)\right)$
196 195 ad5ant135 ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge ¬{X}=\varnothing \right)\wedge {j}\in ℕ\right)\wedge sup\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right),ℝ,<\right)<{j}\right)\wedge {i}\in {X}\right)\to \left[-{j},{j}\right)=\left[{1}^{st}\left({I}\left({j}\right)\left({i}\right)\right),{2}^{nd}\left({I}\left({j}\right)\left({i}\right)\right)\right)$
197 165 196 eleqtrd ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge ¬{X}=\varnothing \right)\wedge {j}\in ℕ\right)\wedge sup\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right),ℝ,<\right)<{j}\right)\wedge {i}\in {X}\right)\to {f}\left({i}\right)\in \left[{1}^{st}\left({I}\left({j}\right)\left({i}\right)\right),{2}^{nd}\left({I}\left({j}\right)\left({i}\right)\right)\right)$
198 80 83 sseldi ${⊢}{j}\in ℕ\to -{j}\in ℝ$
199 opelxpi ${⊢}\left(-{j}\in ℝ\wedge {j}\in ℝ\right)\to ⟨-{j},{j}⟩\in {ℝ}^{2}$
200 198 95 199 syl2anc ${⊢}{j}\in ℕ\to ⟨-{j},{j}⟩\in {ℝ}^{2}$
201 200 ad2antlr ${⊢}\left(\left({\phi }\wedge {j}\in ℕ\right)\wedge {x}\in {X}\right)\to ⟨-{j},{j}⟩\in {ℝ}^{2}$
202 eqid ${⊢}\left({x}\in {X}⟼⟨-{j},{j}⟩\right)=\left({x}\in {X}⟼⟨-{j},{j}⟩\right)$
203 201 202 fmptd ${⊢}\left({\phi }\wedge {j}\in ℕ\right)\to \left({x}\in {X}⟼⟨-{j},{j}⟩\right):{X}⟶{ℝ}^{2}$
204 171 feq1d ${⊢}\left({\phi }\wedge {j}\in ℕ\right)\to \left({I}\left({j}\right):{X}⟶{ℝ}^{2}↔\left({x}\in {X}⟼⟨-{j},{j}⟩\right):{X}⟶{ℝ}^{2}\right)$
205 203 204 mpbird ${⊢}\left({\phi }\wedge {j}\in ℕ\right)\to {I}\left({j}\right):{X}⟶{ℝ}^{2}$
206 205 ad4ant14 ${⊢}\left(\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge ¬{X}=\varnothing \right)\wedge {j}\in ℕ\right)\to {I}\left({j}\right):{X}⟶{ℝ}^{2}$
207 206 ad2antrr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge ¬{X}=\varnothing \right)\wedge {j}\in ℕ\right)\wedge sup\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right),ℝ,<\right)<{j}\right)\wedge {i}\in {X}\right)\to {I}\left({j}\right):{X}⟶{ℝ}^{2}$
208 simpr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge ¬{X}=\varnothing \right)\wedge {j}\in ℕ\right)\wedge sup\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right),ℝ,<\right)<{j}\right)\wedge {i}\in {X}\right)\to {i}\in {X}$
209 207 208 fvovco ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge ¬{X}=\varnothing \right)\wedge {j}\in ℕ\right)\wedge sup\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right),ℝ,<\right)<{j}\right)\wedge {i}\in {X}\right)\to \left(\left[.\right)\circ {I}\left({j}\right)\right)\left({i}\right)=\left[{1}^{st}\left({I}\left({j}\right)\left({i}\right)\right),{2}^{nd}\left({I}\left({j}\right)\left({i}\right)\right)\right)$
210 209 eqcomd ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge ¬{X}=\varnothing \right)\wedge {j}\in ℕ\right)\wedge sup\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right),ℝ,<\right)<{j}\right)\wedge {i}\in {X}\right)\to \left[{1}^{st}\left({I}\left({j}\right)\left({i}\right)\right),{2}^{nd}\left({I}\left({j}\right)\left({i}\right)\right)\right)=\left(\left[.\right)\circ {I}\left({j}\right)\right)\left({i}\right)$
211 197 210 eleqtrd ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge ¬{X}=\varnothing \right)\wedge {j}\in ℕ\right)\wedge sup\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right),ℝ,<\right)<{j}\right)\wedge {i}\in {X}\right)\to {f}\left({i}\right)\in \left(\left[.\right)\circ {I}\left({j}\right)\right)\left({i}\right)$
212 211 ralrimiva ${⊢}\left(\left(\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge ¬{X}=\varnothing \right)\wedge {j}\in ℕ\right)\wedge sup\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right),ℝ,<\right)<{j}\right)\to \forall {i}\in {X}\phantom{\rule{.4em}{0ex}}{f}\left({i}\right)\in \left(\left[.\right)\circ {I}\left({j}\right)\right)\left({i}\right)$
213 73 212 jca ${⊢}\left(\left(\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge ¬{X}=\varnothing \right)\wedge {j}\in ℕ\right)\wedge sup\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right),ℝ,<\right)<{j}\right)\to \left({f}Fn{X}\wedge \forall {i}\in {X}\phantom{\rule{.4em}{0ex}}{f}\left({i}\right)\in \left(\left[.\right)\circ {I}\left({j}\right)\right)\left({i}\right)\right)$
214 vex ${⊢}{f}\in \mathrm{V}$
215 214 elixp ${⊢}{f}\in \underset{{i}\in {X}}{⨉}\left(\left[.\right)\circ {I}\left({j}\right)\right)\left({i}\right)↔\left({f}Fn{X}\wedge \forall {i}\in {X}\phantom{\rule{.4em}{0ex}}{f}\left({i}\right)\in \left(\left[.\right)\circ {I}\left({j}\right)\right)\left({i}\right)\right)$
216 213 215 sylibr ${⊢}\left(\left(\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge ¬{X}=\varnothing \right)\wedge {j}\in ℕ\right)\wedge sup\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right),ℝ,<\right)<{j}\right)\to {f}\in \underset{{i}\in {X}}{⨉}\left(\left[.\right)\circ {I}\left({j}\right)\right)\left({i}\right)$
217 216 ex ${⊢}\left(\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge ¬{X}=\varnothing \right)\wedge {j}\in ℕ\right)\to \left(sup\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right),ℝ,<\right)<{j}\to {f}\in \underset{{i}\in {X}}{⨉}\left(\left[.\right)\circ {I}\left({j}\right)\right)\left({i}\right)\right)$
218 217 reximdva ${⊢}\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge ¬{X}=\varnothing \right)\to \left(\exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}sup\left(\mathrm{ran}\left(\mathrm{abs}\circ {f}\right),ℝ,<\right)<{j}\to \exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}{f}\in \underset{{i}\in {X}}{⨉}\left(\left[.\right)\circ {I}\left({j}\right)\right)\left({i}\right)\right)$
219 70 218 mpd ${⊢}\left(\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\wedge ¬{X}=\varnothing \right)\to \exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}{f}\in \underset{{i}\in {X}}{⨉}\left(\left[.\right)\circ {I}\left({j}\right)\right)\left({i}\right)$
220 24 25 26 219 syl21anc ${⊢}\left(\left({\phi }\wedge ¬{X}=\varnothing \right)\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\to \exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}{f}\in \underset{{i}\in {X}}{⨉}\left(\left[.\right)\circ {I}\left({j}\right)\right)\left({i}\right)$
221 eliun ${⊢}{f}\in \bigcup _{{j}\in ℕ}\underset{{i}\in {X}}{⨉}\left(\left[.\right)\circ {I}\left({j}\right)\right)\left({i}\right)↔\exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}{f}\in \underset{{i}\in {X}}{⨉}\left(\left[.\right)\circ {I}\left({j}\right)\right)\left({i}\right)$
222 220 221 sylibr ${⊢}\left(\left({\phi }\wedge ¬{X}=\varnothing \right)\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\to {f}\in \bigcup _{{j}\in ℕ}\underset{{i}\in {X}}{⨉}\left(\left[.\right)\circ {I}\left({j}\right)\right)\left({i}\right)$
223 222 ralrimiva ${⊢}\left({\phi }\wedge ¬{X}=\varnothing \right)\to \forall {f}\in \left({ℝ}^{{X}}\right)\phantom{\rule{.4em}{0ex}}{f}\in \bigcup _{{j}\in ℕ}\underset{{i}\in {X}}{⨉}\left(\left[.\right)\circ {I}\left({j}\right)\right)\left({i}\right)$
224 dfss3 ${⊢}{ℝ}^{{X}}\subseteq \bigcup _{{j}\in ℕ}\underset{{i}\in {X}}{⨉}\left(\left[.\right)\circ {I}\left({j}\right)\right)\left({i}\right)↔\forall {f}\in \left({ℝ}^{{X}}\right)\phantom{\rule{.4em}{0ex}}{f}\in \bigcup _{{j}\in ℕ}\underset{{i}\in {X}}{⨉}\left(\left[.\right)\circ {I}\left({j}\right)\right)\left({i}\right)$
225 223 224 sylibr ${⊢}\left({\phi }\wedge ¬{X}=\varnothing \right)\to {ℝ}^{{X}}\subseteq \bigcup _{{j}\in ℕ}\underset{{i}\in {X}}{⨉}\left(\left[.\right)\circ {I}\left({j}\right)\right)\left({i}\right)$
226 23 225 pm2.61dan ${⊢}{\phi }\to {ℝ}^{{X}}\subseteq \bigcup _{{j}\in ℕ}\underset{{i}\in {X}}{⨉}\left(\left[.\right)\circ {I}\left({j}\right)\right)\left({i}\right)$