Step |
Hyp |
Ref |
Expression |
1 |
|
homarcl.h |
⊢ 𝐻 = ( Homa ‘ 𝐶 ) |
2 |
|
homafval.b |
⊢ 𝐵 = ( Base ‘ 𝐶 ) |
3 |
|
homafval.c |
⊢ ( 𝜑 → 𝐶 ∈ Cat ) |
4 |
|
homafval.j |
⊢ 𝐽 = ( Hom ‘ 𝐶 ) |
5 |
|
fveq2 |
⊢ ( 𝑐 = 𝐶 → ( Base ‘ 𝑐 ) = ( Base ‘ 𝐶 ) ) |
6 |
5 2
|
eqtr4di |
⊢ ( 𝑐 = 𝐶 → ( Base ‘ 𝑐 ) = 𝐵 ) |
7 |
6
|
sqxpeqd |
⊢ ( 𝑐 = 𝐶 → ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑐 ) ) = ( 𝐵 × 𝐵 ) ) |
8 |
|
fveq2 |
⊢ ( 𝑐 = 𝐶 → ( Hom ‘ 𝑐 ) = ( Hom ‘ 𝐶 ) ) |
9 |
8 4
|
eqtr4di |
⊢ ( 𝑐 = 𝐶 → ( Hom ‘ 𝑐 ) = 𝐽 ) |
10 |
9
|
fveq1d |
⊢ ( 𝑐 = 𝐶 → ( ( Hom ‘ 𝑐 ) ‘ 𝑥 ) = ( 𝐽 ‘ 𝑥 ) ) |
11 |
10
|
xpeq2d |
⊢ ( 𝑐 = 𝐶 → ( { 𝑥 } × ( ( Hom ‘ 𝑐 ) ‘ 𝑥 ) ) = ( { 𝑥 } × ( 𝐽 ‘ 𝑥 ) ) ) |
12 |
7 11
|
mpteq12dv |
⊢ ( 𝑐 = 𝐶 → ( 𝑥 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑐 ) ) ↦ ( { 𝑥 } × ( ( Hom ‘ 𝑐 ) ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( 𝐵 × 𝐵 ) ↦ ( { 𝑥 } × ( 𝐽 ‘ 𝑥 ) ) ) ) |
13 |
|
df-homa |
⊢ Homa = ( 𝑐 ∈ Cat ↦ ( 𝑥 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑐 ) ) ↦ ( { 𝑥 } × ( ( Hom ‘ 𝑐 ) ‘ 𝑥 ) ) ) ) |
14 |
2
|
fvexi |
⊢ 𝐵 ∈ V |
15 |
14 14
|
xpex |
⊢ ( 𝐵 × 𝐵 ) ∈ V |
16 |
15
|
mptex |
⊢ ( 𝑥 ∈ ( 𝐵 × 𝐵 ) ↦ ( { 𝑥 } × ( 𝐽 ‘ 𝑥 ) ) ) ∈ V |
17 |
12 13 16
|
fvmpt |
⊢ ( 𝐶 ∈ Cat → ( Homa ‘ 𝐶 ) = ( 𝑥 ∈ ( 𝐵 × 𝐵 ) ↦ ( { 𝑥 } × ( 𝐽 ‘ 𝑥 ) ) ) ) |
18 |
3 17
|
syl |
⊢ ( 𝜑 → ( Homa ‘ 𝐶 ) = ( 𝑥 ∈ ( 𝐵 × 𝐵 ) ↦ ( { 𝑥 } × ( 𝐽 ‘ 𝑥 ) ) ) ) |
19 |
1 18
|
eqtrid |
⊢ ( 𝜑 → 𝐻 = ( 𝑥 ∈ ( 𝐵 × 𝐵 ) ↦ ( { 𝑥 } × ( 𝐽 ‘ 𝑥 ) ) ) ) |