Metamath Proof Explorer


Theorem prf2

Description: Value of the pairing functor on morphisms. (Contributed by Mario Carneiro, 12-Jan-2017)

Ref Expression
Hypotheses prfval.k 𝑃 = ( 𝐹 ⟨,⟩F 𝐺 )
prfval.b 𝐵 = ( Base ‘ 𝐶 )
prfval.h 𝐻 = ( Hom ‘ 𝐶 )
prfval.c ( 𝜑𝐹 ∈ ( 𝐶 Func 𝐷 ) )
prfval.d ( 𝜑𝐺 ∈ ( 𝐶 Func 𝐸 ) )
prf1.x ( 𝜑𝑋𝐵 )
prf2.y ( 𝜑𝑌𝐵 )
prf2.k ( 𝜑𝐾 ∈ ( 𝑋 𝐻 𝑌 ) )
Assertion prf2 ( 𝜑 → ( ( 𝑋 ( 2nd𝑃 ) 𝑌 ) ‘ 𝐾 ) = ⟨ ( ( 𝑋 ( 2nd𝐹 ) 𝑌 ) ‘ 𝐾 ) , ( ( 𝑋 ( 2nd𝐺 ) 𝑌 ) ‘ 𝐾 ) ⟩ )

Proof

Step Hyp Ref Expression
1 prfval.k 𝑃 = ( 𝐹 ⟨,⟩F 𝐺 )
2 prfval.b 𝐵 = ( Base ‘ 𝐶 )
3 prfval.h 𝐻 = ( Hom ‘ 𝐶 )
4 prfval.c ( 𝜑𝐹 ∈ ( 𝐶 Func 𝐷 ) )
5 prfval.d ( 𝜑𝐺 ∈ ( 𝐶 Func 𝐸 ) )
6 prf1.x ( 𝜑𝑋𝐵 )
7 prf2.y ( 𝜑𝑌𝐵 )
8 prf2.k ( 𝜑𝐾 ∈ ( 𝑋 𝐻 𝑌 ) )
9 1 2 3 4 5 6 7 prf2fval ( 𝜑 → ( 𝑋 ( 2nd𝑃 ) 𝑌 ) = ( ∈ ( 𝑋 𝐻 𝑌 ) ↦ ⟨ ( ( 𝑋 ( 2nd𝐹 ) 𝑌 ) ‘ ) , ( ( 𝑋 ( 2nd𝐺 ) 𝑌 ) ‘ ) ⟩ ) )
10 simpr ( ( 𝜑 = 𝐾 ) → = 𝐾 )
11 10 fveq2d ( ( 𝜑 = 𝐾 ) → ( ( 𝑋 ( 2nd𝐹 ) 𝑌 ) ‘ ) = ( ( 𝑋 ( 2nd𝐹 ) 𝑌 ) ‘ 𝐾 ) )
12 10 fveq2d ( ( 𝜑 = 𝐾 ) → ( ( 𝑋 ( 2nd𝐺 ) 𝑌 ) ‘ ) = ( ( 𝑋 ( 2nd𝐺 ) 𝑌 ) ‘ 𝐾 ) )
13 11 12 opeq12d ( ( 𝜑 = 𝐾 ) → ⟨ ( ( 𝑋 ( 2nd𝐹 ) 𝑌 ) ‘ ) , ( ( 𝑋 ( 2nd𝐺 ) 𝑌 ) ‘ ) ⟩ = ⟨ ( ( 𝑋 ( 2nd𝐹 ) 𝑌 ) ‘ 𝐾 ) , ( ( 𝑋 ( 2nd𝐺 ) 𝑌 ) ‘ 𝐾 ) ⟩ )
14 opex ⟨ ( ( 𝑋 ( 2nd𝐹 ) 𝑌 ) ‘ 𝐾 ) , ( ( 𝑋 ( 2nd𝐺 ) 𝑌 ) ‘ 𝐾 ) ⟩ ∈ V
15 14 a1i ( 𝜑 → ⟨ ( ( 𝑋 ( 2nd𝐹 ) 𝑌 ) ‘ 𝐾 ) , ( ( 𝑋 ( 2nd𝐺 ) 𝑌 ) ‘ 𝐾 ) ⟩ ∈ V )
16 9 13 8 15 fvmptd ( 𝜑 → ( ( 𝑋 ( 2nd𝑃 ) 𝑌 ) ‘ 𝐾 ) = ⟨ ( ( 𝑋 ( 2nd𝐹 ) 𝑌 ) ‘ 𝐾 ) , ( ( 𝑋 ( 2nd𝐺 ) 𝑌 ) ‘ 𝐾 ) ⟩ )