Metamath Proof Explorer

Theorem funcf2

Description: The morphism part of a functor is a function on homsets. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses funcixp.b ⊢ 𝐵 = ( Base ‘ 𝐷 )
funcixp.h ⊢ 𝐻 = ( Hom ‘ 𝐷 )
funcixp.j ⊢ 𝐽 = ( Hom ‘ 𝐸 )
funcixp.f ⊢ ( 𝜑 → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
funcf2.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
funcf2.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion funcf2 ( 𝜑 → ( 𝑋 𝐺 𝑌 ) : ( 𝑋 𝐻 𝑌 ) ⟶ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 funcixp.b ⊢ 𝐵 = ( Base ‘ 𝐷 )
2 funcixp.h ⊢ 𝐻 = ( Hom ‘ 𝐷 )
3 funcixp.j ⊢ 𝐽 = ( Hom ‘ 𝐸 )
4 funcixp.f ⊢ ( 𝜑 → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
5 funcf2.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6 funcf2.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
7 df-ov ⊢ ( 𝑋 𝐺 𝑌 ) = ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ )
8 1 2 3 4 funcixp ⊢ ( 𝜑 → 𝐺 ∈ X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝐹 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝐹 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) )
9 5 6 opelxpd ⊢ ( 𝜑 → ⟨ 𝑋 , 𝑌 ⟩ ∈ ( 𝐵 × 𝐵 ) )
10 2fveq3 ⊢ ( 𝑧 = ⟨ 𝑋 , 𝑌 ⟩ → ( 𝐹 ‘ ( 1st ‘ 𝑧 ) ) = ( 𝐹 ‘ ( 1st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) )
11 2fveq3 ⊢ ( 𝑧 = ⟨ 𝑋 , 𝑌 ⟩ → ( 𝐹 ‘ ( 2nd ‘ 𝑧 ) ) = ( 𝐹 ‘ ( 2nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) )
12 10 11 oveq12d ⊢ ( 𝑧 = ⟨ 𝑋 , 𝑌 ⟩ → ( ( 𝐹 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝐹 ‘ ( 2nd ‘ 𝑧 ) ) ) = ( ( 𝐹 ‘ ( 1st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) 𝐽 ( 𝐹 ‘ ( 2nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) ) )
13 fveq2 ⊢ ( 𝑧 = ⟨ 𝑋 , 𝑌 ⟩ → ( 𝐻 ‘ 𝑧 ) = ( 𝐻 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) )
14 df-ov ⊢ ( 𝑋 𝐻 𝑌 ) = ( 𝐻 ‘ ⟨ 𝑋 , 𝑌 ⟩ )
15 13 14 eqtr4di ⊢ ( 𝑧 = ⟨ 𝑋 , 𝑌 ⟩ → ( 𝐻 ‘ 𝑧 ) = ( 𝑋 𝐻 𝑌 ) )
16 12 15 oveq12d ⊢ ( 𝑧 = ⟨ 𝑋 , 𝑌 ⟩ → ( ( ( 𝐹 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝐹 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) = ( ( ( 𝐹 ‘ ( 1st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) 𝐽 ( 𝐹 ‘ ( 2nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) ) ↑m ( 𝑋 𝐻 𝑌 ) ) )
17 16 fvixp ⊢ ( ( 𝐺 ∈ X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝐹 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝐹 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ∧ ⟨ 𝑋 , 𝑌 ⟩ ∈ ( 𝐵 × 𝐵 ) ) → ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ ( ( ( 𝐹 ‘ ( 1st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) 𝐽 ( 𝐹 ‘ ( 2nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) ) ↑m ( 𝑋 𝐻 𝑌 ) ) )
18 8 9 17 syl2anc ⊢ ( 𝜑 → ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ ( ( ( 𝐹 ‘ ( 1st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) 𝐽 ( 𝐹 ‘ ( 2nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) ) ↑m ( 𝑋 𝐻 𝑌 ) ) )
19 7 18 eqeltrid ⊢ ( 𝜑 → ( 𝑋 𝐺 𝑌 ) ∈ ( ( ( 𝐹 ‘ ( 1st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) 𝐽 ( 𝐹 ‘ ( 2nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) ) ↑m ( 𝑋 𝐻 𝑌 ) ) )
20 op1stg ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 1st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑋 )
21 20 fveq2d ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝐹 ‘ ( 1st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) = ( 𝐹 ‘ 𝑋 ) )
22 op2ndg ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 2nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑌 )
23 22 fveq2d ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝐹 ‘ ( 2nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) = ( 𝐹 ‘ 𝑌 ) )
24 21 23 oveq12d ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝐹 ‘ ( 1st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) 𝐽 ( 𝐹 ‘ ( 2nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) ) = ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) )
25 5 6 24 syl2anc ⊢ ( 𝜑 → ( ( 𝐹 ‘ ( 1st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) 𝐽 ( 𝐹 ‘ ( 2nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) ) = ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) )
26 25 oveq1d ⊢ ( 𝜑 → ( ( ( 𝐹 ‘ ( 1st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) 𝐽 ( 𝐹 ‘ ( 2nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) ) ↑m ( 𝑋 𝐻 𝑌 ) ) = ( ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) ↑m ( 𝑋 𝐻 𝑌 ) ) )
27 19 26 eleqtrd ⊢ ( 𝜑 → ( 𝑋 𝐺 𝑌 ) ∈ ( ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) ↑m ( 𝑋 𝐻 𝑌 ) ) )
28 elmapi ⊢ ( ( 𝑋 𝐺 𝑌 ) ∈ ( ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) ↑m ( 𝑋 𝐻 𝑌 ) ) → ( 𝑋 𝐺 𝑌 ) : ( 𝑋 𝐻 𝑌 ) ⟶ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) )
29 27 28 syl ⊢ ( 𝜑 → ( 𝑋 𝐺 𝑌 ) : ( 𝑋 𝐻 𝑌 ) ⟶ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) )