Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  hoicvr Structured version   Visualization version   GIF version

Theorem hoicvr 45817
Description: 𝐼 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.)
Hypotheses
Ref Expression
hoicvr.2 𝐼 = (𝑗 ∈ β„• ↦ (π‘₯ ∈ 𝑋 ↦ ⟨-𝑗, π‘—βŸ©))
hoicvr.3 (πœ‘ β†’ 𝑋 ∈ Fin)
Assertion
Ref Expression
hoicvr (πœ‘ β†’ (ℝ ↑m 𝑋) βŠ† βˆͺ 𝑗 ∈ β„• X𝑖 ∈ 𝑋 (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–))
Distinct variable groups:   𝑖,𝑋,𝑗,π‘₯   πœ‘,𝑖,𝑗,π‘₯
Allowed substitution hints:   𝐼(π‘₯,𝑖,𝑗)

Proof of Theorem hoicvr
Dummy variables 𝑓 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 reex 11200 . . . . . . 7 ℝ ∈ V
2 mapdm0 8835 . . . . . . 7 (ℝ ∈ V β†’ (ℝ ↑m βˆ…) = {βˆ…})
31, 2ax-mp 5 . . . . . 6 (ℝ ↑m βˆ…) = {βˆ…}
43a1i 11 . . . . 5 (𝑋 = βˆ… β†’ (ℝ ↑m βˆ…) = {βˆ…})
5 oveq2 7412 . . . . 5 (𝑋 = βˆ… β†’ (ℝ ↑m 𝑋) = (ℝ ↑m βˆ…))
6 ixpeq1 8901 . . . . . . 7 (𝑋 = βˆ… β†’ X𝑖 ∈ 𝑋 (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–) = X𝑖 ∈ βˆ… (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–))
76iuneq2d 5019 . . . . . 6 (𝑋 = βˆ… β†’ βˆͺ 𝑗 ∈ β„• X𝑖 ∈ 𝑋 (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–) = βˆͺ 𝑗 ∈ β„• X𝑖 ∈ βˆ… (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–))
8 ixp0x 8919 . . . . . . . . . 10 X𝑖 ∈ βˆ… (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–) = {βˆ…}
98a1i 11 . . . . . . . . 9 (𝑗 ∈ β„• β†’ X𝑖 ∈ βˆ… (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–) = {βˆ…})
109iuneq2i 5011 . . . . . . . 8 βˆͺ 𝑗 ∈ β„• X𝑖 ∈ βˆ… (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–) = βˆͺ 𝑗 ∈ β„• {βˆ…}
11 1nn 12224 . . . . . . . . . 10 1 ∈ β„•
1211ne0ii 4332 . . . . . . . . 9 β„• β‰  βˆ…
13 iunconst 4999 . . . . . . . . 9 (β„• β‰  βˆ… β†’ βˆͺ 𝑗 ∈ β„• {βˆ…} = {βˆ…})
1412, 13ax-mp 5 . . . . . . . 8 βˆͺ 𝑗 ∈ β„• {βˆ…} = {βˆ…}
1510, 14eqtri 2754 . . . . . . 7 βˆͺ 𝑗 ∈ β„• X𝑖 ∈ βˆ… (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–) = {βˆ…}
1615a1i 11 . . . . . 6 (𝑋 = βˆ… β†’ βˆͺ 𝑗 ∈ β„• X𝑖 ∈ βˆ… (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–) = {βˆ…})
177, 16eqtrd 2766 . . . . 5 (𝑋 = βˆ… β†’ βˆͺ 𝑗 ∈ β„• X𝑖 ∈ 𝑋 (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–) = {βˆ…})
184, 5, 173eqtr4d 2776 . . . 4 (𝑋 = βˆ… β†’ (ℝ ↑m 𝑋) = βˆͺ 𝑗 ∈ β„• X𝑖 ∈ 𝑋 (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–))
19 eqimss 4035 . . . 4 ((ℝ ↑m 𝑋) = βˆͺ 𝑗 ∈ β„• X𝑖 ∈ 𝑋 (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–) β†’ (ℝ ↑m 𝑋) βŠ† βˆͺ 𝑗 ∈ β„• X𝑖 ∈ 𝑋 (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–))
2018, 19syl 17 . . 3 (𝑋 = βˆ… β†’ (ℝ ↑m 𝑋) βŠ† βˆͺ 𝑗 ∈ β„• X𝑖 ∈ 𝑋 (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–))
2120adantl 481 . 2 ((πœ‘ ∧ 𝑋 = βˆ…) β†’ (ℝ ↑m 𝑋) βŠ† βˆͺ 𝑗 ∈ β„• X𝑖 ∈ 𝑋 (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–))
22 simpll 764 . . . . . 6 (((πœ‘ ∧ Β¬ 𝑋 = βˆ…) ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) β†’ πœ‘)
23 simpr 484 . . . . . 6 (((πœ‘ ∧ Β¬ 𝑋 = βˆ…) ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) β†’ 𝑓 ∈ (ℝ ↑m 𝑋))
24 simplr 766 . . . . . 6 (((πœ‘ ∧ Β¬ 𝑋 = βˆ…) ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) β†’ Β¬ 𝑋 = βˆ…)
25 rncoss 5964 . . . . . . . . . . 11 ran (abs ∘ 𝑓) βŠ† ran abs
26 absf 15288 . . . . . . . . . . . 12 abs:β„‚βŸΆβ„
27 frn 6717 . . . . . . . . . . . 12 (abs:β„‚βŸΆβ„ β†’ ran abs βŠ† ℝ)
2826, 27ax-mp 5 . . . . . . . . . . 11 ran abs βŠ† ℝ
2925, 28sstri 3986 . . . . . . . . . 10 ran (abs ∘ 𝑓) βŠ† ℝ
3029a1i 11 . . . . . . . . 9 (((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) β†’ ran (abs ∘ 𝑓) βŠ† ℝ)
31 ltso 11295 . . . . . . . . . . 11 < Or ℝ
3231a1i 11 . . . . . . . . . 10 (((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) β†’ < Or ℝ)
3326a1i 11 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) β†’ abs:β„‚βŸΆβ„)
34 elmapi 8842 . . . . . . . . . . . . . . 15 (𝑓 ∈ (ℝ ↑m 𝑋) β†’ 𝑓:π‘‹βŸΆβ„)
3534adantl 481 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) β†’ 𝑓:π‘‹βŸΆβ„)
36 ax-resscn 11166 . . . . . . . . . . . . . . 15 ℝ βŠ† β„‚
3736a1i 11 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) β†’ ℝ βŠ† β„‚)
3835, 37fssd 6728 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) β†’ 𝑓:π‘‹βŸΆβ„‚)
39 fco 6734 . . . . . . . . . . . . 13 ((abs:β„‚βŸΆβ„ ∧ 𝑓:π‘‹βŸΆβ„‚) β†’ (abs ∘ 𝑓):π‘‹βŸΆβ„)
4033, 38, 39syl2anc 583 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) β†’ (abs ∘ 𝑓):π‘‹βŸΆβ„)
41 hoicvr.3 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑋 ∈ Fin)
4241adantr 480 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) β†’ 𝑋 ∈ Fin)
43 rnffi 44427 . . . . . . . . . . . 12 (((abs ∘ 𝑓):π‘‹βŸΆβ„ ∧ 𝑋 ∈ Fin) β†’ ran (abs ∘ 𝑓) ∈ Fin)
4440, 42, 43syl2anc 583 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) β†’ ran (abs ∘ 𝑓) ∈ Fin)
4544adantr 480 . . . . . . . . . 10 (((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) β†’ ran (abs ∘ 𝑓) ∈ Fin)
4634frnd 6718 . . . . . . . . . . . . . . . . . . 19 (𝑓 ∈ (ℝ ↑m 𝑋) β†’ ran 𝑓 βŠ† ℝ)
4726fdmi 6722 . . . . . . . . . . . . . . . . . . . . . 22 dom abs = β„‚
4847eqcomi 2735 . . . . . . . . . . . . . . . . . . . . 21 β„‚ = dom abs
4936, 48sseqtri 4013 . . . . . . . . . . . . . . . . . . . 20 ℝ βŠ† dom abs
5049a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝑓 ∈ (ℝ ↑m 𝑋) β†’ ℝ βŠ† dom abs)
5146, 50sstrd 3987 . . . . . . . . . . . . . . . . . 18 (𝑓 ∈ (ℝ ↑m 𝑋) β†’ ran 𝑓 βŠ† dom abs)
52 dmcosseq 5965 . . . . . . . . . . . . . . . . . 18 (ran 𝑓 βŠ† dom abs β†’ dom (abs ∘ 𝑓) = dom 𝑓)
5351, 52syl 17 . . . . . . . . . . . . . . . . 17 (𝑓 ∈ (ℝ ↑m 𝑋) β†’ dom (abs ∘ 𝑓) = dom 𝑓)
5434fdmd 6721 . . . . . . . . . . . . . . . . 17 (𝑓 ∈ (ℝ ↑m 𝑋) β†’ dom 𝑓 = 𝑋)
5553, 54eqtrd 2766 . . . . . . . . . . . . . . . 16 (𝑓 ∈ (ℝ ↑m 𝑋) β†’ dom (abs ∘ 𝑓) = 𝑋)
5655adantr 480 . . . . . . . . . . . . . . 15 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ Β¬ 𝑋 = βˆ…) β†’ dom (abs ∘ 𝑓) = 𝑋)
57 neqne 2942 . . . . . . . . . . . . . . . 16 (Β¬ 𝑋 = βˆ… β†’ 𝑋 β‰  βˆ…)
5857adantl 481 . . . . . . . . . . . . . . 15 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ Β¬ 𝑋 = βˆ…) β†’ 𝑋 β‰  βˆ…)
5956, 58eqnetrd 3002 . . . . . . . . . . . . . 14 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ Β¬ 𝑋 = βˆ…) β†’ dom (abs ∘ 𝑓) β‰  βˆ…)
6059neneqd 2939 . . . . . . . . . . . . 13 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ Β¬ 𝑋 = βˆ…) β†’ Β¬ dom (abs ∘ 𝑓) = βˆ…)
61 dm0rn0 5917 . . . . . . . . . . . . 13 (dom (abs ∘ 𝑓) = βˆ… ↔ ran (abs ∘ 𝑓) = βˆ…)
6260, 61sylnib 328 . . . . . . . . . . . 12 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ Β¬ 𝑋 = βˆ…) β†’ Β¬ ran (abs ∘ 𝑓) = βˆ…)
6362neqned 2941 . . . . . . . . . . 11 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ Β¬ 𝑋 = βˆ…) β†’ ran (abs ∘ 𝑓) β‰  βˆ…)
6463adantll 711 . . . . . . . . . 10 (((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) β†’ ran (abs ∘ 𝑓) β‰  βˆ…)
65 fisupcl 9463 . . . . . . . . . 10 (( < Or ℝ ∧ (ran (abs ∘ 𝑓) ∈ Fin ∧ ran (abs ∘ 𝑓) β‰  βˆ… ∧ ran (abs ∘ 𝑓) βŠ† ℝ)) β†’ sup(ran (abs ∘ 𝑓), ℝ, < ) ∈ ran (abs ∘ 𝑓))
6632, 45, 64, 30, 65syl13anc 1369 . . . . . . . . 9 (((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) β†’ sup(ran (abs ∘ 𝑓), ℝ, < ) ∈ ran (abs ∘ 𝑓))
6730, 66sseldd 3978 . . . . . . . 8 (((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) β†’ sup(ran (abs ∘ 𝑓), ℝ, < ) ∈ ℝ)
68 arch 12470 . . . . . . . 8 (sup(ran (abs ∘ 𝑓), ℝ, < ) ∈ ℝ β†’ βˆƒπ‘— ∈ β„• sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗)
6967, 68syl 17 . . . . . . 7 (((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) β†’ βˆƒπ‘— ∈ β„• sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗)
7035ffnd 6711 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) β†’ 𝑓 Fn 𝑋)
7170ad2antrr 723 . . . . . . . . . . . 12 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) β†’ 𝑓 Fn 𝑋)
7271adantlr 712 . . . . . . . . . . 11 (((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) ∧ 𝑗 ∈ β„•) ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) β†’ 𝑓 Fn 𝑋)
73 simplll 772 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„•) ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ (πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)))
74 id 22 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ β„• β†’ 𝑗 ∈ β„•)
7574ad3antlr 728 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„•) ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ 𝑗 ∈ β„•)
76 simplr 766 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„•) ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗)
77 simpr 484 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„•) ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ 𝑖 ∈ 𝑋)
78 simp2 1134 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) β†’ 𝑗 ∈ β„•)
79 zssre 12566 . . . . . . . . . . . . . . . . . . . . 21 β„€ βŠ† ℝ
80 ressxr 11259 . . . . . . . . . . . . . . . . . . . . 21 ℝ βŠ† ℝ*
8179, 80sstri 3986 . . . . . . . . . . . . . . . . . . . 20 β„€ βŠ† ℝ*
82 nnnegz 12562 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ β„• β†’ -𝑗 ∈ β„€)
8381, 82sselid 3975 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ β„• β†’ -𝑗 ∈ ℝ*)
8483adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝑗 ∈ β„• ∧ 𝑖 ∈ 𝑋) β†’ -𝑗 ∈ ℝ*)
8578, 84sylan 579 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ -𝑗 ∈ ℝ*)
8674nnxrd 44536 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ β„• β†’ 𝑗 ∈ ℝ*)
8786adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝑗 ∈ β„• ∧ 𝑖 ∈ 𝑋) β†’ 𝑗 ∈ ℝ*)
8878, 87sylan 579 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ 𝑗 ∈ ℝ*)
89343ad2ant1 1130 . . . . . . . . . . . . . . . . . . . 20 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) β†’ 𝑓:π‘‹βŸΆβ„)
9080a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) β†’ ℝ βŠ† ℝ*)
9189, 90fssd 6728 . . . . . . . . . . . . . . . . . . 19 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) β†’ 𝑓:π‘‹βŸΆβ„*)
92913adant1l 1173 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) β†’ 𝑓:π‘‹βŸΆβ„*)
9392ffvelcdmda 7079 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ∈ ℝ*)
94 nnre 12220 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ β„• β†’ 𝑗 ∈ ℝ)
9594adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝑗 ∈ β„• ∧ 𝑖 ∈ 𝑋) β†’ 𝑗 ∈ ℝ)
96953ad2antl2 1183 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ 𝑗 ∈ ℝ)
9796renegcld 11642 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ -𝑗 ∈ ℝ)
9835ffvelcdmda 7079 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ∈ ℝ)
99983ad2antl1 1182 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ∈ ℝ)
10099renegcld 11642 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ -(π‘“β€˜π‘–) ∈ ℝ)
101 simpll 764 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖 ∈ 𝑋) β†’ πœ‘)
102 simplr 766 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖 ∈ 𝑋) β†’ 𝑓 ∈ (ℝ ↑m 𝑋))
103 n0i 4328 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑖 ∈ 𝑋 β†’ Β¬ 𝑋 = βˆ…)
104103adantl 481 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖 ∈ 𝑋) β†’ Β¬ 𝑋 = βˆ…)
105101, 102, 104, 67syl21anc 835 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖 ∈ 𝑋) β†’ sup(ran (abs ∘ 𝑓), ℝ, < ) ∈ ℝ)
1061053ad2antl1 1182 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ sup(ran (abs ∘ 𝑓), ℝ, < ) ∈ ℝ)
10734ffvelcdmda 7079 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ∈ ℝ)
10836, 107sselid 3975 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ∈ β„‚)
109108abscld 15387 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ 𝑖 ∈ 𝑋) β†’ (absβ€˜(π‘“β€˜π‘–)) ∈ ℝ)
110109adantll 711 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖 ∈ 𝑋) β†’ (absβ€˜(π‘“β€˜π‘–)) ∈ ℝ)
1111103ad2antl1 1182 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ (absβ€˜(π‘“β€˜π‘–)) ∈ ℝ)
112107renegcld 11642 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ 𝑖 ∈ 𝑋) β†’ -(π‘“β€˜π‘–) ∈ ℝ)
113112leabsd 15365 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ 𝑖 ∈ 𝑋) β†’ -(π‘“β€˜π‘–) ≀ (absβ€˜-(π‘“β€˜π‘–)))
114108absnegd 15400 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ 𝑖 ∈ 𝑋) β†’ (absβ€˜-(π‘“β€˜π‘–)) = (absβ€˜(π‘“β€˜π‘–)))
115113, 114breqtrd 5167 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ 𝑖 ∈ 𝑋) β†’ -(π‘“β€˜π‘–) ≀ (absβ€˜(π‘“β€˜π‘–)))
116115adantll 711 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖 ∈ 𝑋) β†’ -(π‘“β€˜π‘–) ≀ (absβ€˜(π‘“β€˜π‘–)))
1171163ad2antl1 1182 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ -(π‘“β€˜π‘–) ≀ (absβ€˜(π‘“β€˜π‘–)))
11829a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ ran (abs ∘ 𝑓) βŠ† ℝ)
119104, 64syldan 590 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖 ∈ 𝑋) β†’ ran (abs ∘ 𝑓) β‰  βˆ…)
1201193ad2antl1 1182 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ ran (abs ∘ 𝑓) β‰  βˆ…)
121 fimaxre2 12160 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((ran (abs ∘ 𝑓) βŠ† ℝ ∧ ran (abs ∘ 𝑓) ∈ Fin) β†’ βˆƒπ‘¦ ∈ ℝ βˆ€π‘§ ∈ ran (abs ∘ 𝑓)𝑧 ≀ 𝑦)
12229, 44, 121sylancr 586 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) β†’ βˆƒπ‘¦ ∈ ℝ βˆ€π‘§ ∈ ran (abs ∘ 𝑓)𝑧 ≀ 𝑦)
123122adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖 ∈ 𝑋) β†’ βˆƒπ‘¦ ∈ ℝ βˆ€π‘§ ∈ ran (abs ∘ 𝑓)𝑧 ≀ 𝑦)
1241233ad2antl1 1182 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ βˆƒπ‘¦ ∈ ℝ βˆ€π‘§ ∈ ran (abs ∘ 𝑓)𝑧 ≀ 𝑦)
125 elmapfun 8859 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑓 ∈ (ℝ ↑m 𝑋) β†’ Fun 𝑓)
126125adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ 𝑖 ∈ 𝑋) β†’ Fun 𝑓)
127 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ 𝑖 ∈ 𝑋) β†’ 𝑖 ∈ 𝑋)
12854eqcomd 2732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑓 ∈ (ℝ ↑m 𝑋) β†’ 𝑋 = dom 𝑓)
129128adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ 𝑖 ∈ 𝑋) β†’ 𝑋 = dom 𝑓)
130127, 129eleqtrd 2829 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ 𝑖 ∈ 𝑋) β†’ 𝑖 ∈ dom 𝑓)
131 fvco 6982 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((Fun 𝑓 ∧ 𝑖 ∈ dom 𝑓) β†’ ((abs ∘ 𝑓)β€˜π‘–) = (absβ€˜(π‘“β€˜π‘–)))
132126, 130, 131syl2anc 583 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ 𝑖 ∈ 𝑋) β†’ ((abs ∘ 𝑓)β€˜π‘–) = (absβ€˜(π‘“β€˜π‘–)))
133132eqcomd 2732 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ 𝑖 ∈ 𝑋) β†’ (absβ€˜(π‘“β€˜π‘–)) = ((abs ∘ 𝑓)β€˜π‘–))
134 absfun 44613 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 Fun abs
135134a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑓 ∈ (ℝ ↑m 𝑋) β†’ Fun abs)
136 funco 6581 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((Fun abs ∧ Fun 𝑓) β†’ Fun (abs ∘ 𝑓))
137135, 125, 136syl2anc 583 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑓 ∈ (ℝ ↑m 𝑋) β†’ Fun (abs ∘ 𝑓))
138137adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ 𝑖 ∈ 𝑋) β†’ Fun (abs ∘ 𝑓))
139108, 48eleqtrdi 2837 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ∈ dom abs)
140 dmfco 6980 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((Fun 𝑓 ∧ 𝑖 ∈ dom 𝑓) β†’ (𝑖 ∈ dom (abs ∘ 𝑓) ↔ (π‘“β€˜π‘–) ∈ dom abs))
141126, 130, 140syl2anc 583 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ 𝑖 ∈ 𝑋) β†’ (𝑖 ∈ dom (abs ∘ 𝑓) ↔ (π‘“β€˜π‘–) ∈ dom abs))
142139, 141mpbird 257 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ 𝑖 ∈ 𝑋) β†’ 𝑖 ∈ dom (abs ∘ 𝑓))
143 fvelrn 7071 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((Fun (abs ∘ 𝑓) ∧ 𝑖 ∈ dom (abs ∘ 𝑓)) β†’ ((abs ∘ 𝑓)β€˜π‘–) ∈ ran (abs ∘ 𝑓))
144138, 142, 143syl2anc 583 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ 𝑖 ∈ 𝑋) β†’ ((abs ∘ 𝑓)β€˜π‘–) ∈ ran (abs ∘ 𝑓))
145133, 144eqeltrd 2827 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ 𝑖 ∈ 𝑋) β†’ (absβ€˜(π‘“β€˜π‘–)) ∈ ran (abs ∘ 𝑓))
146145adantll 711 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖 ∈ 𝑋) β†’ (absβ€˜(π‘“β€˜π‘–)) ∈ ran (abs ∘ 𝑓))
1471463ad2antl1 1182 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ (absβ€˜(π‘“β€˜π‘–)) ∈ ran (abs ∘ 𝑓))
148 suprub 12176 . . . . . . . . . . . . . . . . . . . . . . 23 (((ran (abs ∘ 𝑓) βŠ† ℝ ∧ ran (abs ∘ 𝑓) β‰  βˆ… ∧ βˆƒπ‘¦ ∈ ℝ βˆ€π‘§ ∈ ran (abs ∘ 𝑓)𝑧 ≀ 𝑦) ∧ (absβ€˜(π‘“β€˜π‘–)) ∈ ran (abs ∘ 𝑓)) β†’ (absβ€˜(π‘“β€˜π‘–)) ≀ sup(ran (abs ∘ 𝑓), ℝ, < ))
149118, 120, 124, 147, 148syl31anc 1370 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ (absβ€˜(π‘“β€˜π‘–)) ≀ sup(ran (abs ∘ 𝑓), ℝ, < ))
150100, 111, 106, 117, 149letrd 11372 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ -(π‘“β€˜π‘–) ≀ sup(ran (abs ∘ 𝑓), ℝ, < ))
151 simpl3 1190 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗)
152100, 106, 96, 150, 151lelttrd 11373 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ -(π‘“β€˜π‘–) < 𝑗)
153100, 96ltnegd 11793 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ (-(π‘“β€˜π‘–) < 𝑗 ↔ -𝑗 < --(π‘“β€˜π‘–)))
154152, 153mpbid 231 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ -𝑗 < --(π‘“β€˜π‘–))
15536, 99sselid 3975 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ∈ β„‚)
156155negnegd 11563 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ --(π‘“β€˜π‘–) = (π‘“β€˜π‘–))
157154, 156breqtrd 5167 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ -𝑗 < (π‘“β€˜π‘–))
15897, 99, 157ltled 11363 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ -𝑗 ≀ (π‘“β€˜π‘–))
15999leabsd 15365 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ≀ (absβ€˜(π‘“β€˜π‘–)))
16099, 111, 106, 159, 149letrd 11372 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ≀ sup(ran (abs ∘ 𝑓), ℝ, < ))
16199, 106, 96, 160, 151lelttrd 11373 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) < 𝑗)
16285, 88, 93, 158, 161elicod 13377 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ∈ (-𝑗[,)𝑗))
16373, 75, 76, 77, 162syl31anc 1370 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„•) ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ∈ (-𝑗[,)𝑗))
164163adantl3r 747 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) ∧ 𝑗 ∈ β„•) ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ∈ (-𝑗[,)𝑗))
165 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ 𝑗 ∈ β„•)
166 mptexg 7217 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑋 ∈ Fin β†’ (π‘₯ ∈ 𝑋 ↦ ⟨-𝑗, π‘—βŸ©) ∈ V)
16741, 166syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ (π‘₯ ∈ 𝑋 ↦ ⟨-𝑗, π‘—βŸ©) ∈ V)
168167adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (π‘₯ ∈ 𝑋 ↦ ⟨-𝑗, π‘—βŸ©) ∈ V)
169 hoicvr.2 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝐼 = (𝑗 ∈ β„• ↦ (π‘₯ ∈ 𝑋 ↦ ⟨-𝑗, π‘—βŸ©))
170169fvmpt2 7002 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑗 ∈ β„• ∧ (π‘₯ ∈ 𝑋 ↦ ⟨-𝑗, π‘—βŸ©) ∈ V) β†’ (πΌβ€˜π‘—) = (π‘₯ ∈ 𝑋 ↦ ⟨-𝑗, π‘—βŸ©))
171165, 168, 170syl2anc 583 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (πΌβ€˜π‘—) = (π‘₯ ∈ 𝑋 ↦ ⟨-𝑗, π‘—βŸ©))
172171fveq1d 6886 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ ((πΌβ€˜π‘—)β€˜π‘–) = ((π‘₯ ∈ 𝑋 ↦ ⟨-𝑗, π‘—βŸ©)β€˜π‘–))
1731723adant3 1129 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ 𝑖 ∈ 𝑋) β†’ ((πΌβ€˜π‘—)β€˜π‘–) = ((π‘₯ ∈ 𝑋 ↦ ⟨-𝑗, π‘—βŸ©)β€˜π‘–))
174 eqidd 2727 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 ∈ 𝑋 β†’ (π‘₯ ∈ 𝑋 ↦ ⟨-𝑗, π‘—βŸ©) = (π‘₯ ∈ 𝑋 ↦ ⟨-𝑗, π‘—βŸ©))
175 eqid 2726 . . . . . . . . . . . . . . . . . . . . . . . 24 ⟨-𝑗, π‘—βŸ© = ⟨-𝑗, π‘—βŸ©
176175a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑖 ∈ 𝑋 ∧ π‘₯ = 𝑖) β†’ ⟨-𝑗, π‘—βŸ© = ⟨-𝑗, π‘—βŸ©)
177 id 22 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 ∈ 𝑋 β†’ 𝑖 ∈ 𝑋)
178 opex 5457 . . . . . . . . . . . . . . . . . . . . . . . 24 ⟨-𝑗, π‘—βŸ© ∈ V
179178a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 ∈ 𝑋 β†’ ⟨-𝑗, π‘—βŸ© ∈ V)
180174, 176, 177, 179fvmptd 6998 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 ∈ 𝑋 β†’ ((π‘₯ ∈ 𝑋 ↦ ⟨-𝑗, π‘—βŸ©)β€˜π‘–) = ⟨-𝑗, π‘—βŸ©)
1811803ad2ant3 1132 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ 𝑖 ∈ 𝑋) β†’ ((π‘₯ ∈ 𝑋 ↦ ⟨-𝑗, π‘—βŸ©)β€˜π‘–) = ⟨-𝑗, π‘—βŸ©)
182173, 181eqtrd 2766 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ 𝑖 ∈ 𝑋) β†’ ((πΌβ€˜π‘—)β€˜π‘–) = ⟨-𝑗, π‘—βŸ©)
183182fveq2d 6888 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ 𝑖 ∈ 𝑋) β†’ (1st β€˜((πΌβ€˜π‘—)β€˜π‘–)) = (1st β€˜βŸ¨-𝑗, π‘—βŸ©))
184 negex 11459 . . . . . . . . . . . . . . . . . . . . 21 -𝑗 ∈ V
185 vex 3472 . . . . . . . . . . . . . . . . . . . . 21 𝑗 ∈ V
186184, 185op1st 7979 . . . . . . . . . . . . . . . . . . . 20 (1st β€˜βŸ¨-𝑗, π‘—βŸ©) = -𝑗
187186a1i 11 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ 𝑖 ∈ 𝑋) β†’ (1st β€˜βŸ¨-𝑗, π‘—βŸ©) = -𝑗)
188183, 187eqtrd 2766 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ 𝑖 ∈ 𝑋) β†’ (1st β€˜((πΌβ€˜π‘—)β€˜π‘–)) = -𝑗)
189182fveq2d 6888 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ 𝑖 ∈ 𝑋) β†’ (2nd β€˜((πΌβ€˜π‘—)β€˜π‘–)) = (2nd β€˜βŸ¨-𝑗, π‘—βŸ©))
190184, 185op2nd 7980 . . . . . . . . . . . . . . . . . . . 20 (2nd β€˜βŸ¨-𝑗, π‘—βŸ©) = 𝑗
191190a1i 11 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ 𝑖 ∈ 𝑋) β†’ (2nd β€˜βŸ¨-𝑗, π‘—βŸ©) = 𝑗)
192189, 191eqtrd 2766 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ 𝑖 ∈ 𝑋) β†’ (2nd β€˜((πΌβ€˜π‘—)β€˜π‘–)) = 𝑗)
193188, 192oveq12d 7422 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ 𝑖 ∈ 𝑋) β†’ ((1st β€˜((πΌβ€˜π‘—)β€˜π‘–))[,)(2nd β€˜((πΌβ€˜π‘—)β€˜π‘–))) = (-𝑗[,)𝑗))
194193eqcomd 2732 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ 𝑖 ∈ 𝑋) β†’ (-𝑗[,)𝑗) = ((1st β€˜((πΌβ€˜π‘—)β€˜π‘–))[,)(2nd β€˜((πΌβ€˜π‘—)β€˜π‘–))))
1951943adant1r 1174 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ 𝑖 ∈ 𝑋) β†’ (-𝑗[,)𝑗) = ((1st β€˜((πΌβ€˜π‘—)β€˜π‘–))[,)(2nd β€˜((πΌβ€˜π‘—)β€˜π‘–))))
196195ad5ant135 1365 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) ∧ 𝑗 ∈ β„•) ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ (-𝑗[,)𝑗) = ((1st β€˜((πΌβ€˜π‘—)β€˜π‘–))[,)(2nd β€˜((πΌβ€˜π‘—)β€˜π‘–))))
197164, 196eleqtrd 2829 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) ∧ 𝑗 ∈ β„•) ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ∈ ((1st β€˜((πΌβ€˜π‘—)β€˜π‘–))[,)(2nd β€˜((πΌβ€˜π‘—)β€˜π‘–))))
19879, 82sselid 3975 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ β„• β†’ -𝑗 ∈ ℝ)
199 opelxpi 5706 . . . . . . . . . . . . . . . . . . . . 21 ((-𝑗 ∈ ℝ ∧ 𝑗 ∈ ℝ) β†’ ⟨-𝑗, π‘—βŸ© ∈ (ℝ Γ— ℝ))
200198, 94, 199syl2anc 583 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ β„• β†’ ⟨-𝑗, π‘—βŸ© ∈ (ℝ Γ— ℝ))
201200ad2antlr 724 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑗 ∈ β„•) ∧ π‘₯ ∈ 𝑋) β†’ ⟨-𝑗, π‘—βŸ© ∈ (ℝ Γ— ℝ))
202 eqid 2726 . . . . . . . . . . . . . . . . . . 19 (π‘₯ ∈ 𝑋 ↦ ⟨-𝑗, π‘—βŸ©) = (π‘₯ ∈ 𝑋 ↦ ⟨-𝑗, π‘—βŸ©)
203201, 202fmptd 7108 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (π‘₯ ∈ 𝑋 ↦ ⟨-𝑗, π‘—βŸ©):π‘‹βŸΆ(ℝ Γ— ℝ))
204171feq1d 6695 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ ((πΌβ€˜π‘—):π‘‹βŸΆ(ℝ Γ— ℝ) ↔ (π‘₯ ∈ 𝑋 ↦ ⟨-𝑗, π‘—βŸ©):π‘‹βŸΆ(ℝ Γ— ℝ)))
205203, 204mpbird 257 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (πΌβ€˜π‘—):π‘‹βŸΆ(ℝ Γ— ℝ))
206205ad4ant14 749 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) ∧ 𝑗 ∈ β„•) β†’ (πΌβ€˜π‘—):π‘‹βŸΆ(ℝ Γ— ℝ))
207206ad2antrr 723 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) ∧ 𝑗 ∈ β„•) ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ (πΌβ€˜π‘—):π‘‹βŸΆ(ℝ Γ— ℝ))
208 simpr 484 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) ∧ 𝑗 ∈ β„•) ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ 𝑖 ∈ 𝑋)
209207, 208fvovco 44445 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) ∧ 𝑗 ∈ β„•) ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–) = ((1st β€˜((πΌβ€˜π‘—)β€˜π‘–))[,)(2nd β€˜((πΌβ€˜π‘—)β€˜π‘–))))
210209eqcomd 2732 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) ∧ 𝑗 ∈ β„•) ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ ((1st β€˜((πΌβ€˜π‘—)β€˜π‘–))[,)(2nd β€˜((πΌβ€˜π‘—)β€˜π‘–))) = (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–))
211197, 210eleqtrd 2829 . . . . . . . . . . . 12 ((((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) ∧ 𝑗 ∈ β„•) ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ∈ (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–))
212211ralrimiva 3140 . . . . . . . . . . 11 (((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) ∧ 𝑗 ∈ β„•) ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) β†’ βˆ€π‘– ∈ 𝑋 (π‘“β€˜π‘–) ∈ (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–))
21372, 212jca 511 . . . . . . . . . 10 (((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) ∧ 𝑗 ∈ β„•) ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) β†’ (𝑓 Fn 𝑋 ∧ βˆ€π‘– ∈ 𝑋 (π‘“β€˜π‘–) ∈ (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–)))
214 vex 3472 . . . . . . . . . . 11 𝑓 ∈ V
215214elixp 8897 . . . . . . . . . 10 (𝑓 ∈ X𝑖 ∈ 𝑋 (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–) ↔ (𝑓 Fn 𝑋 ∧ βˆ€π‘– ∈ 𝑋 (π‘“β€˜π‘–) ∈ (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–)))
216213, 215sylibr 233 . . . . . . . . 9 (((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) ∧ 𝑗 ∈ β„•) ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) β†’ 𝑓 ∈ X𝑖 ∈ 𝑋 (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–))
217216ex 412 . . . . . . . 8 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) ∧ 𝑗 ∈ β„•) β†’ (sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗 β†’ 𝑓 ∈ X𝑖 ∈ 𝑋 (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–)))
218217reximdva 3162 . . . . . . 7 (((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) β†’ (βˆƒπ‘— ∈ β„• sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗 β†’ βˆƒπ‘— ∈ β„• 𝑓 ∈ X𝑖 ∈ 𝑋 (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–)))
21969, 218mpd 15 . . . . . 6 (((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) β†’ βˆƒπ‘— ∈ β„• 𝑓 ∈ X𝑖 ∈ 𝑋 (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–))
22022, 23, 24, 219syl21anc 835 . . . . 5 (((πœ‘ ∧ Β¬ 𝑋 = βˆ…) ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) β†’ βˆƒπ‘— ∈ β„• 𝑓 ∈ X𝑖 ∈ 𝑋 (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–))
221 eliun 4994 . . . . 5 (𝑓 ∈ βˆͺ 𝑗 ∈ β„• X𝑖 ∈ 𝑋 (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–) ↔ βˆƒπ‘— ∈ β„• 𝑓 ∈ X𝑖 ∈ 𝑋 (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–))
222220, 221sylibr 233 . . . 4 (((πœ‘ ∧ Β¬ 𝑋 = βˆ…) ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) β†’ 𝑓 ∈ βˆͺ 𝑗 ∈ β„• X𝑖 ∈ 𝑋 (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–))
223222ralrimiva 3140 . . 3 ((πœ‘ ∧ Β¬ 𝑋 = βˆ…) β†’ βˆ€π‘“ ∈ (ℝ ↑m 𝑋)𝑓 ∈ βˆͺ 𝑗 ∈ β„• X𝑖 ∈ 𝑋 (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–))
224 dfss3 3965 . . 3 ((ℝ ↑m 𝑋) βŠ† βˆͺ 𝑗 ∈ β„• X𝑖 ∈ 𝑋 (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–) ↔ βˆ€π‘“ ∈ (ℝ ↑m 𝑋)𝑓 ∈ βˆͺ 𝑗 ∈ β„• X𝑖 ∈ 𝑋 (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–))
225223, 224sylibr 233 . 2 ((πœ‘ ∧ Β¬ 𝑋 = βˆ…) β†’ (ℝ ↑m 𝑋) βŠ† βˆͺ 𝑗 ∈ β„• X𝑖 ∈ 𝑋 (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–))
22621, 225pm2.61dan 810 1 (πœ‘ β†’ (ℝ ↑m 𝑋) βŠ† βˆͺ 𝑗 ∈ β„• X𝑖 ∈ 𝑋 (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098   β‰  wne 2934  βˆ€wral 3055  βˆƒwrex 3064  Vcvv 3468   βŠ† wss 3943  βˆ…c0 4317  {csn 4623  βŸ¨cop 4629  βˆͺ ciun 4990   class class class wbr 5141   ↦ cmpt 5224   Or wor 5580   Γ— cxp 5667  dom cdm 5669  ran crn 5670   ∘ ccom 5673  Fun wfun 6530   Fn wfn 6531  βŸΆwf 6532  β€˜cfv 6536  (class class class)co 7404  1st c1st 7969  2nd c2nd 7970   ↑m cmap 8819  Xcixp 8890  Fincfn 8938  supcsup 9434  β„‚cc 11107  β„cr 11108  1c1 11110  β„*cxr 11248   < clt 11249   ≀ cle 11250  -cneg 11446  β„•cn 12213  β„€cz 12559  [,)cico 13329  abscabs 15185
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2697  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7721  ax-cnex 11165  ax-resscn 11166  ax-1cn 11167  ax-icn 11168  ax-addcl 11169  ax-addrcl 11170  ax-mulcl 11171  ax-mulrcl 11172  ax-mulcom 11173  ax-addass 11174  ax-mulass 11175  ax-distr 11176  ax-i2m1 11177  ax-1ne0 11178  ax-1rid 11179  ax-rnegex 11180  ax-rrecex 11181  ax-cnre 11182  ax-pre-lttri 11183  ax-pre-lttrn 11184  ax-pre-ltadd 11185  ax-pre-mulgt0 11186  ax-pre-sup 11187
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-nel 3041  df-ral 3056  df-rex 3065  df-rmo 3370  df-reu 3371  df-rab 3427  df-v 3470  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-pss 3962  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-pred 6293  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6488  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7360  df-ov 7407  df-oprab 7408  df-mpo 7409  df-om 7852  df-1st 7971  df-2nd 7972  df-frecs 8264  df-wrecs 8295  df-recs 8369  df-rdg 8408  df-1o 8464  df-er 8702  df-map 8821  df-ixp 8891  df-en 8939  df-dom 8940  df-sdom 8941  df-fin 8942  df-sup 9436  df-pnf 11251  df-mnf 11252  df-xr 11253  df-ltxr 11254  df-le 11255  df-sub 11447  df-neg 11448  df-div 11873  df-nn 12214  df-2 12276  df-3 12277  df-n0 12474  df-z 12560  df-uz 12824  df-rp 12978  df-ico 13333  df-seq 13970  df-exp 14031  df-cj 15050  df-re 15051  df-im 15052  df-sqrt 15186  df-abs 15187
This theorem is referenced by:  hoicvrrex  45825
  Copyright terms: Public domain W3C validator