Step 
Hyp 
Ref 
Expression 
1 

xrltso 
⊢ < Or ℝ^{*} 
2 
1

supex 
⊢ sup ( { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( norm_{ℎ} ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( norm_{ℎ} ‘ ( 𝑇 ‘ 𝑦 ) ) ) } , ℝ^{*} , < ) ∈ V 
3 

axhilex 
⊢ ℋ ∈ V 
4 

fveq1 
⊢ ( 𝑡 = 𝑇 → ( 𝑡 ‘ 𝑦 ) = ( 𝑇 ‘ 𝑦 ) ) 
5 
4

fveq2d 
⊢ ( 𝑡 = 𝑇 → ( norm_{ℎ} ‘ ( 𝑡 ‘ 𝑦 ) ) = ( norm_{ℎ} ‘ ( 𝑇 ‘ 𝑦 ) ) ) 
6 
5

eqeq2d 
⊢ ( 𝑡 = 𝑇 → ( 𝑥 = ( norm_{ℎ} ‘ ( 𝑡 ‘ 𝑦 ) ) ↔ 𝑥 = ( norm_{ℎ} ‘ ( 𝑇 ‘ 𝑦 ) ) ) ) 
7 
6

anbi2d 
⊢ ( 𝑡 = 𝑇 → ( ( ( norm_{ℎ} ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( norm_{ℎ} ‘ ( 𝑡 ‘ 𝑦 ) ) ) ↔ ( ( norm_{ℎ} ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( norm_{ℎ} ‘ ( 𝑇 ‘ 𝑦 ) ) ) ) ) 
8 
7

rexbidv 
⊢ ( 𝑡 = 𝑇 → ( ∃ 𝑦 ∈ ℋ ( ( norm_{ℎ} ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( norm_{ℎ} ‘ ( 𝑡 ‘ 𝑦 ) ) ) ↔ ∃ 𝑦 ∈ ℋ ( ( norm_{ℎ} ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( norm_{ℎ} ‘ ( 𝑇 ‘ 𝑦 ) ) ) ) ) 
9 
8

abbidv 
⊢ ( 𝑡 = 𝑇 → { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( norm_{ℎ} ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( norm_{ℎ} ‘ ( 𝑡 ‘ 𝑦 ) ) ) } = { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( norm_{ℎ} ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( norm_{ℎ} ‘ ( 𝑇 ‘ 𝑦 ) ) ) } ) 
10 
9

supeq1d 
⊢ ( 𝑡 = 𝑇 → sup ( { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( norm_{ℎ} ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( norm_{ℎ} ‘ ( 𝑡 ‘ 𝑦 ) ) ) } , ℝ^{*} , < ) = sup ( { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( norm_{ℎ} ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( norm_{ℎ} ‘ ( 𝑇 ‘ 𝑦 ) ) ) } , ℝ^{*} , < ) ) 
11 

dfnmop 
⊢ norm_{op} = ( 𝑡 ∈ ( ℋ ↑_{m} ℋ ) ↦ sup ( { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( norm_{ℎ} ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( norm_{ℎ} ‘ ( 𝑡 ‘ 𝑦 ) ) ) } , ℝ^{*} , < ) ) 
12 
2 3 3 10 11

fvmptmap 
⊢ ( 𝑇 : ℋ ⟶ ℋ → ( norm_{op} ‘ 𝑇 ) = sup ( { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( norm_{ℎ} ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( norm_{ℎ} ‘ ( 𝑇 ‘ 𝑦 ) ) ) } , ℝ^{*} , < ) ) 