Metamath Proof Explorer


Theorem prf2fval

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 ( 𝜑𝑌𝐵 )
Assertion prf2fval ( 𝜑 → ( 𝑋 ( 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 1 2 3 4 5 prfval ( 𝜑𝑃 = ⟨ ( 𝑥𝐵 ↦ ⟨ ( ( 1st𝐹 ) ‘ 𝑥 ) , ( ( 1st𝐺 ) ‘ 𝑥 ) ⟩ ) , ( 𝑥𝐵 , 𝑦𝐵 ↦ ( ∈ ( 𝑥 𝐻 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2nd𝐹 ) 𝑦 ) ‘ ) , ( ( 𝑥 ( 2nd𝐺 ) 𝑦 ) ‘ ) ⟩ ) ) ⟩ )
9 2 fvexi 𝐵 ∈ V
10 9 mptex ( 𝑥𝐵 ↦ ⟨ ( ( 1st𝐹 ) ‘ 𝑥 ) , ( ( 1st𝐺 ) ‘ 𝑥 ) ⟩ ) ∈ V
11 9 9 mpoex ( 𝑥𝐵 , 𝑦𝐵 ↦ ( ∈ ( 𝑥 𝐻 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2nd𝐹 ) 𝑦 ) ‘ ) , ( ( 𝑥 ( 2nd𝐺 ) 𝑦 ) ‘ ) ⟩ ) ) ∈ V
12 10 11 op2ndd ( 𝑃 = ⟨ ( 𝑥𝐵 ↦ ⟨ ( ( 1st𝐹 ) ‘ 𝑥 ) , ( ( 1st𝐺 ) ‘ 𝑥 ) ⟩ ) , ( 𝑥𝐵 , 𝑦𝐵 ↦ ( ∈ ( 𝑥 𝐻 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2nd𝐹 ) 𝑦 ) ‘ ) , ( ( 𝑥 ( 2nd𝐺 ) 𝑦 ) ‘ ) ⟩ ) ) ⟩ → ( 2nd𝑃 ) = ( 𝑥𝐵 , 𝑦𝐵 ↦ ( ∈ ( 𝑥 𝐻 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2nd𝐹 ) 𝑦 ) ‘ ) , ( ( 𝑥 ( 2nd𝐺 ) 𝑦 ) ‘ ) ⟩ ) ) )
13 8 12 syl ( 𝜑 → ( 2nd𝑃 ) = ( 𝑥𝐵 , 𝑦𝐵 ↦ ( ∈ ( 𝑥 𝐻 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2nd𝐹 ) 𝑦 ) ‘ ) , ( ( 𝑥 ( 2nd𝐺 ) 𝑦 ) ‘ ) ⟩ ) ) )
14 simprl ( ( 𝜑 ∧ ( 𝑥 = 𝑋𝑦 = 𝑌 ) ) → 𝑥 = 𝑋 )
15 simprr ( ( 𝜑 ∧ ( 𝑥 = 𝑋𝑦 = 𝑌 ) ) → 𝑦 = 𝑌 )
16 14 15 oveq12d ( ( 𝜑 ∧ ( 𝑥 = 𝑋𝑦 = 𝑌 ) ) → ( 𝑥 𝐻 𝑦 ) = ( 𝑋 𝐻 𝑌 ) )
17 14 15 oveq12d ( ( 𝜑 ∧ ( 𝑥 = 𝑋𝑦 = 𝑌 ) ) → ( 𝑥 ( 2nd𝐹 ) 𝑦 ) = ( 𝑋 ( 2nd𝐹 ) 𝑌 ) )
18 17 fveq1d ( ( 𝜑 ∧ ( 𝑥 = 𝑋𝑦 = 𝑌 ) ) → ( ( 𝑥 ( 2nd𝐹 ) 𝑦 ) ‘ ) = ( ( 𝑋 ( 2nd𝐹 ) 𝑌 ) ‘ ) )
19 14 15 oveq12d ( ( 𝜑 ∧ ( 𝑥 = 𝑋𝑦 = 𝑌 ) ) → ( 𝑥 ( 2nd𝐺 ) 𝑦 ) = ( 𝑋 ( 2nd𝐺 ) 𝑌 ) )
20 19 fveq1d ( ( 𝜑 ∧ ( 𝑥 = 𝑋𝑦 = 𝑌 ) ) → ( ( 𝑥 ( 2nd𝐺 ) 𝑦 ) ‘ ) = ( ( 𝑋 ( 2nd𝐺 ) 𝑌 ) ‘ ) )
21 18 20 opeq12d ( ( 𝜑 ∧ ( 𝑥 = 𝑋𝑦 = 𝑌 ) ) → ⟨ ( ( 𝑥 ( 2nd𝐹 ) 𝑦 ) ‘ ) , ( ( 𝑥 ( 2nd𝐺 ) 𝑦 ) ‘ ) ⟩ = ⟨ ( ( 𝑋 ( 2nd𝐹 ) 𝑌 ) ‘ ) , ( ( 𝑋 ( 2nd𝐺 ) 𝑌 ) ‘ ) ⟩ )
22 16 21 mpteq12dv ( ( 𝜑 ∧ ( 𝑥 = 𝑋𝑦 = 𝑌 ) ) → ( ∈ ( 𝑥 𝐻 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2nd𝐹 ) 𝑦 ) ‘ ) , ( ( 𝑥 ( 2nd𝐺 ) 𝑦 ) ‘ ) ⟩ ) = ( ∈ ( 𝑋 𝐻 𝑌 ) ↦ ⟨ ( ( 𝑋 ( 2nd𝐹 ) 𝑌 ) ‘ ) , ( ( 𝑋 ( 2nd𝐺 ) 𝑌 ) ‘ ) ⟩ ) )
23 ovex ( 𝑋 𝐻 𝑌 ) ∈ V
24 23 mptex ( ∈ ( 𝑋 𝐻 𝑌 ) ↦ ⟨ ( ( 𝑋 ( 2nd𝐹 ) 𝑌 ) ‘ ) , ( ( 𝑋 ( 2nd𝐺 ) 𝑌 ) ‘ ) ⟩ ) ∈ V
25 24 a1i ( 𝜑 → ( ∈ ( 𝑋 𝐻 𝑌 ) ↦ ⟨ ( ( 𝑋 ( 2nd𝐹 ) 𝑌 ) ‘ ) , ( ( 𝑋 ( 2nd𝐺 ) 𝑌 ) ‘ ) ⟩ ) ∈ V )
26 13 22 6 7 25 ovmpod ( 𝜑 → ( 𝑋 ( 2nd𝑃 ) 𝑌 ) = ( ∈ ( 𝑋 𝐻 𝑌 ) ↦ ⟨ ( ( 𝑋 ( 2nd𝐹 ) 𝑌 ) ‘ ) , ( ( 𝑋 ( 2nd𝐺 ) 𝑌 ) ‘ ) ⟩ ) )