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	⊢ ( 𝑇 : ℋ ⟶ ℂ → { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( abs ‘ ( 𝑇 ‘ 𝑦 ) ) ) } ⊆ ℝ )

Proof

Step	Hyp	Ref	Expression
1		ffvelrn	⊢ ( ( 𝑇 : ℋ ⟶ ℂ ∧ 𝑦 ∈ ℋ ) → ( 𝑇 ‘ 𝑦 ) ∈ ℂ )
2	1	abscld	⊢ ( ( 𝑇 : ℋ ⟶ ℂ ∧ 𝑦 ∈ ℋ ) → ( abs ‘ ( 𝑇 ‘ 𝑦 ) ) ∈ ℝ )
3		eleq1	⊢ ( 𝑥 = ( abs ‘ ( 𝑇 ‘ 𝑦 ) ) → ( 𝑥 ∈ ℝ ↔ ( abs ‘ ( 𝑇 ‘ 𝑦 ) ) ∈ ℝ ) )
4	2 3	syl5ibr	⊢ ( 𝑥 = ( abs ‘ ( 𝑇 ‘ 𝑦 ) ) → ( ( 𝑇 : ℋ ⟶ ℂ ∧ 𝑦 ∈ ℋ ) → 𝑥 ∈ ℝ ) )
5	4	impcom	⊢ ( ( ( 𝑇 : ℋ ⟶ ℂ ∧ 𝑦 ∈ ℋ ) ∧ 𝑥 = ( abs ‘ ( 𝑇 ‘ 𝑦 ) ) ) → 𝑥 ∈ ℝ )
6	5	adantrl	⊢ ( ( ( 𝑇 : ℋ ⟶ ℂ ∧ 𝑦 ∈ ℋ ) ∧ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( abs ‘ ( 𝑇 ‘ 𝑦 ) ) ) ) → 𝑥 ∈ ℝ )
7	6	rexlimdva2	⊢ ( 𝑇 : ℋ ⟶ ℂ → ( ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( abs ‘ ( 𝑇 ‘ 𝑦 ) ) ) → 𝑥 ∈ ℝ ) )
8	7	abssdv	⊢ ( 𝑇 : ℋ ⟶ ℂ → { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( abs ‘ ( 𝑇 ‘ 𝑦 ) ) ) } ⊆ ℝ )