# Metamath Proof Explorer

## Theorem nmfnsetn0

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

Ref Expression
Assertion nmfnsetn0 ${⊢}\left|{T}\left({0}_{ℎ}\right)\right|\in \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\}$

### Proof

Step Hyp Ref Expression
1 ax-hv0cl ${⊢}{0}_{ℎ}\in ℋ$
2 norm0 ${⊢}{norm}_{ℎ}\left({0}_{ℎ}\right)=0$
3 0le1 ${⊢}0\le 1$
4 2 3 eqbrtri ${⊢}{norm}_{ℎ}\left({0}_{ℎ}\right)\le 1$
5 eqid ${⊢}\left|{T}\left({0}_{ℎ}\right)\right|=\left|{T}\left({0}_{ℎ}\right)\right|$
6 4 5 pm3.2i ${⊢}\left({norm}_{ℎ}\left({0}_{ℎ}\right)\le 1\wedge \left|{T}\left({0}_{ℎ}\right)\right|=\left|{T}\left({0}_{ℎ}\right)\right|\right)$
7 fveq2 ${⊢}{y}={0}_{ℎ}\to {norm}_{ℎ}\left({y}\right)={norm}_{ℎ}\left({0}_{ℎ}\right)$
8 7 breq1d ${⊢}{y}={0}_{ℎ}\to \left({norm}_{ℎ}\left({y}\right)\le 1↔{norm}_{ℎ}\left({0}_{ℎ}\right)\le 1\right)$
9 2fveq3 ${⊢}{y}={0}_{ℎ}\to \left|{T}\left({y}\right)\right|=\left|{T}\left({0}_{ℎ}\right)\right|$
10 9 eqeq2d ${⊢}{y}={0}_{ℎ}\to \left(\left|{T}\left({0}_{ℎ}\right)\right|=\left|{T}\left({y}\right)\right|↔\left|{T}\left({0}_{ℎ}\right)\right|=\left|{T}\left({0}_{ℎ}\right)\right|\right)$
11 8 10 anbi12d ${⊢}{y}={0}_{ℎ}\to \left(\left({norm}_{ℎ}\left({y}\right)\le 1\wedge \left|{T}\left({0}_{ℎ}\right)\right|=\left|{T}\left({y}\right)\right|\right)↔\left({norm}_{ℎ}\left({0}_{ℎ}\right)\le 1\wedge \left|{T}\left({0}_{ℎ}\right)\right|=\left|{T}\left({0}_{ℎ}\right)\right|\right)\right)$
12 11 rspcev ${⊢}\left({0}_{ℎ}\in ℋ\wedge \left({norm}_{ℎ}\left({0}_{ℎ}\right)\le 1\wedge \left|{T}\left({0}_{ℎ}\right)\right|=\left|{T}\left({0}_{ℎ}\right)\right|\right)\right)\to \exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge \left|{T}\left({0}_{ℎ}\right)\right|=\left|{T}\left({y}\right)\right|\right)$
13 1 6 12 mp2an ${⊢}\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge \left|{T}\left({0}_{ℎ}\right)\right|=\left|{T}\left({y}\right)\right|\right)$
14 fvex ${⊢}\left|{T}\left({0}_{ℎ}\right)\right|\in \mathrm{V}$
15 eqeq1 ${⊢}{x}=\left|{T}\left({0}_{ℎ}\right)\right|\to \left({x}=\left|{T}\left({y}\right)\right|↔\left|{T}\left({0}_{ℎ}\right)\right|=\left|{T}\left({y}\right)\right|\right)$
16 15 anbi2d ${⊢}{x}=\left|{T}\left({0}_{ℎ}\right)\right|\to \left(\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}=\left|{T}\left({y}\right)\right|\right)↔\left({norm}_{ℎ}\left({y}\right)\le 1\wedge \left|{T}\left({0}_{ℎ}\right)\right|=\left|{T}\left({y}\right)\right|\right)\right)$
17 16 rexbidv ${⊢}{x}=\left|{T}\left({0}_{ℎ}\right)\right|\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)↔\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge \left|{T}\left({0}_{ℎ}\right)\right|=\left|{T}\left({y}\right)\right|\right)\right)$
18 14 17 elab ${⊢}\left|{T}\left({0}_{ℎ}\right)\right|\in \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\}↔\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge \left|{T}\left({0}_{ℎ}\right)\right|=\left|{T}\left({y}\right)\right|\right)$
19 13 18 mpbir ${⊢}\left|{T}\left({0}_{ℎ}\right)\right|\in \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\}$