This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem homafval

Description: Value of the disjointified hom-set function. (Contributed by Mario Carneiro, 11-Jan-2017)

Ref Expression
Hypotheses homarcl.h ⊢ 𝐻 = ( Homa ‘ 𝐶 )
homafval.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
homafval.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
homafval.j ⊢ 𝐽 = ( Hom ‘ 𝐶 )
Assertion homafval ( 𝜑 → 𝐻 = ( 𝑥 ∈ ( 𝐵 × 𝐵 ) ↦ ( { 𝑥 } × ( 𝐽 ‘ 𝑥 ) ) ) )

Proof

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 ⊢ ( 𝜑 → 𝐻 = ( 𝑥 ∈ ( 𝐵 × 𝐵 ) ↦ ( { 𝑥 } × ( 𝐽 ‘ 𝑥 ) ) ) )