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

Metamath Proof Explorer

Theorem homffval

Description: Value of the functionalized Hom-set operation. (Contributed by Mario Carneiro, 4-Jan-2017) (Proof shortened by AV, 1-Mar-2024)

Ref Expression
Hypotheses homffval.f ⊢ 𝐹 = ( Homf ‘ 𝐶 )
homffval.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
homffval.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
Assertion homffval 𝐹 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 𝐻 𝑦 ) )

Proof

Step Hyp Ref Expression
1 homffval.f ⊢ 𝐹 = ( Homf ‘ 𝐶 )
2 homffval.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
3 homffval.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
4 fveq2 ⊢ ( 𝑐 = 𝐶 → ( Base ‘ 𝑐 ) = ( Base ‘ 𝐶 ) )
5 4 2 eqtr4di ⊢ ( 𝑐 = 𝐶 → ( Base ‘ 𝑐 ) = 𝐵 )
6 fveq2 ⊢ ( 𝑐 = 𝐶 → ( Hom ‘ 𝑐 ) = ( Hom ‘ 𝐶 ) )
7 6 3 eqtr4di ⊢ ( 𝑐 = 𝐶 → ( Hom ‘ 𝑐 ) = 𝐻 )
8 7 oveqd ⊢ ( 𝑐 = 𝐶 → ( 𝑥 ( Hom ‘ 𝑐 ) 𝑦 ) = ( 𝑥 𝐻 𝑦 ) )
9 5 5 8 mpoeq123dv ⊢ ( 𝑐 = 𝐶 → ( 𝑥 ∈ ( Base ‘ 𝑐 ) , 𝑦 ∈ ( Base ‘ 𝑐 ) ↦ ( 𝑥 ( Hom ‘ 𝑐 ) 𝑦 ) ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 𝐻 𝑦 ) ) )
10 df-homf ⊢ Homf = ( 𝑐 ∈ V ↦ ( 𝑥 ∈ ( Base ‘ 𝑐 ) , 𝑦 ∈ ( Base ‘ 𝑐 ) ↦ ( 𝑥 ( Hom ‘ 𝑐 ) 𝑦 ) ) )
11 2 fvexi ⊢ 𝐵 ∈ V
12 11 11 mpoex ⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 𝐻 𝑦 ) ) ∈ V
13 9 10 12 fvmpt ⊢ ( 𝐶 ∈ V → ( Homf ‘ 𝐶 ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 𝐻 𝑦 ) ) )
14 fvprc ⊢ ( ¬ 𝐶 ∈ V → ( Homf ‘ 𝐶 ) = ∅ )
15 fvprc ⊢ ( ¬ 𝐶 ∈ V → ( Base ‘ 𝐶 ) = ∅ )
16 2 15 eqtrid ⊢ ( ¬ 𝐶 ∈ V → 𝐵 = ∅ )
17 16 olcd ⊢ ( ¬ 𝐶 ∈ V → ( 𝐵 = ∅ ∨ 𝐵 = ∅ ) )
18 0mpo0 ⊢ ( ( 𝐵 = ∅ ∨ 𝐵 = ∅ ) → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 𝐻 𝑦 ) ) = ∅ )
19 17 18 syl ⊢ ( ¬ 𝐶 ∈ V → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 𝐻 𝑦 ) ) = ∅ )
20 14 19 eqtr4d ⊢ ( ¬ 𝐶 ∈ V → ( Homf ‘ 𝐶 ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 𝐻 𝑦 ) ) )
21 13 20 pm2.61i ⊢ ( Homf ‘ 𝐶 ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 𝐻 𝑦 ) )
22 1 21 eqtri ⊢ 𝐹 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 𝐻 𝑦 ) )