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) Avoid ax-rep and shorten proof. (Revised by GG, 2-Apr-2026)

Ref Expression
Hypotheses hoicvr.2 ⊢ 𝐼 = ( 𝑗 ∈ ℕ ↦ ( 𝑥 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) )
hoicvr.3 ⊢ ( 𝜑 → 𝑋 ∈ Fin )
Assertion hoicvr ( 𝜑 → ( ℝ ↑m 𝑋 ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑖 ∈ 𝑋 ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑖 ) )

Proof

Step Hyp Ref Expression
1 hoicvr.2 ⊢ 𝐼 = ( 𝑗 ∈ ℕ ↦ ( 𝑥 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) )
2 hoicvr.3 ⊢ ( 𝜑 → 𝑋 ∈ Fin )
3 reex ⊢ ℝ ∈ V
4 mapdm0 ⊢ ( ℝ ∈ V → ( ℝ ↑m ∅ ) = { ∅ } )
5 3 4 ax-mp ⊢ ( ℝ ↑m ∅ ) = { ∅ }
6 oveq2 ⊢ ( 𝑋 = ∅ → ( ℝ ↑m 𝑋 ) = ( ℝ ↑m ∅ ) )
7 ixpeq1 ⊢ ( 𝑋 = ∅ → X 𝑖 ∈ 𝑋 ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑖 ) = X 𝑖 ∈ ∅ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑖 ) )
8 7 iuneq2d ⊢ ( 𝑋 = ∅ → ∪ 𝑗 ∈ ℕ X 𝑖 ∈ 𝑋 ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑖 ) = ∪ 𝑗 ∈ ℕ X 𝑖 ∈ ∅ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑖 ) )
9 ixp0x ⊢ X 𝑖 ∈ ∅ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑖 ) = { ∅ }
10 9 a1i ⊢ ( 𝑗 ∈ ℕ → X 𝑖 ∈ ∅ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑖 ) = { ∅ } )
11 10 iuneq2i ⊢ ∪ 𝑗 ∈ ℕ X 𝑖 ∈ ∅ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑖 ) = ∪ 𝑗 ∈ ℕ { ∅ }
12 nnn0 ⊢ ℕ ≠ ∅
13 iunconst ⊢ ( ℕ ≠ ∅ → ∪ 𝑗 ∈ ℕ { ∅ } = { ∅ } )
14 12 13 ax-mp ⊢ ∪ 𝑗 ∈ ℕ { ∅ } = { ∅ }
15 11 14 eqtri ⊢ ∪ 𝑗 ∈ ℕ X 𝑖 ∈ ∅ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑖 ) = { ∅ }
16 8 15 eqtrdi ⊢ ( 𝑋 = ∅ → ∪ 𝑗 ∈ ℕ X 𝑖 ∈ 𝑋 ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑖 ) = { ∅ } )
17 5 6 16 3eqtr4a ⊢ ( 𝑋 = ∅ → ( ℝ ↑m 𝑋 ) = ∪ 𝑗 ∈ ℕ X 𝑖 ∈ 𝑋 ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑖 ) )
18 17 eqimssd ⊢ ( 𝑋 = ∅ → ( ℝ ↑m 𝑋 ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑖 ∈ 𝑋 ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑖 ) )
19 18 adantl ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ( ℝ ↑m 𝑋 ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑖 ∈ 𝑋 ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑖 ) )
20 elmapi ⊢ ( 𝑓 ∈ ( ℝ ↑m 𝑋 ) → 𝑓 : 𝑋 ⟶ ℝ )
21 20 adantl ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) → 𝑓 : 𝑋 ⟶ ℝ )
22 21 ffnd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) → 𝑓 Fn 𝑋 )
23 22 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) ∧ ¬ 𝑋 = ∅ ) ∧ 𝑗 ∈ ℕ ) ∧ sup ( ran ( abs ∘ 𝑓 ) , ℝ , < ) < 𝑗 ) → 𝑓 Fn 𝑋 )
24 simplll ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) ∧ 𝑗 ∈ ℕ ) ∧ sup ( ran ( abs ∘ 𝑓 ) , ℝ , < ) < 𝑗 ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) )
25 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) ∧ 𝑗 ∈ ℕ ) ∧ sup ( ran ( abs ∘ 𝑓 ) , ℝ , < ) < 𝑗 ) ∧ 𝑖 ∈ 𝑋 ) → 𝑗 ∈ ℕ )
26 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) ∧ 𝑗 ∈ ℕ ) ∧ sup ( ran ( abs ∘ 𝑓 ) , ℝ , < ) < 𝑗 ) ∧ 𝑖 ∈ 𝑋 ) → sup ( ran ( abs ∘ 𝑓 ) , ℝ , < ) < 𝑗 )
27 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) ∧ 𝑗 ∈ ℕ ) ∧ sup ( ran ( abs ∘ 𝑓 ) , ℝ , < ) < 𝑗 ) ∧ 𝑖 ∈ 𝑋 ) → 𝑖 ∈ 𝑋 )
28 nnnegz ⊢ ( 𝑗 ∈ ℕ → - 𝑗 ∈ ℤ )
29 28 zxrd ⊢ ( 𝑗 ∈ ℕ → - 𝑗 ∈ ℝ* )
30 29 adantr ⊢ ( ( 𝑗 ∈ ℕ ∧ 𝑖 ∈ 𝑋 ) → - 𝑗 ∈ ℝ* )
31 30 3ad2antl2 ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) ∧ 𝑗 ∈ ℕ ∧ sup ( ran ( abs ∘ 𝑓 ) , ℝ , < ) < 𝑗 ) ∧ 𝑖 ∈ 𝑋 ) → - 𝑗 ∈ ℝ* )
32 nnxr ⊢ ( 𝑗 ∈ ℕ → 𝑗 ∈ ℝ* )
33 32 adantr ⊢ ( ( 𝑗 ∈ ℕ ∧ 𝑖 ∈ 𝑋 ) → 𝑗 ∈ ℝ* )
34 33 3ad2antl2 ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) ∧ 𝑗 ∈ ℕ ∧ sup ( ran ( abs ∘ 𝑓 ) , ℝ , < ) < 𝑗 ) ∧ 𝑖 ∈ 𝑋 ) → 𝑗 ∈ ℝ* )
35 20 3ad2ant1 ⊢ ( ( 𝑓 ∈ ( ℝ ↑m 𝑋 ) ∧ 𝑗 ∈ ℕ ∧ sup ( ran ( abs ∘ 𝑓 ) , ℝ , < ) < 𝑗 ) → 𝑓 : 𝑋 ⟶ ℝ )
36 35 frexr ⊢ ( ( 𝑓 ∈ ( ℝ ↑m 𝑋 ) ∧ 𝑗 ∈ ℕ ∧ sup ( ran ( abs ∘ 𝑓 ) , ℝ , < ) < 𝑗 ) → 𝑓 : 𝑋 ⟶ ℝ* )
37 36 3adant1l ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) ∧ 𝑗 ∈ ℕ ∧ sup ( ran ( abs ∘ 𝑓 ) , ℝ , < ) < 𝑗 ) → 𝑓 : 𝑋 ⟶ ℝ* )
38 37 ffvelcdmda ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) ∧ 𝑗 ∈ ℕ ∧ sup ( ran ( abs ∘ 𝑓 ) , ℝ , < ) < 𝑗 ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑖 ) ∈ ℝ* )
39 nnre ⊢ ( 𝑗 ∈ ℕ → 𝑗 ∈ ℝ )
40 39 adantr ⊢ ( ( 𝑗 ∈ ℕ ∧ 𝑖 ∈ 𝑋 ) → 𝑗 ∈ ℝ )
41 40 3ad2antl2 ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) ∧ 𝑗 ∈ ℕ ∧ sup ( ran ( abs ∘ 𝑓 ) , ℝ , < ) < 𝑗 ) ∧ 𝑖 ∈ 𝑋 ) → 𝑗 ∈ ℝ )
42 41 renegcld ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) ∧ 𝑗 ∈ ℕ ∧ sup ( ran ( abs ∘ 𝑓 ) , ℝ , < ) < 𝑗 ) ∧ 𝑖 ∈ 𝑋 ) → - 𝑗 ∈ ℝ )
43 21 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑖 ) ∈ ℝ )
44 43 3ad2antl1 ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) ∧ 𝑗 ∈ ℕ ∧ sup ( ran ( abs ∘ 𝑓 ) , ℝ , < ) < 𝑗 ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑖 ) ∈ ℝ )
45 44 renegcld ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) ∧ 𝑗 ∈ ℕ ∧ sup ( ran ( abs ∘ 𝑓 ) , ℝ , < ) < 𝑗 ) ∧ 𝑖 ∈ 𝑋 ) → - ( 𝑓 ‘ 𝑖 ) ∈ ℝ )
46 n0i ⊢ ( 𝑖 ∈ 𝑋 → ¬ 𝑋 = ∅ )
47 rncoss ⊢ ran ( abs ∘ 𝑓 ) ⊆ ran abs
48 absf ⊢ abs : ℂ ⟶ ℝ
49 frn ⊢ ( abs : ℂ ⟶ ℝ → ran abs ⊆ ℝ )
50 48 49 ax-mp ⊢ ran abs ⊆ ℝ
51 47 50 sstri ⊢ ran ( abs ∘ 𝑓 ) ⊆ ℝ
52 ltso ⊢ < Or ℝ
53 52 a1i ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) ∧ ¬ 𝑋 = ∅ ) → < Or ℝ )
54 48 a1i ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) → abs : ℂ ⟶ ℝ )
55 ax-resscn ⊢ ℝ ⊆ ℂ
56 55 a1i ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) → ℝ ⊆ ℂ )
57 54 56 21 fcoss ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) → ( abs ∘ 𝑓 ) : 𝑋 ⟶ ℝ )
58 2 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) → 𝑋 ∈ Fin )
59 rnffi ⊢ ( ( ( abs ∘ 𝑓 ) : 𝑋 ⟶ ℝ ∧ 𝑋 ∈ Fin ) → ran ( abs ∘ 𝑓 ) ∈ Fin )
60 57 58 59 syl2anc ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) → ran ( abs ∘ 𝑓 ) ∈ Fin )
61 60 adantr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) ∧ ¬ 𝑋 = ∅ ) → ran ( abs ∘ 𝑓 ) ∈ Fin )
62 20 frnd ⊢ ( 𝑓 ∈ ( ℝ ↑m 𝑋 ) → ran 𝑓 ⊆ ℝ )
63 48 fdmi ⊢ dom abs = ℂ
64 63 eqcomi ⊢ ℂ = dom abs
65 55 64 sseqtri ⊢ ℝ ⊆ dom abs
66 62 65 sstrdi ⊢ ( 𝑓 ∈ ( ℝ ↑m 𝑋 ) → ran 𝑓 ⊆ dom abs )
67 dmcosseq ⊢ ( ran 𝑓 ⊆ dom abs → dom ( abs ∘ 𝑓 ) = dom 𝑓 )
68 66 67 syl ⊢ ( 𝑓 ∈ ( ℝ ↑m 𝑋 ) → dom ( abs ∘ 𝑓 ) = dom 𝑓 )
69 20 fdmd ⊢ ( 𝑓 ∈ ( ℝ ↑m 𝑋 ) → dom 𝑓 = 𝑋 )
70 68 69 eqtrd ⊢ ( 𝑓 ∈ ( ℝ ↑m 𝑋 ) → dom ( abs ∘ 𝑓 ) = 𝑋 )
71 70 adantr ⊢ ( ( 𝑓 ∈ ( ℝ ↑m 𝑋 ) ∧ ¬ 𝑋 = ∅ ) → dom ( abs ∘ 𝑓 ) = 𝑋 )
72 neqne ⊢ ( ¬ 𝑋 = ∅ → 𝑋 ≠ ∅ )
73 72 adantl ⊢ ( ( 𝑓 ∈ ( ℝ ↑m 𝑋 ) ∧ ¬ 𝑋 = ∅ ) → 𝑋 ≠ ∅ )
74 71 73 eqnetrd ⊢ ( ( 𝑓 ∈ ( ℝ ↑m 𝑋 ) ∧ ¬ 𝑋 = ∅ ) → dom ( abs ∘ 𝑓 ) ≠ ∅ )
75 74 neneqd ⊢ ( ( 𝑓 ∈ ( ℝ ↑m 𝑋 ) ∧ ¬ 𝑋 = ∅ ) → ¬ dom ( abs ∘ 𝑓 ) = ∅ )
76 dm0rn0 ⊢ ( dom ( abs ∘ 𝑓 ) = ∅ ↔ ran ( abs ∘ 𝑓 ) = ∅ )
77 75 76 sylnib ⊢ ( ( 𝑓 ∈ ( ℝ ↑m 𝑋 ) ∧ ¬ 𝑋 = ∅ ) → ¬ ran ( abs ∘ 𝑓 ) = ∅ )
78 77 neqned ⊢ ( ( 𝑓 ∈ ( ℝ ↑m 𝑋 ) ∧ ¬ 𝑋 = ∅ ) → ran ( abs ∘ 𝑓 ) ≠ ∅ )
79 78 adantll ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) ∧ ¬ 𝑋 = ∅ ) → ran ( abs ∘ 𝑓 ) ≠ ∅ )
80 51 a1i ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) ∧ ¬ 𝑋 = ∅ ) → ran ( abs ∘ 𝑓 ) ⊆ ℝ )
81 fisupcl ⊢ ( ( < Or ℝ ∧ ( ran ( abs ∘ 𝑓 ) ∈ Fin ∧ ran ( abs ∘ 𝑓 ) ≠ ∅ ∧ ran ( abs ∘ 𝑓 ) ⊆ ℝ ) ) → sup ( ran ( abs ∘ 𝑓 ) , ℝ , < ) ∈ ran ( abs ∘ 𝑓 ) )
82 53 61 79 80 81 syl13anc ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) ∧ ¬ 𝑋 = ∅ ) → sup ( ran ( abs ∘ 𝑓 ) , ℝ , < ) ∈ ran ( abs ∘ 𝑓 ) )
83 51 82 sselid ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) ∧ ¬ 𝑋 = ∅ ) → sup ( ran ( abs ∘ 𝑓 ) , ℝ , < ) ∈ ℝ )
84 46 83 sylan2 ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) ∧ 𝑖 ∈ 𝑋 ) → sup ( ran ( abs ∘ 𝑓 ) , ℝ , < ) ∈ ℝ )
85 84 3ad2antl1 ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) ∧ 𝑗 ∈ ℕ ∧ sup ( ran ( abs ∘ 𝑓 ) , ℝ , < ) < 𝑗 ) ∧ 𝑖 ∈ 𝑋 ) → sup ( ran ( abs ∘ 𝑓 ) , ℝ , < ) ∈ ℝ )
86 20 ffvelcdmda ⊢ ( ( 𝑓 ∈ ( ℝ ↑m 𝑋 ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑖 ) ∈ ℝ )
87 86 recnd ⊢ ( ( 𝑓 ∈ ( ℝ ↑m 𝑋 ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑖 ) ∈ ℂ )
88 87 abscld ⊢ ( ( 𝑓 ∈ ( ℝ ↑m 𝑋 ) ∧ 𝑖 ∈ 𝑋 ) → ( abs ‘ ( 𝑓 ‘ 𝑖 ) ) ∈ ℝ )
89 88 adantll ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) ∧ 𝑖 ∈ 𝑋 ) → ( abs ‘ ( 𝑓 ‘ 𝑖 ) ) ∈ ℝ )
90 89 3ad2antl1 ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) ∧ 𝑗 ∈ ℕ ∧ sup ( ran ( abs ∘ 𝑓 ) , ℝ , < ) < 𝑗 ) ∧ 𝑖 ∈ 𝑋 ) → ( abs ‘ ( 𝑓 ‘ 𝑖 ) ) ∈ ℝ )
91 86 renegcld ⊢ ( ( 𝑓 ∈ ( ℝ ↑m 𝑋 ) ∧ 𝑖 ∈ 𝑋 ) → - ( 𝑓 ‘ 𝑖 ) ∈ ℝ )
92 91 leabsd ⊢ ( ( 𝑓 ∈ ( ℝ ↑m 𝑋 ) ∧ 𝑖 ∈ 𝑋 ) → - ( 𝑓 ‘ 𝑖 ) ≤ ( abs ‘ - ( 𝑓 ‘ 𝑖 ) ) )
93 87 absnegd ⊢ ( ( 𝑓 ∈ ( ℝ ↑m 𝑋 ) ∧ 𝑖 ∈ 𝑋 ) → ( abs ‘ - ( 𝑓 ‘ 𝑖 ) ) = ( abs ‘ ( 𝑓 ‘ 𝑖 ) ) )
94 92 93 breqtrd ⊢ ( ( 𝑓 ∈ ( ℝ ↑m 𝑋 ) ∧ 𝑖 ∈ 𝑋 ) → - ( 𝑓 ‘ 𝑖 ) ≤ ( abs ‘ ( 𝑓 ‘ 𝑖 ) ) )
95 94 adantll ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) ∧ 𝑖 ∈ 𝑋 ) → - ( 𝑓 ‘ 𝑖 ) ≤ ( abs ‘ ( 𝑓 ‘ 𝑖 ) ) )
96 95 3ad2antl1 ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) ∧ 𝑗 ∈ ℕ ∧ sup ( ran ( abs ∘ 𝑓 ) , ℝ , < ) < 𝑗 ) ∧ 𝑖 ∈ 𝑋 ) → - ( 𝑓 ‘ 𝑖 ) ≤ ( abs ‘ ( 𝑓 ‘ 𝑖 ) ) )
97 51 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) ∧ 𝑗 ∈ ℕ ∧ sup ( ran ( abs ∘ 𝑓 ) , ℝ , < ) < 𝑗 ) ∧ 𝑖 ∈ 𝑋 ) → ran ( abs ∘ 𝑓 ) ⊆ ℝ )
98 46 79 sylan2 ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) ∧ 𝑖 ∈ 𝑋 ) → ran ( abs ∘ 𝑓 ) ≠ ∅ )
99 98 3ad2antl1 ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) ∧ 𝑗 ∈ ℕ ∧ sup ( ran ( abs ∘ 𝑓 ) , ℝ , < ) < 𝑗 ) ∧ 𝑖 ∈ 𝑋 ) → ran ( abs ∘ 𝑓 ) ≠ ∅ )
100 fimaxre2 ⊢ ( ( ran ( abs ∘ 𝑓 ) ⊆ ℝ ∧ ran ( abs ∘ 𝑓 ) ∈ Fin ) → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran ( abs ∘ 𝑓 ) 𝑧 ≤ 𝑦 )
101 51 60 100 sylancr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran ( abs ∘ 𝑓 ) 𝑧 ≤ 𝑦 )
102 101 adantr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) ∧ 𝑖 ∈ 𝑋 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran ( abs ∘ 𝑓 ) 𝑧 ≤ 𝑦 )
103 102 3ad2antl1 ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) ∧ 𝑗 ∈ ℕ ∧ sup ( ran ( abs ∘ 𝑓 ) , ℝ , < ) < 𝑗 ) ∧ 𝑖 ∈ 𝑋 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran ( abs ∘ 𝑓 ) 𝑧 ≤ 𝑦 )
104 elmapfun ⊢ ( 𝑓 ∈ ( ℝ ↑m 𝑋 ) → Fun 𝑓 )
105 simpr ⊢ ( ( 𝑓 ∈ ( ℝ ↑m 𝑋 ) ∧ 𝑖 ∈ 𝑋 ) → 𝑖 ∈ 𝑋 )
106 69 eqcomd ⊢ ( 𝑓 ∈ ( ℝ ↑m 𝑋 ) → 𝑋 = dom 𝑓 )
107 106 adantr ⊢ ( ( 𝑓 ∈ ( ℝ ↑m 𝑋 ) ∧ 𝑖 ∈ 𝑋 ) → 𝑋 = dom 𝑓 )
108 105 107 eleqtrd ⊢ ( ( 𝑓 ∈ ( ℝ ↑m 𝑋 ) ∧ 𝑖 ∈ 𝑋 ) → 𝑖 ∈ dom 𝑓 )
109 fvco ⊢ ( ( Fun 𝑓 ∧ 𝑖 ∈ dom 𝑓 ) → ( ( abs ∘ 𝑓 ) ‘ 𝑖 ) = ( abs ‘ ( 𝑓 ‘ 𝑖 ) ) )
110 104 108 109 syl2an2r ⊢ ( ( 𝑓 ∈ ( ℝ ↑m 𝑋 ) ∧ 𝑖 ∈ 𝑋 ) → ( ( abs ∘ 𝑓 ) ‘ 𝑖 ) = ( abs ‘ ( 𝑓 ‘ 𝑖 ) ) )
111 absfun ⊢ Fun abs
112 funco ⊢ ( ( Fun abs ∧ Fun 𝑓 ) → Fun ( abs ∘ 𝑓 ) )
113 111 104 112 sylancr ⊢ ( 𝑓 ∈ ( ℝ ↑m 𝑋 ) → Fun ( abs ∘ 𝑓 ) )
114 87 64 eleqtrdi ⊢ ( ( 𝑓 ∈ ( ℝ ↑m 𝑋 ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑖 ) ∈ dom abs )
115 dmfco ⊢ ( ( Fun 𝑓 ∧ 𝑖 ∈ dom 𝑓 ) → ( 𝑖 ∈ dom ( abs ∘ 𝑓 ) ↔ ( 𝑓 ‘ 𝑖 ) ∈ dom abs ) )
116 104 108 115 syl2an2r ⊢ ( ( 𝑓 ∈ ( ℝ ↑m 𝑋 ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑖 ∈ dom ( abs ∘ 𝑓 ) ↔ ( 𝑓 ‘ 𝑖 ) ∈ dom abs ) )
117 114 116 mpbird ⊢ ( ( 𝑓 ∈ ( ℝ ↑m 𝑋 ) ∧ 𝑖 ∈ 𝑋 ) → 𝑖 ∈ dom ( abs ∘ 𝑓 ) )
118 fvelrn ⊢ ( ( Fun ( abs ∘ 𝑓 ) ∧ 𝑖 ∈ dom ( abs ∘ 𝑓 ) ) → ( ( abs ∘ 𝑓 ) ‘ 𝑖 ) ∈ ran ( abs ∘ 𝑓 ) )
119 113 117 118 syl2an2r ⊢ ( ( 𝑓 ∈ ( ℝ ↑m 𝑋 ) ∧ 𝑖 ∈ 𝑋 ) → ( ( abs ∘ 𝑓 ) ‘ 𝑖 ) ∈ ran ( abs ∘ 𝑓 ) )
120 110 119 eqeltrrd ⊢ ( ( 𝑓 ∈ ( ℝ ↑m 𝑋 ) ∧ 𝑖 ∈ 𝑋 ) → ( abs ‘ ( 𝑓 ‘ 𝑖 ) ) ∈ ran ( abs ∘ 𝑓 ) )
121 120 adantll ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) ∧ 𝑖 ∈ 𝑋 ) → ( abs ‘ ( 𝑓 ‘ 𝑖 ) ) ∈ ran ( abs ∘ 𝑓 ) )
122 121 3ad2antl1 ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) ∧ 𝑗 ∈ ℕ ∧ sup ( ran ( abs ∘ 𝑓 ) , ℝ , < ) < 𝑗 ) ∧ 𝑖 ∈ 𝑋 ) → ( abs ‘ ( 𝑓 ‘ 𝑖 ) ) ∈ ran ( abs ∘ 𝑓 ) )
123 97 99 103 122 suprubd ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) ∧ 𝑗 ∈ ℕ ∧ sup ( ran ( abs ∘ 𝑓 ) , ℝ , < ) < 𝑗 ) ∧ 𝑖 ∈ 𝑋 ) → ( abs ‘ ( 𝑓 ‘ 𝑖 ) ) ≤ sup ( ran ( abs ∘ 𝑓 ) , ℝ , < ) )
124 45 90 85 96 123 letrd ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) ∧ 𝑗 ∈ ℕ ∧ sup ( ran ( abs ∘ 𝑓 ) , ℝ , < ) < 𝑗 ) ∧ 𝑖 ∈ 𝑋 ) → - ( 𝑓 ‘ 𝑖 ) ≤ sup ( ran ( abs ∘ 𝑓 ) , ℝ , < ) )
125 simpl3 ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) ∧ 𝑗 ∈ ℕ ∧ sup ( ran ( abs ∘ 𝑓 ) , ℝ , < ) < 𝑗 ) ∧ 𝑖 ∈ 𝑋 ) → sup ( ran ( abs ∘ 𝑓 ) , ℝ , < ) < 𝑗 )
126 45 85 41 124 125 lelttrd ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) ∧ 𝑗 ∈ ℕ ∧ sup ( ran ( abs ∘ 𝑓 ) , ℝ , < ) < 𝑗 ) ∧ 𝑖 ∈ 𝑋 ) → - ( 𝑓 ‘ 𝑖 ) < 𝑗 )
127 44 41 126 ltnegcon1d ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) ∧ 𝑗 ∈ ℕ ∧ sup ( ran ( abs ∘ 𝑓 ) , ℝ , < ) < 𝑗 ) ∧ 𝑖 ∈ 𝑋 ) → - 𝑗 < ( 𝑓 ‘ 𝑖 ) )
128 42 44 127 ltled ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) ∧ 𝑗 ∈ ℕ ∧ sup ( ran ( abs ∘ 𝑓 ) , ℝ , < ) < 𝑗 ) ∧ 𝑖 ∈ 𝑋 ) → - 𝑗 ≤ ( 𝑓 ‘ 𝑖 ) )
129 44 leabsd ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) ∧ 𝑗 ∈ ℕ ∧ sup ( ran ( abs ∘ 𝑓 ) , ℝ , < ) < 𝑗 ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑖 ) ≤ ( abs ‘ ( 𝑓 ‘ 𝑖 ) ) )
130 44 90 85 129 123 letrd ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) ∧ 𝑗 ∈ ℕ ∧ sup ( ran ( abs ∘ 𝑓 ) , ℝ , < ) < 𝑗 ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑖 ) ≤ sup ( ran ( abs ∘ 𝑓 ) , ℝ , < ) )
131 44 85 41 130 125 lelttrd ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) ∧ 𝑗 ∈ ℕ ∧ sup ( ran ( abs ∘ 𝑓 ) , ℝ , < ) < 𝑗 ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑖 ) < 𝑗 )
132 31 34 38 128 131 elicod ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) ∧ 𝑗 ∈ ℕ ∧ sup ( ran ( abs ∘ 𝑓 ) , ℝ , < ) < 𝑗 ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑖 ) ∈ ( - 𝑗 [,) 𝑗 ) )
133 24 25 26 27 132 syl31anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) ∧ 𝑗 ∈ ℕ ) ∧ sup ( ran ( abs ∘ 𝑓 ) , ℝ , < ) < 𝑗 ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑖 ) ∈ ( - 𝑗 [,) 𝑗 ) )
134 133 adantl3r ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) ∧ ¬ 𝑋 = ∅ ) ∧ 𝑗 ∈ ℕ ) ∧ sup ( ran ( abs ∘ 𝑓 ) , ℝ , < ) < 𝑗 ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑖 ) ∈ ( - 𝑗 [,) 𝑗 ) )
135 simpr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ ℕ )
136 fconstmpt ⊢ ( 𝑋 × { ⟨ - 𝑗 , 𝑗 ⟩ } ) = ( 𝑥 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ )
137 snex ⊢ { ⟨ - 𝑗 , 𝑗 ⟩ } ∈ V
138 137 a1i ⊢ ( 𝜑 → { ⟨ - 𝑗 , 𝑗 ⟩ } ∈ V )
139 2 138 xpexd ⊢ ( 𝜑 → ( 𝑋 × { ⟨ - 𝑗 , 𝑗 ⟩ } ) ∈ V )
140 136 139 eqeltrrid ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ∈ V )
141 140 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝑥 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ∈ V )
142 1 fvmpt2 ⊢ ( ( 𝑗 ∈ ℕ ∧ ( 𝑥 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ∈ V ) → ( 𝐼 ‘ 𝑗 ) = ( 𝑥 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) )
143 135 141 142 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐼 ‘ 𝑗 ) = ( 𝑥 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) )
144 143 fveq1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐼 ‘ 𝑗 ) ‘ 𝑖 ) = ( ( 𝑥 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ‘ 𝑖 ) )
145 144 3adant3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝐼 ‘ 𝑗 ) ‘ 𝑖 ) = ( ( 𝑥 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ‘ 𝑖 ) )
146 eqidd ⊢ ( 𝑖 ∈ 𝑋 → ( 𝑥 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) = ( 𝑥 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) )
147 eqidd ⊢ ( ( 𝑖 ∈ 𝑋 ∧ 𝑥 = 𝑖 ) → ⟨ - 𝑗 , 𝑗 ⟩ = ⟨ - 𝑗 , 𝑗 ⟩ )
148 id ⊢ ( 𝑖 ∈ 𝑋 → 𝑖 ∈ 𝑋 )
149 opex ⊢ ⟨ - 𝑗 , 𝑗 ⟩ ∈ V
150 149 a1i ⊢ ( 𝑖 ∈ 𝑋 → ⟨ - 𝑗 , 𝑗 ⟩ ∈ V )
151 146 147 148 150 fvmptd ⊢ ( 𝑖 ∈ 𝑋 → ( ( 𝑥 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ‘ 𝑖 ) = ⟨ - 𝑗 , 𝑗 ⟩ )
152 151 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝑥 ∈ 𝑋 ↦ ⟨ - 𝑗 , 𝑗 ⟩ ) ‘ 𝑖 ) = ⟨ - 𝑗 , 𝑗 ⟩ )
153 145 152 eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝐼 ‘ 𝑗 ) ‘ 𝑖 ) = ⟨ - 𝑗 , 𝑗 ⟩ )
154 153 fveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑖 ∈ 𝑋 ) → ( 1st ‘ ( ( 𝐼 ‘ 𝑗 ) ‘ 𝑖 ) ) = ( 1st ‘ ⟨ - 𝑗 , 𝑗 ⟩ ) )
155 negex ⊢ - 𝑗 ∈ V
156 vex ⊢ 𝑗 ∈ V
157 155 156 op1st ⊢ ( 1st ‘ ⟨ - 𝑗 , 𝑗 ⟩ ) = - 𝑗
158 154 157 eqtrdi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑖 ∈ 𝑋 ) → ( 1st ‘ ( ( 𝐼 ‘ 𝑗 ) ‘ 𝑖 ) ) = - 𝑗 )
159 153 fveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑖 ∈ 𝑋 ) → ( 2nd ‘ ( ( 𝐼 ‘ 𝑗 ) ‘ 𝑖 ) ) = ( 2nd ‘ ⟨ - 𝑗 , 𝑗 ⟩ ) )
160 155 156 op2nd ⊢ ( 2nd ‘ ⟨ - 𝑗 , 𝑗 ⟩ ) = 𝑗
161 159 160 eqtrdi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑖 ∈ 𝑋 ) → ( 2nd ‘ ( ( 𝐼 ‘ 𝑗 ) ‘ 𝑖 ) ) = 𝑗 )
162 158 161 oveq12d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑖 ∈ 𝑋 ) → ( ( 1st ‘ ( ( 𝐼 ‘ 𝑗 ) ‘ 𝑖 ) ) [,) ( 2nd ‘ ( ( 𝐼 ‘ 𝑗 ) ‘ 𝑖 ) ) ) = ( - 𝑗 [,) 𝑗 ) )
163 162 eqcomd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑖 ∈ 𝑋 ) → ( - 𝑗 [,) 𝑗 ) = ( ( 1st ‘ ( ( 𝐼 ‘ 𝑗 ) ‘ 𝑖 ) ) [,) ( 2nd ‘ ( ( 𝐼 ‘ 𝑗 ) ‘ 𝑖 ) ) ) )
164 163 3adant1r ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) ∧ 𝑗 ∈ ℕ ∧ 𝑖 ∈ 𝑋 ) → ( - 𝑗 [,) 𝑗 ) = ( ( 1st ‘ ( ( 𝐼 ‘ 𝑗 ) ‘ 𝑖 ) ) [,) ( 2nd ‘ ( ( 𝐼 ‘ 𝑗 ) ‘ 𝑖 ) ) ) )
165 164 ad5ant135 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) ∧ ¬ 𝑋 = ∅ ) ∧ 𝑗 ∈ ℕ ) ∧ sup ( ran ( abs ∘ 𝑓 ) , ℝ , < ) < 𝑗 ) ∧ 𝑖 ∈ 𝑋 ) → ( - 𝑗 [,) 𝑗 ) = ( ( 1st ‘ ( ( 𝐼 ‘ 𝑗 ) ‘ 𝑖 ) ) [,) ( 2nd ‘ ( ( 𝐼 ‘ 𝑗 ) ‘ 𝑖 ) ) ) )
166 134 165 eleqtrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) ∧ ¬ 𝑋 = ∅ ) ∧ 𝑗 ∈ ℕ ) ∧ sup ( ran ( abs ∘ 𝑓 ) , ℝ , < ) < 𝑗 ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑖 ) ∈ ( ( 1st ‘ ( ( 𝐼 ‘ 𝑗 ) ‘ 𝑖 ) ) [,) ( 2nd ‘ ( ( 𝐼 ‘ 𝑗 ) ‘ 𝑖 ) ) ) )
167 28 zred ⊢ ( 𝑗 ∈ ℕ → - 𝑗 ∈ ℝ )
168 167 39 opelxpd ⊢ ( 𝑗 ∈ ℕ → ⟨ - 𝑗 , 𝑗 ⟩ ∈ ( ℝ × ℝ ) )
169 168 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑥 ∈ 𝑋 ) → ⟨ - 𝑗 , 𝑗 ⟩ ∈ ( ℝ × ℝ ) )
170 143 169 fmpt3d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐼 ‘ 𝑗 ) : 𝑋 ⟶ ( ℝ × ℝ ) )
171 170 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) ∧ ¬ 𝑋 = ∅ ) ∧ 𝑗 ∈ ℕ ) → ( 𝐼 ‘ 𝑗 ) : 𝑋 ⟶ ( ℝ × ℝ ) )
172 171 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) ∧ ¬ 𝑋 = ∅ ) ∧ 𝑗 ∈ ℕ ) ∧ sup ( ran ( abs ∘ 𝑓 ) , ℝ , < ) < 𝑗 ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝐼 ‘ 𝑗 ) : 𝑋 ⟶ ( ℝ × ℝ ) )
173 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) ∧ ¬ 𝑋 = ∅ ) ∧ 𝑗 ∈ ℕ ) ∧ sup ( ran ( abs ∘ 𝑓 ) , ℝ , < ) < 𝑗 ) ∧ 𝑖 ∈ 𝑋 ) → 𝑖 ∈ 𝑋 )
174 172 173 fvovco ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) ∧ ¬ 𝑋 = ∅ ) ∧ 𝑗 ∈ ℕ ) ∧ sup ( ran ( abs ∘ 𝑓 ) , ℝ , < ) < 𝑗 ) ∧ 𝑖 ∈ 𝑋 ) → ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑖 ) = ( ( 1st ‘ ( ( 𝐼 ‘ 𝑗 ) ‘ 𝑖 ) ) [,) ( 2nd ‘ ( ( 𝐼 ‘ 𝑗 ) ‘ 𝑖 ) ) ) )
175 166 174 eleqtrrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) ∧ ¬ 𝑋 = ∅ ) ∧ 𝑗 ∈ ℕ ) ∧ sup ( ran ( abs ∘ 𝑓 ) , ℝ , < ) < 𝑗 ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑖 ) ∈ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑖 ) )
176 175 ralrimiva ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) ∧ ¬ 𝑋 = ∅ ) ∧ 𝑗 ∈ ℕ ) ∧ sup ( ran ( abs ∘ 𝑓 ) , ℝ , < ) < 𝑗 ) → ∀ 𝑖 ∈ 𝑋 ( 𝑓 ‘ 𝑖 ) ∈ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑖 ) )
177 vex ⊢ 𝑓 ∈ V
178 177 elixp ⊢ ( 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑖 ) ↔ ( 𝑓 Fn 𝑋 ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑓 ‘ 𝑖 ) ∈ ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑖 ) ) )
179 23 176 178 sylanbrc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) ∧ ¬ 𝑋 = ∅ ) ∧ 𝑗 ∈ ℕ ) ∧ sup ( ran ( abs ∘ 𝑓 ) , ℝ , < ) < 𝑗 ) → 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑖 ) )
180 83 archd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) ∧ ¬ 𝑋 = ∅ ) → ∃ 𝑗 ∈ ℕ sup ( ran ( abs ∘ 𝑓 ) , ℝ , < ) < 𝑗 )
181 179 180 reximddv3 ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) ∧ ¬ 𝑋 = ∅ ) → ∃ 𝑗 ∈ ℕ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑖 ) )
182 181 an32s ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) → ∃ 𝑗 ∈ ℕ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑖 ) )
183 182 eliund ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) → 𝑓 ∈ ∪ 𝑗 ∈ ℕ X 𝑖 ∈ 𝑋 ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑖 ) )
184 183 ssd ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → ( ℝ ↑m 𝑋 ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑖 ∈ 𝑋 ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑖 ) )
185 19 184 pm2.61dan ⊢ ( 𝜑 → ( ℝ ↑m 𝑋 ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑖 ∈ 𝑋 ( ( [,) ∘ ( 𝐼 ‘ 𝑗 ) ) ‘ 𝑖 ) )