Metamath Proof Explorer


Theorem homaval

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 )
homaval.j 𝐽 = ( Hom ‘ 𝐶 )
homaval.x ( 𝜑𝑋𝐵 )
homaval.y ( 𝜑𝑌𝐵 )
Assertion homaval ( 𝜑 → ( 𝑋 𝐻 𝑌 ) = ( { ⟨ 𝑋 , 𝑌 ⟩ } × ( 𝑋 𝐽 𝑌 ) ) )

Proof

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 ( 𝜑 → ( 𝑋 𝐻 𝑌 ) = ( { ⟨ 𝑋 , 𝑌 ⟩ } × ( 𝑋 𝐽 𝑌 ) ) )