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

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 ‘ 𝐺 ) 𝑌 ) ‘ 𝐾 ) ⟩ )