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 ⊢ T ⁡ 0 ℎ ∈ x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = T ⁡ y

Proof

Step Hyp Ref Expression
1 ax-hv0cl ⊢ 0 ℎ ∈ ℋ
2 norm0 ⊢ norm ℎ ⁡ 0 ℎ = 0
3 0le1 ⊢ 0 ≤ 1
4 2 3 eqbrtri ⊢ norm ℎ ⁡ 0 ℎ ≤ 1
5 eqid ⊢ T ⁡ 0 ℎ = T ⁡ 0 ℎ
6 4 5 pm3.2i ⊢ norm ℎ ⁡ 0 ℎ ≤ 1 ∧ T ⁡ 0 ℎ = T ⁡ 0 ℎ
7 fveq2 ⊢ y = 0 ℎ → norm ℎ ⁡ y = norm ℎ ⁡ 0 ℎ
8 7 breq1d ⊢ y = 0 ℎ → norm ℎ ⁡ y ≤ 1 ↔ norm ℎ ⁡ 0 ℎ ≤ 1
9 2fveq3 ⊢ y = 0 ℎ → T ⁡ y = T ⁡ 0 ℎ
10 9 eqeq2d ⊢ y = 0 ℎ → T ⁡ 0 ℎ = T ⁡ y ↔ T ⁡ 0 ℎ = T ⁡ 0 ℎ
11 8 10 anbi12d ⊢ y = 0 ℎ → norm ℎ ⁡ y ≤ 1 ∧ T ⁡ 0 ℎ = T ⁡ y ↔ norm ℎ ⁡ 0 ℎ ≤ 1 ∧ T ⁡ 0 ℎ = T ⁡ 0 ℎ
12 11 rspcev ⊢ 0 ℎ ∈ ℋ ∧ norm ℎ ⁡ 0 ℎ ≤ 1 ∧ T ⁡ 0 ℎ = T ⁡ 0 ℎ → ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ T ⁡ 0 ℎ = T ⁡ y
13 1 6 12 mp2an ⊢ ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ T ⁡ 0 ℎ = T ⁡ y
14 fvex ⊢ T ⁡ 0 ℎ ∈ V
15 eqeq1 ⊢ x = T ⁡ 0 ℎ → x = T ⁡ y ↔ T ⁡ 0 ℎ = T ⁡ y
16 15 anbi2d ⊢ x = T ⁡ 0 ℎ → norm ℎ ⁡ y ≤ 1 ∧ x = T ⁡ y ↔ norm ℎ ⁡ y ≤ 1 ∧ T ⁡ 0 ℎ = T ⁡ y
17 16 rexbidv ⊢ x = T ⁡ 0 ℎ → ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = T ⁡ y ↔ ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ T ⁡ 0 ℎ = T ⁡ y
18 14 17 elab ⊢ T ⁡ 0 ℎ ∈ x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = T ⁡ y ↔ ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ T ⁡ 0 ℎ = T ⁡ y
19 13 18 mpbir ⊢ T ⁡ 0 ℎ ∈ x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = T ⁡ y