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 45938
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 11235 . . . . . . 7 ℝ ∈ V
2 mapdm0 8865 . . . . . . 7 (ℝ ∈ V β†’ (ℝ ↑m βˆ…) = {βˆ…})
31, 2ax-mp 5 . . . . . 6 (ℝ ↑m βˆ…) = {βˆ…}
43a1i 11 . . . . 5 (𝑋 = βˆ… β†’ (ℝ ↑m βˆ…) = {βˆ…})
5 oveq2 7432 . . . . 5 (𝑋 = βˆ… β†’ (ℝ ↑m 𝑋) = (ℝ ↑m βˆ…))
6 ixpeq1 8931 . . . . . . 7 (𝑋 = βˆ… β†’ X𝑖 ∈ 𝑋 (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–) = X𝑖 ∈ βˆ… (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–))
76iuneq2d 5027 . . . . . 6 (𝑋 = βˆ… β†’ βˆͺ 𝑗 ∈ β„• X𝑖 ∈ 𝑋 (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–) = βˆͺ 𝑗 ∈ β„• X𝑖 ∈ βˆ… (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–))
8 ixp0x 8949 . . . . . . . . . 10 X𝑖 ∈ βˆ… (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–) = {βˆ…}
98a1i 11 . . . . . . . . 9 (𝑗 ∈ β„• β†’ X𝑖 ∈ βˆ… (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–) = {βˆ…})
109iuneq2i 5019 . . . . . . . 8 βˆͺ 𝑗 ∈ β„• X𝑖 ∈ βˆ… (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–) = βˆͺ 𝑗 ∈ β„• {βˆ…}
11 1nn 12259 . . . . . . . . . 10 1 ∈ β„•
1211ne0ii 4339 . . . . . . . . 9 β„• β‰  βˆ…
13 iunconst 5007 . . . . . . . . 9 (β„• β‰  βˆ… β†’ βˆͺ 𝑗 ∈ β„• {βˆ…} = {βˆ…})
1412, 13ax-mp 5 . . . . . . . 8 βˆͺ 𝑗 ∈ β„• {βˆ…} = {βˆ…}
1510, 14eqtri 2755 . . . . . . 7 βˆͺ 𝑗 ∈ β„• X𝑖 ∈ βˆ… (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–) = {βˆ…}
1615a1i 11 . . . . . 6 (𝑋 = βˆ… β†’ βˆͺ 𝑗 ∈ β„• X𝑖 ∈ βˆ… (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–) = {βˆ…})
177, 16eqtrd 2767 . . . . 5 (𝑋 = βˆ… β†’ βˆͺ 𝑗 ∈ β„• X𝑖 ∈ 𝑋 (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–) = {βˆ…})
184, 5, 173eqtr4d 2777 . . . 4 (𝑋 = βˆ… β†’ (ℝ ↑m 𝑋) = βˆͺ 𝑗 ∈ β„• X𝑖 ∈ 𝑋 (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–))
19 eqimss 4038 . . . 4 ((ℝ ↑m 𝑋) = βˆͺ 𝑗 ∈ β„• X𝑖 ∈ 𝑋 (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–) β†’ (ℝ ↑m 𝑋) βŠ† βˆͺ 𝑗 ∈ β„• X𝑖 ∈ 𝑋 (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–))
2018, 19syl 17 . . 3 (𝑋 = βˆ… β†’ (ℝ ↑m 𝑋) βŠ† βˆͺ 𝑗 ∈ β„• X𝑖 ∈ 𝑋 (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–))
2120adantl 480 . 2 ((πœ‘ ∧ 𝑋 = βˆ…) β†’ (ℝ ↑m 𝑋) βŠ† βˆͺ 𝑗 ∈ β„• X𝑖 ∈ 𝑋 (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–))
22 simpll 765 . . . . . 6 (((πœ‘ ∧ Β¬ 𝑋 = βˆ…) ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) β†’ πœ‘)
23 simpr 483 . . . . . 6 (((πœ‘ ∧ Β¬ 𝑋 = βˆ…) ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) β†’ 𝑓 ∈ (ℝ ↑m 𝑋))
24 simplr 767 . . . . . 6 (((πœ‘ ∧ Β¬ 𝑋 = βˆ…) ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) β†’ Β¬ 𝑋 = βˆ…)
25 rncoss 5977 . . . . . . . . . . 11 ran (abs ∘ 𝑓) βŠ† ran abs
26 absf 15322 . . . . . . . . . . . 12 abs:β„‚βŸΆβ„
27 frn 6732 . . . . . . . . . . . 12 (abs:β„‚βŸΆβ„ β†’ ran abs βŠ† ℝ)
2826, 27ax-mp 5 . . . . . . . . . . 11 ran abs βŠ† ℝ
2925, 28sstri 3989 . . . . . . . . . 10 ran (abs ∘ 𝑓) βŠ† ℝ
3029a1i 11 . . . . . . . . 9 (((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) β†’ ran (abs ∘ 𝑓) βŠ† ℝ)
31 ltso 11330 . . . . . . . . . . 11 < Or ℝ
3231a1i 11 . . . . . . . . . 10 (((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) β†’ < Or ℝ)
3326a1i 11 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) β†’ abs:β„‚βŸΆβ„)
34 elmapi 8872 . . . . . . . . . . . . . . 15 (𝑓 ∈ (ℝ ↑m 𝑋) β†’ 𝑓:π‘‹βŸΆβ„)
3534adantl 480 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) β†’ 𝑓:π‘‹βŸΆβ„)
36 ax-resscn 11201 . . . . . . . . . . . . . . 15 ℝ βŠ† β„‚
3736a1i 11 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) β†’ ℝ βŠ† β„‚)
3835, 37fssd 6743 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) β†’ 𝑓:π‘‹βŸΆβ„‚)
39 fco 6750 . . . . . . . . . . . . 13 ((abs:β„‚βŸΆβ„ ∧ 𝑓:π‘‹βŸΆβ„‚) β†’ (abs ∘ 𝑓):π‘‹βŸΆβ„)
4033, 38, 39syl2anc 582 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) β†’ (abs ∘ 𝑓):π‘‹βŸΆβ„)
41 hoicvr.3 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑋 ∈ Fin)
4241adantr 479 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) β†’ 𝑋 ∈ Fin)
43 rnffi 44551 . . . . . . . . . . . 12 (((abs ∘ 𝑓):π‘‹βŸΆβ„ ∧ 𝑋 ∈ Fin) β†’ ran (abs ∘ 𝑓) ∈ Fin)
4440, 42, 43syl2anc 582 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) β†’ ran (abs ∘ 𝑓) ∈ Fin)
4544adantr 479 . . . . . . . . . 10 (((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) β†’ ran (abs ∘ 𝑓) ∈ Fin)
4634frnd 6733 . . . . . . . . . . . . . . . . . . 19 (𝑓 ∈ (ℝ ↑m 𝑋) β†’ ran 𝑓 βŠ† ℝ)
4726fdmi 6737 . . . . . . . . . . . . . . . . . . . . . 22 dom abs = β„‚
4847eqcomi 2736 . . . . . . . . . . . . . . . . . . . . 21 β„‚ = dom abs
4936, 48sseqtri 4016 . . . . . . . . . . . . . . . . . . . 20 ℝ βŠ† dom abs
5049a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝑓 ∈ (ℝ ↑m 𝑋) β†’ ℝ βŠ† dom abs)
5146, 50sstrd 3990 . . . . . . . . . . . . . . . . . 18 (𝑓 ∈ (ℝ ↑m 𝑋) β†’ ran 𝑓 βŠ† dom abs)
52 dmcosseq 5978 . . . . . . . . . . . . . . . . . 18 (ran 𝑓 βŠ† dom abs β†’ dom (abs ∘ 𝑓) = dom 𝑓)
5351, 52syl 17 . . . . . . . . . . . . . . . . 17 (𝑓 ∈ (ℝ ↑m 𝑋) β†’ dom (abs ∘ 𝑓) = dom 𝑓)
5434fdmd 6736 . . . . . . . . . . . . . . . . 17 (𝑓 ∈ (ℝ ↑m 𝑋) β†’ dom 𝑓 = 𝑋)
5553, 54eqtrd 2767 . . . . . . . . . . . . . . . 16 (𝑓 ∈ (ℝ ↑m 𝑋) β†’ dom (abs ∘ 𝑓) = 𝑋)
5655adantr 479 . . . . . . . . . . . . . . 15 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ Β¬ 𝑋 = βˆ…) β†’ dom (abs ∘ 𝑓) = 𝑋)
57 neqne 2944 . . . . . . . . . . . . . . . 16 (Β¬ 𝑋 = βˆ… β†’ 𝑋 β‰  βˆ…)
5857adantl 480 . . . . . . . . . . . . . . 15 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ Β¬ 𝑋 = βˆ…) β†’ 𝑋 β‰  βˆ…)
5956, 58eqnetrd 3004 . . . . . . . . . . . . . 14 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ Β¬ 𝑋 = βˆ…) β†’ dom (abs ∘ 𝑓) β‰  βˆ…)
6059neneqd 2941 . . . . . . . . . . . . 13 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ Β¬ 𝑋 = βˆ…) β†’ Β¬ dom (abs ∘ 𝑓) = βˆ…)
61 dm0rn0 5929 . . . . . . . . . . . . 13 (dom (abs ∘ 𝑓) = βˆ… ↔ ran (abs ∘ 𝑓) = βˆ…)
6260, 61sylnib 327 . . . . . . . . . . . 12 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ Β¬ 𝑋 = βˆ…) β†’ Β¬ ran (abs ∘ 𝑓) = βˆ…)
6362neqned 2943 . . . . . . . . . . 11 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ Β¬ 𝑋 = βˆ…) β†’ ran (abs ∘ 𝑓) β‰  βˆ…)
6463adantll 712 . . . . . . . . . 10 (((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) β†’ ran (abs ∘ 𝑓) β‰  βˆ…)
65 fisupcl 9498 . . . . . . . . . 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 3981 . . . . . . . 8 (((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) β†’ sup(ran (abs ∘ 𝑓), ℝ, < ) ∈ ℝ)
68 arch 12505 . . . . . . . 8 (sup(ran (abs ∘ 𝑓), ℝ, < ) ∈ ℝ β†’ βˆƒπ‘— ∈ β„• sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗)
6967, 68syl 17 . . . . . . 7 (((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) β†’ βˆƒπ‘— ∈ β„• sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗)
7035ffnd 6726 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) β†’ 𝑓 Fn 𝑋)
7170ad2antrr 724 . . . . . . . . . . . 12 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) β†’ 𝑓 Fn 𝑋)
7271adantlr 713 . . . . . . . . . . 11 (((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) ∧ 𝑗 ∈ β„•) ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) β†’ 𝑓 Fn 𝑋)
73 simplll 773 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„•) ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ (πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)))
74 id 22 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ β„• β†’ 𝑗 ∈ β„•)
7574ad3antlr 729 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„•) ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ 𝑗 ∈ β„•)
76 simplr 767 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„•) ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗)
77 simpr 483 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„•) ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ 𝑖 ∈ 𝑋)
78 simp2 1134 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) β†’ 𝑗 ∈ β„•)
79 zssre 12601 . . . . . . . . . . . . . . . . . . . . 21 β„€ βŠ† ℝ
80 ressxr 11294 . . . . . . . . . . . . . . . . . . . . 21 ℝ βŠ† ℝ*
8179, 80sstri 3989 . . . . . . . . . . . . . . . . . . . 20 β„€ βŠ† ℝ*
82 nnnegz 12597 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ β„• β†’ -𝑗 ∈ β„€)
8381, 82sselid 3978 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ β„• β†’ -𝑗 ∈ ℝ*)
8483adantr 479 . . . . . . . . . . . . . . . . . 18 ((𝑗 ∈ β„• ∧ 𝑖 ∈ 𝑋) β†’ -𝑗 ∈ ℝ*)
8578, 84sylan 578 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ -𝑗 ∈ ℝ*)
8674nnxrd 44657 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ β„• β†’ 𝑗 ∈ ℝ*)
8786adantr 479 . . . . . . . . . . . . . . . . . 18 ((𝑗 ∈ β„• ∧ 𝑖 ∈ 𝑋) β†’ 𝑗 ∈ ℝ*)
8878, 87sylan 578 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ 𝑗 ∈ ℝ*)
89343ad2ant1 1130 . . . . . . . . . . . . . . . . . . . 20 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) β†’ 𝑓:π‘‹βŸΆβ„)
9080a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) β†’ ℝ βŠ† ℝ*)
9189, 90fssd 6743 . . . . . . . . . . . . . . . . . . 19 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) β†’ 𝑓:π‘‹βŸΆβ„*)
92913adant1l 1173 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) β†’ 𝑓:π‘‹βŸΆβ„*)
9392ffvelcdmda 7097 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ∈ ℝ*)
94 nnre 12255 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ β„• β†’ 𝑗 ∈ ℝ)
9594adantr 479 . . . . . . . . . . . . . . . . . . . 20 ((𝑗 ∈ β„• ∧ 𝑖 ∈ 𝑋) β†’ 𝑗 ∈ ℝ)
96953ad2antl2 1183 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ 𝑗 ∈ ℝ)
9796renegcld 11677 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ -𝑗 ∈ ℝ)
9835ffvelcdmda 7097 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ∈ ℝ)
99983ad2antl1 1182 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ∈ ℝ)
10099renegcld 11677 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ -(π‘“β€˜π‘–) ∈ ℝ)
101 simpll 765 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖 ∈ 𝑋) β†’ πœ‘)
102 simplr 767 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖 ∈ 𝑋) β†’ 𝑓 ∈ (ℝ ↑m 𝑋))
103 n0i 4335 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑖 ∈ 𝑋 β†’ Β¬ 𝑋 = βˆ…)
104103adantl 480 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖 ∈ 𝑋) β†’ Β¬ 𝑋 = βˆ…)
105101, 102, 104, 67syl21anc 836 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖 ∈ 𝑋) β†’ sup(ran (abs ∘ 𝑓), ℝ, < ) ∈ ℝ)
1061053ad2antl1 1182 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ sup(ran (abs ∘ 𝑓), ℝ, < ) ∈ ℝ)
10734ffvelcdmda 7097 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ∈ ℝ)
10836, 107sselid 3978 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ∈ β„‚)
109108abscld 15421 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ 𝑖 ∈ 𝑋) β†’ (absβ€˜(π‘“β€˜π‘–)) ∈ ℝ)
110109adantll 712 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖 ∈ 𝑋) β†’ (absβ€˜(π‘“β€˜π‘–)) ∈ ℝ)
1111103ad2antl1 1182 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ (absβ€˜(π‘“β€˜π‘–)) ∈ ℝ)
112107renegcld 11677 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ 𝑖 ∈ 𝑋) β†’ -(π‘“β€˜π‘–) ∈ ℝ)
113112leabsd 15399 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ 𝑖 ∈ 𝑋) β†’ -(π‘“β€˜π‘–) ≀ (absβ€˜-(π‘“β€˜π‘–)))
114108absnegd 15434 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ 𝑖 ∈ 𝑋) β†’ (absβ€˜-(π‘“β€˜π‘–)) = (absβ€˜(π‘“β€˜π‘–)))
115113, 114breqtrd 5176 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ 𝑖 ∈ 𝑋) β†’ -(π‘“β€˜π‘–) ≀ (absβ€˜(π‘“β€˜π‘–)))
116115adantll 712 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖 ∈ 𝑋) β†’ -(π‘“β€˜π‘–) ≀ (absβ€˜(π‘“β€˜π‘–)))
1171163ad2antl1 1182 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ -(π‘“β€˜π‘–) ≀ (absβ€˜(π‘“β€˜π‘–)))
11829a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ ran (abs ∘ 𝑓) βŠ† ℝ)
119104, 64syldan 589 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖 ∈ 𝑋) β†’ ran (abs ∘ 𝑓) β‰  βˆ…)
1201193ad2antl1 1182 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ ran (abs ∘ 𝑓) β‰  βˆ…)
121 fimaxre2 12195 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((ran (abs ∘ 𝑓) βŠ† ℝ ∧ ran (abs ∘ 𝑓) ∈ Fin) β†’ βˆƒπ‘¦ ∈ ℝ βˆ€π‘§ ∈ ran (abs ∘ 𝑓)𝑧 ≀ 𝑦)
12229, 44, 121sylancr 585 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) β†’ βˆƒπ‘¦ ∈ ℝ βˆ€π‘§ ∈ ran (abs ∘ 𝑓)𝑧 ≀ 𝑦)
123122adantr 479 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖 ∈ 𝑋) β†’ βˆƒπ‘¦ ∈ ℝ βˆ€π‘§ ∈ ran (abs ∘ 𝑓)𝑧 ≀ 𝑦)
1241233ad2antl1 1182 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ βˆƒπ‘¦ ∈ ℝ βˆ€π‘§ ∈ ran (abs ∘ 𝑓)𝑧 ≀ 𝑦)
125 elmapfun 8889 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑓 ∈ (ℝ ↑m 𝑋) β†’ Fun 𝑓)
126125adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ 𝑖 ∈ 𝑋) β†’ Fun 𝑓)
127 simpr 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ 𝑖 ∈ 𝑋) β†’ 𝑖 ∈ 𝑋)
12854eqcomd 2733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑓 ∈ (ℝ ↑m 𝑋) β†’ 𝑋 = dom 𝑓)
129128adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ 𝑖 ∈ 𝑋) β†’ 𝑋 = dom 𝑓)
130127, 129eleqtrd 2830 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ 𝑖 ∈ 𝑋) β†’ 𝑖 ∈ dom 𝑓)
131 fvco 6999 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((Fun 𝑓 ∧ 𝑖 ∈ dom 𝑓) β†’ ((abs ∘ 𝑓)β€˜π‘–) = (absβ€˜(π‘“β€˜π‘–)))
132126, 130, 131syl2anc 582 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ 𝑖 ∈ 𝑋) β†’ ((abs ∘ 𝑓)β€˜π‘–) = (absβ€˜(π‘“β€˜π‘–)))
133132eqcomd 2733 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ 𝑖 ∈ 𝑋) β†’ (absβ€˜(π‘“β€˜π‘–)) = ((abs ∘ 𝑓)β€˜π‘–))
134 absfun 44734 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 Fun abs
135134a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑓 ∈ (ℝ ↑m 𝑋) β†’ Fun abs)
136 funco 6596 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((Fun abs ∧ Fun 𝑓) β†’ Fun (abs ∘ 𝑓))
137135, 125, 136syl2anc 582 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑓 ∈ (ℝ ↑m 𝑋) β†’ Fun (abs ∘ 𝑓))
138137adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ 𝑖 ∈ 𝑋) β†’ Fun (abs ∘ 𝑓))
139108, 48eleqtrdi 2838 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ∈ dom abs)
140 dmfco 6997 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((Fun 𝑓 ∧ 𝑖 ∈ dom 𝑓) β†’ (𝑖 ∈ dom (abs ∘ 𝑓) ↔ (π‘“β€˜π‘–) ∈ dom abs))
141126, 130, 140syl2anc 582 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ 𝑖 ∈ 𝑋) β†’ (𝑖 ∈ dom (abs ∘ 𝑓) ↔ (π‘“β€˜π‘–) ∈ dom abs))
142139, 141mpbird 256 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ 𝑖 ∈ 𝑋) β†’ 𝑖 ∈ dom (abs ∘ 𝑓))
143 fvelrn 7089 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((Fun (abs ∘ 𝑓) ∧ 𝑖 ∈ dom (abs ∘ 𝑓)) β†’ ((abs ∘ 𝑓)β€˜π‘–) ∈ ran (abs ∘ 𝑓))
144138, 142, 143syl2anc 582 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ 𝑖 ∈ 𝑋) β†’ ((abs ∘ 𝑓)β€˜π‘–) ∈ ran (abs ∘ 𝑓))
145133, 144eqeltrd 2828 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ 𝑖 ∈ 𝑋) β†’ (absβ€˜(π‘“β€˜π‘–)) ∈ ran (abs ∘ 𝑓))
146145adantll 712 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖 ∈ 𝑋) β†’ (absβ€˜(π‘“β€˜π‘–)) ∈ ran (abs ∘ 𝑓))
1471463ad2antl1 1182 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ (absβ€˜(π‘“β€˜π‘–)) ∈ ran (abs ∘ 𝑓))
148 suprub 12211 . . . . . . . . . . . . . . . . . . . . . . 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 11407 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ -(π‘“β€˜π‘–) ≀ sup(ran (abs ∘ 𝑓), ℝ, < ))
151 simpl3 1190 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗)
152100, 106, 96, 150, 151lelttrd 11408 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ -(π‘“β€˜π‘–) < 𝑗)
153100, 96ltnegd 11828 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ (-(π‘“β€˜π‘–) < 𝑗 ↔ -𝑗 < --(π‘“β€˜π‘–)))
154152, 153mpbid 231 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ -𝑗 < --(π‘“β€˜π‘–))
15536, 99sselid 3978 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ∈ β„‚)
156155negnegd 11598 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ --(π‘“β€˜π‘–) = (π‘“β€˜π‘–))
157154, 156breqtrd 5176 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ -𝑗 < (π‘“β€˜π‘–))
15897, 99, 157ltled 11398 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ -𝑗 ≀ (π‘“β€˜π‘–))
15999leabsd 15399 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ≀ (absβ€˜(π‘“β€˜π‘–)))
16099, 111, 106, 159, 149letrd 11407 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ≀ sup(ran (abs ∘ 𝑓), ℝ, < ))
16199, 106, 96, 160, 151lelttrd 11408 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) < 𝑗)
16285, 88, 93, 158, 161elicod 13412 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ∈ (-𝑗[,)𝑗))
16373, 75, 76, 77, 162syl31anc 1370 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„•) ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ∈ (-𝑗[,)𝑗))
164163adantl3r 748 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) ∧ 𝑗 ∈ β„•) ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ∈ (-𝑗[,)𝑗))
165 simpr 483 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ 𝑗 ∈ β„•)
166 mptexg 7237 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑋 ∈ Fin β†’ (π‘₯ ∈ 𝑋 ↦ ⟨-𝑗, π‘—βŸ©) ∈ V)
16741, 166syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ (π‘₯ ∈ 𝑋 ↦ ⟨-𝑗, π‘—βŸ©) ∈ V)
168167adantr 479 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (π‘₯ ∈ 𝑋 ↦ ⟨-𝑗, π‘—βŸ©) ∈ V)
169 hoicvr.2 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝐼 = (𝑗 ∈ β„• ↦ (π‘₯ ∈ 𝑋 ↦ ⟨-𝑗, π‘—βŸ©))
170169fvmpt2 7019 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑗 ∈ β„• ∧ (π‘₯ ∈ 𝑋 ↦ ⟨-𝑗, π‘—βŸ©) ∈ V) β†’ (πΌβ€˜π‘—) = (π‘₯ ∈ 𝑋 ↦ ⟨-𝑗, π‘—βŸ©))
171165, 168, 170syl2anc 582 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (πΌβ€˜π‘—) = (π‘₯ ∈ 𝑋 ↦ ⟨-𝑗, π‘—βŸ©))
172171fveq1d 6902 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ ((πΌβ€˜π‘—)β€˜π‘–) = ((π‘₯ ∈ 𝑋 ↦ ⟨-𝑗, π‘—βŸ©)β€˜π‘–))
1731723adant3 1129 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ 𝑖 ∈ 𝑋) β†’ ((πΌβ€˜π‘—)β€˜π‘–) = ((π‘₯ ∈ 𝑋 ↦ ⟨-𝑗, π‘—βŸ©)β€˜π‘–))
174 eqidd 2728 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 ∈ 𝑋 β†’ (π‘₯ ∈ 𝑋 ↦ ⟨-𝑗, π‘—βŸ©) = (π‘₯ ∈ 𝑋 ↦ ⟨-𝑗, π‘—βŸ©))
175 eqid 2727 . . . . . . . . . . . . . . . . . . . . . . . 24 ⟨-𝑗, π‘—βŸ© = ⟨-𝑗, π‘—βŸ©
176175a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑖 ∈ 𝑋 ∧ π‘₯ = 𝑖) β†’ ⟨-𝑗, π‘—βŸ© = ⟨-𝑗, π‘—βŸ©)
177 id 22 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 ∈ 𝑋 β†’ 𝑖 ∈ 𝑋)
178 opex 5468 . . . . . . . . . . . . . . . . . . . . . . . 24 ⟨-𝑗, π‘—βŸ© ∈ V
179178a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 ∈ 𝑋 β†’ ⟨-𝑗, π‘—βŸ© ∈ V)
180174, 176, 177, 179fvmptd 7015 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 ∈ 𝑋 β†’ ((π‘₯ ∈ 𝑋 ↦ ⟨-𝑗, π‘—βŸ©)β€˜π‘–) = ⟨-𝑗, π‘—βŸ©)
1811803ad2ant3 1132 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ 𝑖 ∈ 𝑋) β†’ ((π‘₯ ∈ 𝑋 ↦ ⟨-𝑗, π‘—βŸ©)β€˜π‘–) = ⟨-𝑗, π‘—βŸ©)
182173, 181eqtrd 2767 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ 𝑖 ∈ 𝑋) β†’ ((πΌβ€˜π‘—)β€˜π‘–) = ⟨-𝑗, π‘—βŸ©)
183182fveq2d 6904 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ 𝑖 ∈ 𝑋) β†’ (1st β€˜((πΌβ€˜π‘—)β€˜π‘–)) = (1st β€˜βŸ¨-𝑗, π‘—βŸ©))
184 negex 11494 . . . . . . . . . . . . . . . . . . . . 21 -𝑗 ∈ V
185 vex 3475 . . . . . . . . . . . . . . . . . . . . 21 𝑗 ∈ V
186184, 185op1st 8005 . . . . . . . . . . . . . . . . . . . 20 (1st β€˜βŸ¨-𝑗, π‘—βŸ©) = -𝑗
187186a1i 11 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ 𝑖 ∈ 𝑋) β†’ (1st β€˜βŸ¨-𝑗, π‘—βŸ©) = -𝑗)
188183, 187eqtrd 2767 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ 𝑖 ∈ 𝑋) β†’ (1st β€˜((πΌβ€˜π‘—)β€˜π‘–)) = -𝑗)
189182fveq2d 6904 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ 𝑖 ∈ 𝑋) β†’ (2nd β€˜((πΌβ€˜π‘—)β€˜π‘–)) = (2nd β€˜βŸ¨-𝑗, π‘—βŸ©))
190184, 185op2nd 8006 . . . . . . . . . . . . . . . . . . . 20 (2nd β€˜βŸ¨-𝑗, π‘—βŸ©) = 𝑗
191190a1i 11 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ 𝑖 ∈ 𝑋) β†’ (2nd β€˜βŸ¨-𝑗, π‘—βŸ©) = 𝑗)
192189, 191eqtrd 2767 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ 𝑖 ∈ 𝑋) β†’ (2nd β€˜((πΌβ€˜π‘—)β€˜π‘–)) = 𝑗)
193188, 192oveq12d 7442 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ 𝑖 ∈ 𝑋) β†’ ((1st β€˜((πΌβ€˜π‘—)β€˜π‘–))[,)(2nd β€˜((πΌβ€˜π‘—)β€˜π‘–))) = (-𝑗[,)𝑗))
194193eqcomd 2733 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ 𝑖 ∈ 𝑋) β†’ (-𝑗[,)𝑗) = ((1st β€˜((πΌβ€˜π‘—)β€˜π‘–))[,)(2nd β€˜((πΌβ€˜π‘—)β€˜π‘–))))
1951943adant1r 1174 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ 𝑖 ∈ 𝑋) β†’ (-𝑗[,)𝑗) = ((1st β€˜((πΌβ€˜π‘—)β€˜π‘–))[,)(2nd β€˜((πΌβ€˜π‘—)β€˜π‘–))))
196195ad5ant135 1365 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) ∧ 𝑗 ∈ β„•) ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ (-𝑗[,)𝑗) = ((1st β€˜((πΌβ€˜π‘—)β€˜π‘–))[,)(2nd β€˜((πΌβ€˜π‘—)β€˜π‘–))))
197164, 196eleqtrd 2830 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) ∧ 𝑗 ∈ β„•) ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ∈ ((1st β€˜((πΌβ€˜π‘—)β€˜π‘–))[,)(2nd β€˜((πΌβ€˜π‘—)β€˜π‘–))))
19879, 82sselid 3978 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ β„• β†’ -𝑗 ∈ ℝ)
199 opelxpi 5717 . . . . . . . . . . . . . . . . . . . . 21 ((-𝑗 ∈ ℝ ∧ 𝑗 ∈ ℝ) β†’ ⟨-𝑗, π‘—βŸ© ∈ (ℝ Γ— ℝ))
200198, 94, 199syl2anc 582 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ β„• β†’ ⟨-𝑗, π‘—βŸ© ∈ (ℝ Γ— ℝ))
201200ad2antlr 725 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑗 ∈ β„•) ∧ π‘₯ ∈ 𝑋) β†’ ⟨-𝑗, π‘—βŸ© ∈ (ℝ Γ— ℝ))
202 eqid 2727 . . . . . . . . . . . . . . . . . . 19 (π‘₯ ∈ 𝑋 ↦ ⟨-𝑗, π‘—βŸ©) = (π‘₯ ∈ 𝑋 ↦ ⟨-𝑗, π‘—βŸ©)
203201, 202fmptd 7127 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (π‘₯ ∈ 𝑋 ↦ ⟨-𝑗, π‘—βŸ©):π‘‹βŸΆ(ℝ Γ— ℝ))
204171feq1d 6710 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ ((πΌβ€˜π‘—):π‘‹βŸΆ(ℝ Γ— ℝ) ↔ (π‘₯ ∈ 𝑋 ↦ ⟨-𝑗, π‘—βŸ©):π‘‹βŸΆ(ℝ Γ— ℝ)))
205203, 204mpbird 256 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (πΌβ€˜π‘—):π‘‹βŸΆ(ℝ Γ— ℝ))
206205ad4ant14 750 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) ∧ 𝑗 ∈ β„•) β†’ (πΌβ€˜π‘—):π‘‹βŸΆ(ℝ Γ— ℝ))
207206ad2antrr 724 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) ∧ 𝑗 ∈ β„•) ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ (πΌβ€˜π‘—):π‘‹βŸΆ(ℝ Γ— ℝ))
208 simpr 483 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) ∧ 𝑗 ∈ β„•) ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ 𝑖 ∈ 𝑋)
209207, 208fvovco 44569 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) ∧ 𝑗 ∈ β„•) ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–) = ((1st β€˜((πΌβ€˜π‘—)β€˜π‘–))[,)(2nd β€˜((πΌβ€˜π‘—)β€˜π‘–))))
210209eqcomd 2733 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) ∧ 𝑗 ∈ β„•) ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ ((1st β€˜((πΌβ€˜π‘—)β€˜π‘–))[,)(2nd β€˜((πΌβ€˜π‘—)β€˜π‘–))) = (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–))
211197, 210eleqtrd 2830 . . . . . . . . . . . 12 ((((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) ∧ 𝑗 ∈ β„•) ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ∈ (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–))
212211ralrimiva 3142 . . . . . . . . . . 11 (((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) ∧ 𝑗 ∈ β„•) ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) β†’ βˆ€π‘– ∈ 𝑋 (π‘“β€˜π‘–) ∈ (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–))
21372, 212jca 510 . . . . . . . . . 10 (((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) ∧ 𝑗 ∈ β„•) ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) β†’ (𝑓 Fn 𝑋 ∧ βˆ€π‘– ∈ 𝑋 (π‘“β€˜π‘–) ∈ (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–)))
214 vex 3475 . . . . . . . . . . 11 𝑓 ∈ V
215214elixp 8927 . . . . . . . . . 10 (𝑓 ∈ X𝑖 ∈ 𝑋 (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–) ↔ (𝑓 Fn 𝑋 ∧ βˆ€π‘– ∈ 𝑋 (π‘“β€˜π‘–) ∈ (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–)))
216213, 215sylibr 233 . . . . . . . . 9 (((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) ∧ 𝑗 ∈ β„•) ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) β†’ 𝑓 ∈ X𝑖 ∈ 𝑋 (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–))
217216ex 411 . . . . . . . 8 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) ∧ 𝑗 ∈ β„•) β†’ (sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗 β†’ 𝑓 ∈ X𝑖 ∈ 𝑋 (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–)))
218217reximdva 3164 . . . . . . 7 (((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) β†’ (βˆƒπ‘— ∈ β„• sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗 β†’ βˆƒπ‘— ∈ β„• 𝑓 ∈ X𝑖 ∈ 𝑋 (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–)))
21969, 218mpd 15 . . . . . 6 (((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) β†’ βˆƒπ‘— ∈ β„• 𝑓 ∈ X𝑖 ∈ 𝑋 (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–))
22022, 23, 24, 219syl21anc 836 . . . . 5 (((πœ‘ ∧ Β¬ 𝑋 = βˆ…) ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) β†’ βˆƒπ‘— ∈ β„• 𝑓 ∈ X𝑖 ∈ 𝑋 (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–))
221 eliun 5002 . . . . 5 (𝑓 ∈ βˆͺ 𝑗 ∈ β„• X𝑖 ∈ 𝑋 (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–) ↔ βˆƒπ‘— ∈ β„• 𝑓 ∈ X𝑖 ∈ 𝑋 (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–))
222220, 221sylibr 233 . . . 4 (((πœ‘ ∧ Β¬ 𝑋 = βˆ…) ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) β†’ 𝑓 ∈ βˆͺ 𝑗 ∈ β„• X𝑖 ∈ 𝑋 (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–))
223222ralrimiva 3142 . . 3 ((πœ‘ ∧ Β¬ 𝑋 = βˆ…) β†’ βˆ€π‘“ ∈ (ℝ ↑m 𝑋)𝑓 ∈ βˆͺ 𝑗 ∈ β„• X𝑖 ∈ 𝑋 (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–))
224 dfss3 3968 . . 3 ((ℝ ↑m 𝑋) βŠ† βˆͺ 𝑗 ∈ β„• X𝑖 ∈ 𝑋 (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–) ↔ βˆ€π‘“ ∈ (ℝ ↑m 𝑋)𝑓 ∈ βˆͺ 𝑗 ∈ β„• X𝑖 ∈ 𝑋 (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–))
225223, 224sylibr 233 . 2 ((πœ‘ ∧ Β¬ 𝑋 = βˆ…) β†’ (ℝ ↑m 𝑋) βŠ† βˆͺ 𝑗 ∈ β„• X𝑖 ∈ 𝑋 (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–))
22621, 225pm2.61dan 811 1 (πœ‘ β†’ (ℝ ↑m 𝑋) βŠ† βˆͺ 𝑗 ∈ β„• X𝑖 ∈ 𝑋 (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 394   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098   β‰  wne 2936  βˆ€wral 3057  βˆƒwrex 3066  Vcvv 3471   βŠ† wss 3947  βˆ…c0 4324  {csn 4630  βŸ¨cop 4636  βˆͺ ciun 4998   class class class wbr 5150   ↦ cmpt 5233   Or wor 5591   Γ— cxp 5678  dom cdm 5680  ran crn 5681   ∘ ccom 5684  Fun wfun 6545   Fn wfn 6546  βŸΆwf 6547  β€˜cfv 6551  (class class class)co 7424  1st c1st 7995  2nd c2nd 7996   ↑m cmap 8849  Xcixp 8920  Fincfn 8968  supcsup 9469  β„‚cc 11142  β„cr 11143  1c1 11145  β„*cxr 11283   < clt 11284   ≀ cle 11285  -cneg 11481  β„•cn 12248  β„€cz 12594  [,)cico 13364  abscabs 15219
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 2166  ax-ext 2698  ax-rep 5287  ax-sep 5301  ax-nul 5308  ax-pow 5367  ax-pr 5431  ax-un 7744  ax-cnex 11200  ax-resscn 11201  ax-1cn 11202  ax-icn 11203  ax-addcl 11204  ax-addrcl 11205  ax-mulcl 11206  ax-mulrcl 11207  ax-mulcom 11208  ax-addass 11209  ax-mulass 11210  ax-distr 11211  ax-i2m1 11212  ax-1ne0 11213  ax-1rid 11214  ax-rnegex 11215  ax-rrecex 11216  ax-cnre 11217  ax-pre-lttri 11218  ax-pre-lttrn 11219  ax-pre-ltadd 11220  ax-pre-mulgt0 11221  ax-pre-sup 11222
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2937  df-nel 3043  df-ral 3058  df-rex 3067  df-rmo 3372  df-reu 3373  df-rab 3429  df-v 3473  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4325  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4911  df-iun 5000  df-br 5151  df-opab 5213  df-mpt 5234  df-tr 5268  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5635  df-we 5637  df-xp 5686  df-rel 5687  df-cnv 5688  df-co 5689  df-dm 5690  df-rn 5691  df-res 5692  df-ima 5693  df-pred 6308  df-ord 6375  df-on 6376  df-lim 6377  df-suc 6378  df-iota 6503  df-fun 6553  df-fn 6554  df-f 6555  df-f1 6556  df-fo 6557  df-f1o 6558  df-fv 6559  df-riota 7380  df-ov 7427  df-oprab 7428  df-mpo 7429  df-om 7875  df-1st 7997  df-2nd 7998  df-frecs 8291  df-wrecs 8322  df-recs 8396  df-rdg 8435  df-1o 8491  df-er 8729  df-map 8851  df-ixp 8921  df-en 8969  df-dom 8970  df-sdom 8971  df-fin 8972  df-sup 9471  df-pnf 11286  df-mnf 11287  df-xr 11288  df-ltxr 11289  df-le 11290  df-sub 11482  df-neg 11483  df-div 11908  df-nn 12249  df-2 12311  df-3 12312  df-n0 12509  df-z 12595  df-uz 12859  df-rp 13013  df-ico 13368  df-seq 14005  df-exp 14065  df-cj 15084  df-re 15085  df-im 15086  df-sqrt 15220  df-abs 15221
This theorem is referenced by:  hoicvrrex  45946
  Copyright terms: Public domain W3C validator