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 44863
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 11149 . . . . . . 7 ℝ ∈ V
2 mapdm0 8787 . . . . . . 7 (ℝ ∈ V β†’ (ℝ ↑m βˆ…) = {βˆ…})
31, 2ax-mp 5 . . . . . 6 (ℝ ↑m βˆ…) = {βˆ…}
43a1i 11 . . . . 5 (𝑋 = βˆ… β†’ (ℝ ↑m βˆ…) = {βˆ…})
5 oveq2 7370 . . . . 5 (𝑋 = βˆ… β†’ (ℝ ↑m 𝑋) = (ℝ ↑m βˆ…))
6 ixpeq1 8853 . . . . . . 7 (𝑋 = βˆ… β†’ X𝑖 ∈ 𝑋 (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–) = X𝑖 ∈ βˆ… (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–))
76iuneq2d 4988 . . . . . 6 (𝑋 = βˆ… β†’ βˆͺ 𝑗 ∈ β„• X𝑖 ∈ 𝑋 (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–) = βˆͺ 𝑗 ∈ β„• X𝑖 ∈ βˆ… (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–))
8 ixp0x 8871 . . . . . . . . . 10 X𝑖 ∈ βˆ… (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–) = {βˆ…}
98a1i 11 . . . . . . . . 9 (𝑗 ∈ β„• β†’ X𝑖 ∈ βˆ… (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–) = {βˆ…})
109iuneq2i 4980 . . . . . . . 8 βˆͺ 𝑗 ∈ β„• X𝑖 ∈ βˆ… (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–) = βˆͺ 𝑗 ∈ β„• {βˆ…}
11 1nn 12171 . . . . . . . . . 10 1 ∈ β„•
1211ne0ii 4302 . . . . . . . . 9 β„• β‰  βˆ…
13 iunconst 4968 . . . . . . . . 9 (β„• β‰  βˆ… β†’ βˆͺ 𝑗 ∈ β„• {βˆ…} = {βˆ…})
1412, 13ax-mp 5 . . . . . . . 8 βˆͺ 𝑗 ∈ β„• {βˆ…} = {βˆ…}
1510, 14eqtri 2765 . . . . . . 7 βˆͺ 𝑗 ∈ β„• X𝑖 ∈ βˆ… (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–) = {βˆ…}
1615a1i 11 . . . . . 6 (𝑋 = βˆ… β†’ βˆͺ 𝑗 ∈ β„• X𝑖 ∈ βˆ… (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–) = {βˆ…})
177, 16eqtrd 2777 . . . . 5 (𝑋 = βˆ… β†’ βˆͺ 𝑗 ∈ β„• X𝑖 ∈ 𝑋 (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–) = {βˆ…})
184, 5, 173eqtr4d 2787 . . . 4 (𝑋 = βˆ… β†’ (ℝ ↑m 𝑋) = βˆͺ 𝑗 ∈ β„• X𝑖 ∈ 𝑋 (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–))
19 eqimss 4005 . . . 4 ((ℝ ↑m 𝑋) = βˆͺ 𝑗 ∈ β„• X𝑖 ∈ 𝑋 (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–) β†’ (ℝ ↑m 𝑋) βŠ† βˆͺ 𝑗 ∈ β„• X𝑖 ∈ 𝑋 (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–))
2018, 19syl 17 . . 3 (𝑋 = βˆ… β†’ (ℝ ↑m 𝑋) βŠ† βˆͺ 𝑗 ∈ β„• X𝑖 ∈ 𝑋 (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–))
2120adantl 483 . 2 ((πœ‘ ∧ 𝑋 = βˆ…) β†’ (ℝ ↑m 𝑋) βŠ† βˆͺ 𝑗 ∈ β„• X𝑖 ∈ 𝑋 (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–))
22 simpll 766 . . . . . 6 (((πœ‘ ∧ Β¬ 𝑋 = βˆ…) ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) β†’ πœ‘)
23 simpr 486 . . . . . 6 (((πœ‘ ∧ Β¬ 𝑋 = βˆ…) ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) β†’ 𝑓 ∈ (ℝ ↑m 𝑋))
24 simplr 768 . . . . . 6 (((πœ‘ ∧ Β¬ 𝑋 = βˆ…) ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) β†’ Β¬ 𝑋 = βˆ…)
25 rncoss 5932 . . . . . . . . . . 11 ran (abs ∘ 𝑓) βŠ† ran abs
26 absf 15229 . . . . . . . . . . . 12 abs:β„‚βŸΆβ„
27 frn 6680 . . . . . . . . . . . 12 (abs:β„‚βŸΆβ„ β†’ ran abs βŠ† ℝ)
2826, 27ax-mp 5 . . . . . . . . . . 11 ran abs βŠ† ℝ
2925, 28sstri 3958 . . . . . . . . . 10 ran (abs ∘ 𝑓) βŠ† ℝ
3029a1i 11 . . . . . . . . 9 (((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) β†’ ran (abs ∘ 𝑓) βŠ† ℝ)
31 ltso 11242 . . . . . . . . . . 11 < Or ℝ
3231a1i 11 . . . . . . . . . 10 (((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) β†’ < Or ℝ)
3326a1i 11 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) β†’ abs:β„‚βŸΆβ„)
34 elmapi 8794 . . . . . . . . . . . . . . 15 (𝑓 ∈ (ℝ ↑m 𝑋) β†’ 𝑓:π‘‹βŸΆβ„)
3534adantl 483 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) β†’ 𝑓:π‘‹βŸΆβ„)
36 ax-resscn 11115 . . . . . . . . . . . . . . 15 ℝ βŠ† β„‚
3736a1i 11 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) β†’ ℝ βŠ† β„‚)
3835, 37fssd 6691 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) β†’ 𝑓:π‘‹βŸΆβ„‚)
39 fco 6697 . . . . . . . . . . . . 13 ((abs:β„‚βŸΆβ„ ∧ 𝑓:π‘‹βŸΆβ„‚) β†’ (abs ∘ 𝑓):π‘‹βŸΆβ„)
4033, 38, 39syl2anc 585 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) β†’ (abs ∘ 𝑓):π‘‹βŸΆβ„)
41 hoicvr.3 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑋 ∈ Fin)
4241adantr 482 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) β†’ 𝑋 ∈ Fin)
43 rnffi 43466 . . . . . . . . . . . 12 (((abs ∘ 𝑓):π‘‹βŸΆβ„ ∧ 𝑋 ∈ Fin) β†’ ran (abs ∘ 𝑓) ∈ Fin)
4440, 42, 43syl2anc 585 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) β†’ ran (abs ∘ 𝑓) ∈ Fin)
4544adantr 482 . . . . . . . . . 10 (((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) β†’ ran (abs ∘ 𝑓) ∈ Fin)
4634frnd 6681 . . . . . . . . . . . . . . . . . . 19 (𝑓 ∈ (ℝ ↑m 𝑋) β†’ ran 𝑓 βŠ† ℝ)
4726fdmi 6685 . . . . . . . . . . . . . . . . . . . . . 22 dom abs = β„‚
4847eqcomi 2746 . . . . . . . . . . . . . . . . . . . . 21 β„‚ = dom abs
4936, 48sseqtri 3985 . . . . . . . . . . . . . . . . . . . 20 ℝ βŠ† dom abs
5049a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝑓 ∈ (ℝ ↑m 𝑋) β†’ ℝ βŠ† dom abs)
5146, 50sstrd 3959 . . . . . . . . . . . . . . . . . 18 (𝑓 ∈ (ℝ ↑m 𝑋) β†’ ran 𝑓 βŠ† dom abs)
52 dmcosseq 5933 . . . . . . . . . . . . . . . . . 18 (ran 𝑓 βŠ† dom abs β†’ dom (abs ∘ 𝑓) = dom 𝑓)
5351, 52syl 17 . . . . . . . . . . . . . . . . 17 (𝑓 ∈ (ℝ ↑m 𝑋) β†’ dom (abs ∘ 𝑓) = dom 𝑓)
5434fdmd 6684 . . . . . . . . . . . . . . . . 17 (𝑓 ∈ (ℝ ↑m 𝑋) β†’ dom 𝑓 = 𝑋)
5553, 54eqtrd 2777 . . . . . . . . . . . . . . . 16 (𝑓 ∈ (ℝ ↑m 𝑋) β†’ dom (abs ∘ 𝑓) = 𝑋)
5655adantr 482 . . . . . . . . . . . . . . 15 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ Β¬ 𝑋 = βˆ…) β†’ dom (abs ∘ 𝑓) = 𝑋)
57 neqne 2952 . . . . . . . . . . . . . . . 16 (Β¬ 𝑋 = βˆ… β†’ 𝑋 β‰  βˆ…)
5857adantl 483 . . . . . . . . . . . . . . 15 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ Β¬ 𝑋 = βˆ…) β†’ 𝑋 β‰  βˆ…)
5956, 58eqnetrd 3012 . . . . . . . . . . . . . 14 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ Β¬ 𝑋 = βˆ…) β†’ dom (abs ∘ 𝑓) β‰  βˆ…)
6059neneqd 2949 . . . . . . . . . . . . 13 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ Β¬ 𝑋 = βˆ…) β†’ Β¬ dom (abs ∘ 𝑓) = βˆ…)
61 dm0rn0 5885 . . . . . . . . . . . . 13 (dom (abs ∘ 𝑓) = βˆ… ↔ ran (abs ∘ 𝑓) = βˆ…)
6260, 61sylnib 328 . . . . . . . . . . . 12 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ Β¬ 𝑋 = βˆ…) β†’ Β¬ ran (abs ∘ 𝑓) = βˆ…)
6362neqned 2951 . . . . . . . . . . 11 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ Β¬ 𝑋 = βˆ…) β†’ ran (abs ∘ 𝑓) β‰  βˆ…)
6463adantll 713 . . . . . . . . . 10 (((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) β†’ ran (abs ∘ 𝑓) β‰  βˆ…)
65 fisupcl 9412 . . . . . . . . . 10 (( < Or ℝ ∧ (ran (abs ∘ 𝑓) ∈ Fin ∧ ran (abs ∘ 𝑓) β‰  βˆ… ∧ ran (abs ∘ 𝑓) βŠ† ℝ)) β†’ sup(ran (abs ∘ 𝑓), ℝ, < ) ∈ ran (abs ∘ 𝑓))
6632, 45, 64, 30, 65syl13anc 1373 . . . . . . . . 9 (((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) β†’ sup(ran (abs ∘ 𝑓), ℝ, < ) ∈ ran (abs ∘ 𝑓))
6730, 66sseldd 3950 . . . . . . . 8 (((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) β†’ sup(ran (abs ∘ 𝑓), ℝ, < ) ∈ ℝ)
68 arch 12417 . . . . . . . 8 (sup(ran (abs ∘ 𝑓), ℝ, < ) ∈ ℝ β†’ βˆƒπ‘— ∈ β„• sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗)
6967, 68syl 17 . . . . . . 7 (((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) β†’ βˆƒπ‘— ∈ β„• sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗)
7035ffnd 6674 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) β†’ 𝑓 Fn 𝑋)
7170ad2antrr 725 . . . . . . . . . . . 12 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) β†’ 𝑓 Fn 𝑋)
7271adantlr 714 . . . . . . . . . . 11 (((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) ∧ 𝑗 ∈ β„•) ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) β†’ 𝑓 Fn 𝑋)
73 simplll 774 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„•) ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ (πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)))
74 id 22 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ β„• β†’ 𝑗 ∈ β„•)
7574ad3antlr 730 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„•) ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ 𝑗 ∈ β„•)
76 simplr 768 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„•) ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗)
77 simpr 486 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„•) ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ 𝑖 ∈ 𝑋)
78 simp2 1138 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) β†’ 𝑗 ∈ β„•)
79 zssre 12513 . . . . . . . . . . . . . . . . . . . . 21 β„€ βŠ† ℝ
80 ressxr 11206 . . . . . . . . . . . . . . . . . . . . 21 ℝ βŠ† ℝ*
8179, 80sstri 3958 . . . . . . . . . . . . . . . . . . . 20 β„€ βŠ† ℝ*
82 nnnegz 12509 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ β„• β†’ -𝑗 ∈ β„€)
8381, 82sselid 3947 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ β„• β†’ -𝑗 ∈ ℝ*)
8483adantr 482 . . . . . . . . . . . . . . . . . 18 ((𝑗 ∈ β„• ∧ 𝑖 ∈ 𝑋) β†’ -𝑗 ∈ ℝ*)
8578, 84sylan 581 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ -𝑗 ∈ ℝ*)
8674nnxrd 43581 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ β„• β†’ 𝑗 ∈ ℝ*)
8786adantr 482 . . . . . . . . . . . . . . . . . 18 ((𝑗 ∈ β„• ∧ 𝑖 ∈ 𝑋) β†’ 𝑗 ∈ ℝ*)
8878, 87sylan 581 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ 𝑗 ∈ ℝ*)
89343ad2ant1 1134 . . . . . . . . . . . . . . . . . . . 20 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) β†’ 𝑓:π‘‹βŸΆβ„)
9080a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) β†’ ℝ βŠ† ℝ*)
9189, 90fssd 6691 . . . . . . . . . . . . . . . . . . 19 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) β†’ 𝑓:π‘‹βŸΆβ„*)
92913adant1l 1177 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) β†’ 𝑓:π‘‹βŸΆβ„*)
9392ffvelcdmda 7040 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ∈ ℝ*)
94 nnre 12167 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ β„• β†’ 𝑗 ∈ ℝ)
9594adantr 482 . . . . . . . . . . . . . . . . . . . 20 ((𝑗 ∈ β„• ∧ 𝑖 ∈ 𝑋) β†’ 𝑗 ∈ ℝ)
96953ad2antl2 1187 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ 𝑗 ∈ ℝ)
9796renegcld 11589 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ -𝑗 ∈ ℝ)
9835ffvelcdmda 7040 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ∈ ℝ)
99983ad2antl1 1186 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ∈ ℝ)
10099renegcld 11589 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ -(π‘“β€˜π‘–) ∈ ℝ)
101 simpll 766 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖 ∈ 𝑋) β†’ πœ‘)
102 simplr 768 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖 ∈ 𝑋) β†’ 𝑓 ∈ (ℝ ↑m 𝑋))
103 n0i 4298 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑖 ∈ 𝑋 β†’ Β¬ 𝑋 = βˆ…)
104103adantl 483 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖 ∈ 𝑋) β†’ Β¬ 𝑋 = βˆ…)
105101, 102, 104, 67syl21anc 837 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖 ∈ 𝑋) β†’ sup(ran (abs ∘ 𝑓), ℝ, < ) ∈ ℝ)
1061053ad2antl1 1186 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ sup(ran (abs ∘ 𝑓), ℝ, < ) ∈ ℝ)
10734ffvelcdmda 7040 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ∈ ℝ)
10836, 107sselid 3947 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ∈ β„‚)
109108abscld 15328 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ 𝑖 ∈ 𝑋) β†’ (absβ€˜(π‘“β€˜π‘–)) ∈ ℝ)
110109adantll 713 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖 ∈ 𝑋) β†’ (absβ€˜(π‘“β€˜π‘–)) ∈ ℝ)
1111103ad2antl1 1186 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ (absβ€˜(π‘“β€˜π‘–)) ∈ ℝ)
112107renegcld 11589 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ 𝑖 ∈ 𝑋) β†’ -(π‘“β€˜π‘–) ∈ ℝ)
113112leabsd 15306 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ 𝑖 ∈ 𝑋) β†’ -(π‘“β€˜π‘–) ≀ (absβ€˜-(π‘“β€˜π‘–)))
114108absnegd 15341 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ 𝑖 ∈ 𝑋) β†’ (absβ€˜-(π‘“β€˜π‘–)) = (absβ€˜(π‘“β€˜π‘–)))
115113, 114breqtrd 5136 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ 𝑖 ∈ 𝑋) β†’ -(π‘“β€˜π‘–) ≀ (absβ€˜(π‘“β€˜π‘–)))
116115adantll 713 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖 ∈ 𝑋) β†’ -(π‘“β€˜π‘–) ≀ (absβ€˜(π‘“β€˜π‘–)))
1171163ad2antl1 1186 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ -(π‘“β€˜π‘–) ≀ (absβ€˜(π‘“β€˜π‘–)))
11829a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ ran (abs ∘ 𝑓) βŠ† ℝ)
119104, 64syldan 592 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖 ∈ 𝑋) β†’ ran (abs ∘ 𝑓) β‰  βˆ…)
1201193ad2antl1 1186 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ ran (abs ∘ 𝑓) β‰  βˆ…)
121 fimaxre2 12107 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((ran (abs ∘ 𝑓) βŠ† ℝ ∧ ran (abs ∘ 𝑓) ∈ Fin) β†’ βˆƒπ‘¦ ∈ ℝ βˆ€π‘§ ∈ ran (abs ∘ 𝑓)𝑧 ≀ 𝑦)
12229, 44, 121sylancr 588 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) β†’ βˆƒπ‘¦ ∈ ℝ βˆ€π‘§ ∈ ran (abs ∘ 𝑓)𝑧 ≀ 𝑦)
123122adantr 482 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖 ∈ 𝑋) β†’ βˆƒπ‘¦ ∈ ℝ βˆ€π‘§ ∈ ran (abs ∘ 𝑓)𝑧 ≀ 𝑦)
1241233ad2antl1 1186 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ βˆƒπ‘¦ ∈ ℝ βˆ€π‘§ ∈ ran (abs ∘ 𝑓)𝑧 ≀ 𝑦)
125 elmapfun 8811 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑓 ∈ (ℝ ↑m 𝑋) β†’ Fun 𝑓)
126125adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ 𝑖 ∈ 𝑋) β†’ Fun 𝑓)
127 simpr 486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ 𝑖 ∈ 𝑋) β†’ 𝑖 ∈ 𝑋)
12854eqcomd 2743 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑓 ∈ (ℝ ↑m 𝑋) β†’ 𝑋 = dom 𝑓)
129128adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ 𝑖 ∈ 𝑋) β†’ 𝑋 = dom 𝑓)
130127, 129eleqtrd 2840 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ 𝑖 ∈ 𝑋) β†’ 𝑖 ∈ dom 𝑓)
131 fvco 6944 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((Fun 𝑓 ∧ 𝑖 ∈ dom 𝑓) β†’ ((abs ∘ 𝑓)β€˜π‘–) = (absβ€˜(π‘“β€˜π‘–)))
132126, 130, 131syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ 𝑖 ∈ 𝑋) β†’ ((abs ∘ 𝑓)β€˜π‘–) = (absβ€˜(π‘“β€˜π‘–)))
133132eqcomd 2743 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ 𝑖 ∈ 𝑋) β†’ (absβ€˜(π‘“β€˜π‘–)) = ((abs ∘ 𝑓)β€˜π‘–))
134 absfun 43658 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 Fun abs
135134a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑓 ∈ (ℝ ↑m 𝑋) β†’ Fun abs)
136 funco 6546 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((Fun abs ∧ Fun 𝑓) β†’ Fun (abs ∘ 𝑓))
137135, 125, 136syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑓 ∈ (ℝ ↑m 𝑋) β†’ Fun (abs ∘ 𝑓))
138137adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ 𝑖 ∈ 𝑋) β†’ Fun (abs ∘ 𝑓))
139108, 48eleqtrdi 2848 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ∈ dom abs)
140 dmfco 6942 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((Fun 𝑓 ∧ 𝑖 ∈ dom 𝑓) β†’ (𝑖 ∈ dom (abs ∘ 𝑓) ↔ (π‘“β€˜π‘–) ∈ dom abs))
141126, 130, 140syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ 𝑖 ∈ 𝑋) β†’ (𝑖 ∈ dom (abs ∘ 𝑓) ↔ (π‘“β€˜π‘–) ∈ dom abs))
142139, 141mpbird 257 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ 𝑖 ∈ 𝑋) β†’ 𝑖 ∈ dom (abs ∘ 𝑓))
143 fvelrn 7032 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((Fun (abs ∘ 𝑓) ∧ 𝑖 ∈ dom (abs ∘ 𝑓)) β†’ ((abs ∘ 𝑓)β€˜π‘–) ∈ ran (abs ∘ 𝑓))
144138, 142, 143syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ 𝑖 ∈ 𝑋) β†’ ((abs ∘ 𝑓)β€˜π‘–) ∈ ran (abs ∘ 𝑓))
145133, 144eqeltrd 2838 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑓 ∈ (ℝ ↑m 𝑋) ∧ 𝑖 ∈ 𝑋) β†’ (absβ€˜(π‘“β€˜π‘–)) ∈ ran (abs ∘ 𝑓))
146145adantll 713 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑖 ∈ 𝑋) β†’ (absβ€˜(π‘“β€˜π‘–)) ∈ ran (abs ∘ 𝑓))
1471463ad2antl1 1186 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ (absβ€˜(π‘“β€˜π‘–)) ∈ ran (abs ∘ 𝑓))
148 suprub 12123 . . . . . . . . . . . . . . . . . . . . . . 23 (((ran (abs ∘ 𝑓) βŠ† ℝ ∧ ran (abs ∘ 𝑓) β‰  βˆ… ∧ βˆƒπ‘¦ ∈ ℝ βˆ€π‘§ ∈ ran (abs ∘ 𝑓)𝑧 ≀ 𝑦) ∧ (absβ€˜(π‘“β€˜π‘–)) ∈ ran (abs ∘ 𝑓)) β†’ (absβ€˜(π‘“β€˜π‘–)) ≀ sup(ran (abs ∘ 𝑓), ℝ, < ))
149118, 120, 124, 147, 148syl31anc 1374 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ (absβ€˜(π‘“β€˜π‘–)) ≀ sup(ran (abs ∘ 𝑓), ℝ, < ))
150100, 111, 106, 117, 149letrd 11319 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ -(π‘“β€˜π‘–) ≀ sup(ran (abs ∘ 𝑓), ℝ, < ))
151 simpl3 1194 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗)
152100, 106, 96, 150, 151lelttrd 11320 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ -(π‘“β€˜π‘–) < 𝑗)
153100, 96ltnegd 11740 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ (-(π‘“β€˜π‘–) < 𝑗 ↔ -𝑗 < --(π‘“β€˜π‘–)))
154152, 153mpbid 231 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ -𝑗 < --(π‘“β€˜π‘–))
15536, 99sselid 3947 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ∈ β„‚)
156155negnegd 11510 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ --(π‘“β€˜π‘–) = (π‘“β€˜π‘–))
157154, 156breqtrd 5136 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ -𝑗 < (π‘“β€˜π‘–))
15897, 99, 157ltled 11310 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ -𝑗 ≀ (π‘“β€˜π‘–))
15999leabsd 15306 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ≀ (absβ€˜(π‘“β€˜π‘–)))
16099, 111, 106, 159, 149letrd 11319 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ≀ sup(ran (abs ∘ 𝑓), ℝ, < ))
16199, 106, 96, 160, 151lelttrd 11320 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) < 𝑗)
16285, 88, 93, 158, 161elicod 13321 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ∈ (-𝑗[,)𝑗))
16373, 75, 76, 77, 162syl31anc 1374 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„•) ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ∈ (-𝑗[,)𝑗))
164163adantl3r 749 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) ∧ 𝑗 ∈ β„•) ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ∈ (-𝑗[,)𝑗))
165 simpr 486 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ 𝑗 ∈ β„•)
166 mptexg 7176 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑋 ∈ Fin β†’ (π‘₯ ∈ 𝑋 ↦ ⟨-𝑗, π‘—βŸ©) ∈ V)
16741, 166syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ (π‘₯ ∈ 𝑋 ↦ ⟨-𝑗, π‘—βŸ©) ∈ V)
168167adantr 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (π‘₯ ∈ 𝑋 ↦ ⟨-𝑗, π‘—βŸ©) ∈ V)
169 hoicvr.2 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝐼 = (𝑗 ∈ β„• ↦ (π‘₯ ∈ 𝑋 ↦ ⟨-𝑗, π‘—βŸ©))
170169fvmpt2 6964 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑗 ∈ β„• ∧ (π‘₯ ∈ 𝑋 ↦ ⟨-𝑗, π‘—βŸ©) ∈ V) β†’ (πΌβ€˜π‘—) = (π‘₯ ∈ 𝑋 ↦ ⟨-𝑗, π‘—βŸ©))
171165, 168, 170syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (πΌβ€˜π‘—) = (π‘₯ ∈ 𝑋 ↦ ⟨-𝑗, π‘—βŸ©))
172171fveq1d 6849 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ ((πΌβ€˜π‘—)β€˜π‘–) = ((π‘₯ ∈ 𝑋 ↦ ⟨-𝑗, π‘—βŸ©)β€˜π‘–))
1731723adant3 1133 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ 𝑖 ∈ 𝑋) β†’ ((πΌβ€˜π‘—)β€˜π‘–) = ((π‘₯ ∈ 𝑋 ↦ ⟨-𝑗, π‘—βŸ©)β€˜π‘–))
174 eqidd 2738 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 ∈ 𝑋 β†’ (π‘₯ ∈ 𝑋 ↦ ⟨-𝑗, π‘—βŸ©) = (π‘₯ ∈ 𝑋 ↦ ⟨-𝑗, π‘—βŸ©))
175 eqid 2737 . . . . . . . . . . . . . . . . . . . . . . . 24 ⟨-𝑗, π‘—βŸ© = ⟨-𝑗, π‘—βŸ©
176175a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑖 ∈ 𝑋 ∧ π‘₯ = 𝑖) β†’ ⟨-𝑗, π‘—βŸ© = ⟨-𝑗, π‘—βŸ©)
177 id 22 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 ∈ 𝑋 β†’ 𝑖 ∈ 𝑋)
178 opex 5426 . . . . . . . . . . . . . . . . . . . . . . . 24 ⟨-𝑗, π‘—βŸ© ∈ V
179178a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 ∈ 𝑋 β†’ ⟨-𝑗, π‘—βŸ© ∈ V)
180174, 176, 177, 179fvmptd 6960 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 ∈ 𝑋 β†’ ((π‘₯ ∈ 𝑋 ↦ ⟨-𝑗, π‘—βŸ©)β€˜π‘–) = ⟨-𝑗, π‘—βŸ©)
1811803ad2ant3 1136 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ 𝑖 ∈ 𝑋) β†’ ((π‘₯ ∈ 𝑋 ↦ ⟨-𝑗, π‘—βŸ©)β€˜π‘–) = ⟨-𝑗, π‘—βŸ©)
182173, 181eqtrd 2777 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ 𝑖 ∈ 𝑋) β†’ ((πΌβ€˜π‘—)β€˜π‘–) = ⟨-𝑗, π‘—βŸ©)
183182fveq2d 6851 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ 𝑖 ∈ 𝑋) β†’ (1st β€˜((πΌβ€˜π‘—)β€˜π‘–)) = (1st β€˜βŸ¨-𝑗, π‘—βŸ©))
184 negex 11406 . . . . . . . . . . . . . . . . . . . . 21 -𝑗 ∈ V
185 vex 3452 . . . . . . . . . . . . . . . . . . . . 21 𝑗 ∈ V
186184, 185op1st 7934 . . . . . . . . . . . . . . . . . . . 20 (1st β€˜βŸ¨-𝑗, π‘—βŸ©) = -𝑗
187186a1i 11 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ 𝑖 ∈ 𝑋) β†’ (1st β€˜βŸ¨-𝑗, π‘—βŸ©) = -𝑗)
188183, 187eqtrd 2777 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ 𝑖 ∈ 𝑋) β†’ (1st β€˜((πΌβ€˜π‘—)β€˜π‘–)) = -𝑗)
189182fveq2d 6851 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ 𝑖 ∈ 𝑋) β†’ (2nd β€˜((πΌβ€˜π‘—)β€˜π‘–)) = (2nd β€˜βŸ¨-𝑗, π‘—βŸ©))
190184, 185op2nd 7935 . . . . . . . . . . . . . . . . . . . 20 (2nd β€˜βŸ¨-𝑗, π‘—βŸ©) = 𝑗
191190a1i 11 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ 𝑖 ∈ 𝑋) β†’ (2nd β€˜βŸ¨-𝑗, π‘—βŸ©) = 𝑗)
192189, 191eqtrd 2777 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ 𝑖 ∈ 𝑋) β†’ (2nd β€˜((πΌβ€˜π‘—)β€˜π‘–)) = 𝑗)
193188, 192oveq12d 7380 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ 𝑖 ∈ 𝑋) β†’ ((1st β€˜((πΌβ€˜π‘—)β€˜π‘–))[,)(2nd β€˜((πΌβ€˜π‘—)β€˜π‘–))) = (-𝑗[,)𝑗))
194193eqcomd 2743 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑗 ∈ β„• ∧ 𝑖 ∈ 𝑋) β†’ (-𝑗[,)𝑗) = ((1st β€˜((πΌβ€˜π‘—)β€˜π‘–))[,)(2nd β€˜((πΌβ€˜π‘—)β€˜π‘–))))
1951943adant1r 1178 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ 𝑗 ∈ β„• ∧ 𝑖 ∈ 𝑋) β†’ (-𝑗[,)𝑗) = ((1st β€˜((πΌβ€˜π‘—)β€˜π‘–))[,)(2nd β€˜((πΌβ€˜π‘—)β€˜π‘–))))
196195ad5ant135 1369 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) ∧ 𝑗 ∈ β„•) ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ (-𝑗[,)𝑗) = ((1st β€˜((πΌβ€˜π‘—)β€˜π‘–))[,)(2nd β€˜((πΌβ€˜π‘—)β€˜π‘–))))
197164, 196eleqtrd 2840 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) ∧ 𝑗 ∈ β„•) ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ∈ ((1st β€˜((πΌβ€˜π‘—)β€˜π‘–))[,)(2nd β€˜((πΌβ€˜π‘—)β€˜π‘–))))
19879, 82sselid 3947 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ β„• β†’ -𝑗 ∈ ℝ)
199 opelxpi 5675 . . . . . . . . . . . . . . . . . . . . 21 ((-𝑗 ∈ ℝ ∧ 𝑗 ∈ ℝ) β†’ ⟨-𝑗, π‘—βŸ© ∈ (ℝ Γ— ℝ))
200198, 94, 199syl2anc 585 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ β„• β†’ ⟨-𝑗, π‘—βŸ© ∈ (ℝ Γ— ℝ))
201200ad2antlr 726 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑗 ∈ β„•) ∧ π‘₯ ∈ 𝑋) β†’ ⟨-𝑗, π‘—βŸ© ∈ (ℝ Γ— ℝ))
202 eqid 2737 . . . . . . . . . . . . . . . . . . 19 (π‘₯ ∈ 𝑋 ↦ ⟨-𝑗, π‘—βŸ©) = (π‘₯ ∈ 𝑋 ↦ ⟨-𝑗, π‘—βŸ©)
203201, 202fmptd 7067 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (π‘₯ ∈ 𝑋 ↦ ⟨-𝑗, π‘—βŸ©):π‘‹βŸΆ(ℝ Γ— ℝ))
204171feq1d 6658 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ ((πΌβ€˜π‘—):π‘‹βŸΆ(ℝ Γ— ℝ) ↔ (π‘₯ ∈ 𝑋 ↦ ⟨-𝑗, π‘—βŸ©):π‘‹βŸΆ(ℝ Γ— ℝ)))
205203, 204mpbird 257 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (πΌβ€˜π‘—):π‘‹βŸΆ(ℝ Γ— ℝ))
206205ad4ant14 751 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) ∧ 𝑗 ∈ β„•) β†’ (πΌβ€˜π‘—):π‘‹βŸΆ(ℝ Γ— ℝ))
207206ad2antrr 725 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) ∧ 𝑗 ∈ β„•) ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ (πΌβ€˜π‘—):π‘‹βŸΆ(ℝ Γ— ℝ))
208 simpr 486 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) ∧ 𝑗 ∈ β„•) ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ 𝑖 ∈ 𝑋)
209207, 208fvovco 43487 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) ∧ 𝑗 ∈ β„•) ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–) = ((1st β€˜((πΌβ€˜π‘—)β€˜π‘–))[,)(2nd β€˜((πΌβ€˜π‘—)β€˜π‘–))))
210209eqcomd 2743 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) ∧ 𝑗 ∈ β„•) ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ ((1st β€˜((πΌβ€˜π‘—)β€˜π‘–))[,)(2nd β€˜((πΌβ€˜π‘—)β€˜π‘–))) = (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–))
211197, 210eleqtrd 2840 . . . . . . . . . . . 12 ((((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) ∧ 𝑗 ∈ β„•) ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ∈ (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–))
212211ralrimiva 3144 . . . . . . . . . . 11 (((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) ∧ 𝑗 ∈ β„•) ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) β†’ βˆ€π‘– ∈ 𝑋 (π‘“β€˜π‘–) ∈ (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–))
21372, 212jca 513 . . . . . . . . . 10 (((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) ∧ 𝑗 ∈ β„•) ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) β†’ (𝑓 Fn 𝑋 ∧ βˆ€π‘– ∈ 𝑋 (π‘“β€˜π‘–) ∈ (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–)))
214 vex 3452 . . . . . . . . . . 11 𝑓 ∈ V
215214elixp 8849 . . . . . . . . . 10 (𝑓 ∈ X𝑖 ∈ 𝑋 (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–) ↔ (𝑓 Fn 𝑋 ∧ βˆ€π‘– ∈ 𝑋 (π‘“β€˜π‘–) ∈ (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–)))
216213, 215sylibr 233 . . . . . . . . 9 (((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) ∧ 𝑗 ∈ β„•) ∧ sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗) β†’ 𝑓 ∈ X𝑖 ∈ 𝑋 (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–))
217216ex 414 . . . . . . . 8 ((((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) ∧ 𝑗 ∈ β„•) β†’ (sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗 β†’ 𝑓 ∈ X𝑖 ∈ 𝑋 (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–)))
218217reximdva 3166 . . . . . . 7 (((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) β†’ (βˆƒπ‘— ∈ β„• sup(ran (abs ∘ 𝑓), ℝ, < ) < 𝑗 β†’ βˆƒπ‘— ∈ β„• 𝑓 ∈ X𝑖 ∈ 𝑋 (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–)))
21969, 218mpd 15 . . . . . 6 (((πœ‘ ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) ∧ Β¬ 𝑋 = βˆ…) β†’ βˆƒπ‘— ∈ β„• 𝑓 ∈ X𝑖 ∈ 𝑋 (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–))
22022, 23, 24, 219syl21anc 837 . . . . 5 (((πœ‘ ∧ Β¬ 𝑋 = βˆ…) ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) β†’ βˆƒπ‘— ∈ β„• 𝑓 ∈ X𝑖 ∈ 𝑋 (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–))
221 eliun 4963 . . . . 5 (𝑓 ∈ βˆͺ 𝑗 ∈ β„• X𝑖 ∈ 𝑋 (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–) ↔ βˆƒπ‘— ∈ β„• 𝑓 ∈ X𝑖 ∈ 𝑋 (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–))
222220, 221sylibr 233 . . . 4 (((πœ‘ ∧ Β¬ 𝑋 = βˆ…) ∧ 𝑓 ∈ (ℝ ↑m 𝑋)) β†’ 𝑓 ∈ βˆͺ 𝑗 ∈ β„• X𝑖 ∈ 𝑋 (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–))
223222ralrimiva 3144 . . 3 ((πœ‘ ∧ Β¬ 𝑋 = βˆ…) β†’ βˆ€π‘“ ∈ (ℝ ↑m 𝑋)𝑓 ∈ βˆͺ 𝑗 ∈ β„• X𝑖 ∈ 𝑋 (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–))
224 dfss3 3937 . . 3 ((ℝ ↑m 𝑋) βŠ† βˆͺ 𝑗 ∈ β„• X𝑖 ∈ 𝑋 (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–) ↔ βˆ€π‘“ ∈ (ℝ ↑m 𝑋)𝑓 ∈ βˆͺ 𝑗 ∈ β„• X𝑖 ∈ 𝑋 (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–))
225223, 224sylibr 233 . 2 ((πœ‘ ∧ Β¬ 𝑋 = βˆ…) β†’ (ℝ ↑m 𝑋) βŠ† βˆͺ 𝑗 ∈ β„• X𝑖 ∈ 𝑋 (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–))
22621, 225pm2.61dan 812 1 (πœ‘ β†’ (ℝ ↑m 𝑋) βŠ† βˆͺ 𝑗 ∈ β„• X𝑖 ∈ 𝑋 (([,) ∘ (πΌβ€˜π‘—))β€˜π‘–))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107   β‰  wne 2944  βˆ€wral 3065  βˆƒwrex 3074  Vcvv 3448   βŠ† wss 3915  βˆ…c0 4287  {csn 4591  βŸ¨cop 4597  βˆͺ ciun 4959   class class class wbr 5110   ↦ cmpt 5193   Or wor 5549   Γ— cxp 5636  dom cdm 5638  ran crn 5639   ∘ ccom 5642  Fun wfun 6495   Fn wfn 6496  βŸΆwf 6497  β€˜cfv 6501  (class class class)co 7362  1st c1st 7924  2nd c2nd 7925   ↑m cmap 8772  Xcixp 8842  Fincfn 8890  supcsup 9383  β„‚cc 11056  β„cr 11057  1c1 11059  β„*cxr 11195   < clt 11196   ≀ cle 11197  -cneg 11393  β„•cn 12160  β„€cz 12506  [,)cico 13273  abscabs 15126
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-cnex 11114  ax-resscn 11115  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-addrcl 11119  ax-mulcl 11120  ax-mulrcl 11121  ax-mulcom 11122  ax-addass 11123  ax-mulass 11124  ax-distr 11125  ax-i2m1 11126  ax-1ne0 11127  ax-1rid 11128  ax-rnegex 11129  ax-rrecex 11130  ax-cnre 11131  ax-pre-lttri 11132  ax-pre-lttrn 11133  ax-pre-ltadd 11134  ax-pre-mulgt0 11135  ax-pre-sup 11136
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rmo 3356  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-om 7808  df-1st 7926  df-2nd 7927  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-1o 8417  df-er 8655  df-map 8774  df-ixp 8843  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-sup 9385  df-pnf 11198  df-mnf 11199  df-xr 11200  df-ltxr 11201  df-le 11202  df-sub 11394  df-neg 11395  df-div 11820  df-nn 12161  df-2 12223  df-3 12224  df-n0 12421  df-z 12507  df-uz 12771  df-rp 12923  df-ico 13277  df-seq 13914  df-exp 13975  df-cj 14991  df-re 14992  df-im 14993  df-sqrt 15127  df-abs 15128
This theorem is referenced by:  hoicvrrex  44871
  Copyright terms: Public domain W3C validator