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	⊢ ( 𝜑 → ( 𝑋 ( 2^nd ‘ 𝑃 ) 𝑌 ) = ( ℎ ∈ ( 𝑋 𝐻 𝑌 ) ↦ ⟨ ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑌 ) ‘ ℎ ) , ( ( 𝑋 ( 2^nd ‘ 𝐺 ) 𝑌 ) ‘ ℎ ) ⟩ ) )

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

Metamath Proof Explorer

Theorem prf2fval

Proof