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