This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Proof

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