Metamath Proof Explorer

Theorem nmfnsetre

Description: The set in the supremum of the functional norm definition df-nmfn is a set of reals. (Contributed by NM, 14-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion nmfnsetre ${⊢}{T}:ℋ⟶ℂ\to \left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}=\left|{T}\left({y}\right)\right|\right)\right\}\subseteq ℝ$

Proof

Step Hyp Ref Expression
1 ffvelrn ${⊢}\left({T}:ℋ⟶ℂ\wedge {y}\in ℋ\right)\to {T}\left({y}\right)\in ℂ$
2 1 abscld ${⊢}\left({T}:ℋ⟶ℂ\wedge {y}\in ℋ\right)\to \left|{T}\left({y}\right)\right|\in ℝ$
3 eleq1 ${⊢}{x}=\left|{T}\left({y}\right)\right|\to \left({x}\in ℝ↔\left|{T}\left({y}\right)\right|\in ℝ\right)$
4 2 3 syl5ibr ${⊢}{x}=\left|{T}\left({y}\right)\right|\to \left(\left({T}:ℋ⟶ℂ\wedge {y}\in ℋ\right)\to {x}\in ℝ\right)$
5 4 impcom ${⊢}\left(\left({T}:ℋ⟶ℂ\wedge {y}\in ℋ\right)\wedge {x}=\left|{T}\left({y}\right)\right|\right)\to {x}\in ℝ$
6 5 adantrl ${⊢}\left(\left({T}:ℋ⟶ℂ\wedge {y}\in ℋ\right)\wedge \left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}=\left|{T}\left({y}\right)\right|\right)\right)\to {x}\in ℝ$
7 6 rexlimdva2 ${⊢}{T}:ℋ⟶ℂ\to \left(\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}=\left|{T}\left({y}\right)\right|\right)\to {x}\in ℝ\right)$
8 7 abssdv ${⊢}{T}:ℋ⟶ℂ\to \left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}=\left|{T}\left({y}\right)\right|\right)\right\}\subseteq ℝ$