Step |
Hyp |
Ref |
Expression |
1 |
|
homarcl.h |
⊢ 𝐻 = ( Homa ‘ 𝐶 ) |
2 |
|
homafval.b |
⊢ 𝐵 = ( Base ‘ 𝐶 ) |
3 |
|
homafval.c |
⊢ ( 𝜑 → 𝐶 ∈ Cat ) |
4 |
|
homaval.j |
⊢ 𝐽 = ( Hom ‘ 𝐶 ) |
5 |
|
homaval.x |
⊢ ( 𝜑 → 𝑋 ∈ 𝐵 ) |
6 |
|
homaval.y |
⊢ ( 𝜑 → 𝑌 ∈ 𝐵 ) |
7 |
|
df-ov |
⊢ ( 𝑋 𝐻 𝑌 ) = ( 𝐻 ‘ 〈 𝑋 , 𝑌 〉 ) |
8 |
1 2 3 4
|
homafval |
⊢ ( 𝜑 → 𝐻 = ( 𝑧 ∈ ( 𝐵 × 𝐵 ) ↦ ( { 𝑧 } × ( 𝐽 ‘ 𝑧 ) ) ) ) |
9 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑧 = 〈 𝑋 , 𝑌 〉 ) → 𝑧 = 〈 𝑋 , 𝑌 〉 ) |
10 |
9
|
sneqd |
⊢ ( ( 𝜑 ∧ 𝑧 = 〈 𝑋 , 𝑌 〉 ) → { 𝑧 } = { 〈 𝑋 , 𝑌 〉 } ) |
11 |
9
|
fveq2d |
⊢ ( ( 𝜑 ∧ 𝑧 = 〈 𝑋 , 𝑌 〉 ) → ( 𝐽 ‘ 𝑧 ) = ( 𝐽 ‘ 〈 𝑋 , 𝑌 〉 ) ) |
12 |
|
df-ov |
⊢ ( 𝑋 𝐽 𝑌 ) = ( 𝐽 ‘ 〈 𝑋 , 𝑌 〉 ) |
13 |
11 12
|
eqtr4di |
⊢ ( ( 𝜑 ∧ 𝑧 = 〈 𝑋 , 𝑌 〉 ) → ( 𝐽 ‘ 𝑧 ) = ( 𝑋 𝐽 𝑌 ) ) |
14 |
10 13
|
xpeq12d |
⊢ ( ( 𝜑 ∧ 𝑧 = 〈 𝑋 , 𝑌 〉 ) → ( { 𝑧 } × ( 𝐽 ‘ 𝑧 ) ) = ( { 〈 𝑋 , 𝑌 〉 } × ( 𝑋 𝐽 𝑌 ) ) ) |
15 |
5 6
|
opelxpd |
⊢ ( 𝜑 → 〈 𝑋 , 𝑌 〉 ∈ ( 𝐵 × 𝐵 ) ) |
16 |
|
snex |
⊢ { 〈 𝑋 , 𝑌 〉 } ∈ V |
17 |
|
ovex |
⊢ ( 𝑋 𝐽 𝑌 ) ∈ V |
18 |
16 17
|
xpex |
⊢ ( { 〈 𝑋 , 𝑌 〉 } × ( 𝑋 𝐽 𝑌 ) ) ∈ V |
19 |
18
|
a1i |
⊢ ( 𝜑 → ( { 〈 𝑋 , 𝑌 〉 } × ( 𝑋 𝐽 𝑌 ) ) ∈ V ) |
20 |
8 14 15 19
|
fvmptd |
⊢ ( 𝜑 → ( 𝐻 ‘ 〈 𝑋 , 𝑌 〉 ) = ( { 〈 𝑋 , 𝑌 〉 } × ( 𝑋 𝐽 𝑌 ) ) ) |
21 |
7 20
|
eqtrid |
⊢ ( 𝜑 → ( 𝑋 𝐻 𝑌 ) = ( { 〈 𝑋 , 𝑌 〉 } × ( 𝑋 𝐽 𝑌 ) ) ) |