Step |
Hyp |
Ref |
Expression |
1 |
|
ax-hilex |
⊢ ℋ ∈ V |
2 |
1 1
|
elmap |
⊢ ( 𝑆 ∈ ( ℋ ↑m ℋ ) ↔ 𝑆 : ℋ ⟶ ℋ ) |
3 |
1 1
|
elmap |
⊢ ( 𝑇 ∈ ( ℋ ↑m ℋ ) ↔ 𝑇 : ℋ ⟶ ℋ ) |
4 |
|
fveq1 |
⊢ ( 𝑓 = 𝑆 → ( 𝑓 ‘ 𝑥 ) = ( 𝑆 ‘ 𝑥 ) ) |
5 |
4
|
oveq1d |
⊢ ( 𝑓 = 𝑆 → ( ( 𝑓 ‘ 𝑥 ) −ℎ ( 𝑔 ‘ 𝑥 ) ) = ( ( 𝑆 ‘ 𝑥 ) −ℎ ( 𝑔 ‘ 𝑥 ) ) ) |
6 |
5
|
mpteq2dv |
⊢ ( 𝑓 = 𝑆 → ( 𝑥 ∈ ℋ ↦ ( ( 𝑓 ‘ 𝑥 ) −ℎ ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ℋ ↦ ( ( 𝑆 ‘ 𝑥 ) −ℎ ( 𝑔 ‘ 𝑥 ) ) ) ) |
7 |
|
fveq1 |
⊢ ( 𝑔 = 𝑇 → ( 𝑔 ‘ 𝑥 ) = ( 𝑇 ‘ 𝑥 ) ) |
8 |
7
|
oveq2d |
⊢ ( 𝑔 = 𝑇 → ( ( 𝑆 ‘ 𝑥 ) −ℎ ( 𝑔 ‘ 𝑥 ) ) = ( ( 𝑆 ‘ 𝑥 ) −ℎ ( 𝑇 ‘ 𝑥 ) ) ) |
9 |
8
|
mpteq2dv |
⊢ ( 𝑔 = 𝑇 → ( 𝑥 ∈ ℋ ↦ ( ( 𝑆 ‘ 𝑥 ) −ℎ ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ℋ ↦ ( ( 𝑆 ‘ 𝑥 ) −ℎ ( 𝑇 ‘ 𝑥 ) ) ) ) |
10 |
|
df-hodif |
⊢ −op = ( 𝑓 ∈ ( ℋ ↑m ℋ ) , 𝑔 ∈ ( ℋ ↑m ℋ ) ↦ ( 𝑥 ∈ ℋ ↦ ( ( 𝑓 ‘ 𝑥 ) −ℎ ( 𝑔 ‘ 𝑥 ) ) ) ) |
11 |
1
|
mptex |
⊢ ( 𝑥 ∈ ℋ ↦ ( ( 𝑆 ‘ 𝑥 ) −ℎ ( 𝑇 ‘ 𝑥 ) ) ) ∈ V |
12 |
6 9 10 11
|
ovmpo |
⊢ ( ( 𝑆 ∈ ( ℋ ↑m ℋ ) ∧ 𝑇 ∈ ( ℋ ↑m ℋ ) ) → ( 𝑆 −op 𝑇 ) = ( 𝑥 ∈ ℋ ↦ ( ( 𝑆 ‘ 𝑥 ) −ℎ ( 𝑇 ‘ 𝑥 ) ) ) ) |
13 |
2 3 12
|
syl2anbr |
⊢ ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( 𝑆 −op 𝑇 ) = ( 𝑥 ∈ ℋ ↦ ( ( 𝑆 ‘ 𝑥 ) −ℎ ( 𝑇 ‘ 𝑥 ) ) ) ) |