Metamath Proof Explorer

Theorem prf1

Description: Value of the pairing functor on objects. (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	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	Assertion	prf1	⊢ ( 𝜑 → ( ( 1^st ‘ 𝑃 ) ‘ 𝑋 ) = ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ⟩ )

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	1 2 3 4 5	prfval	⊢ ( 𝜑 → 𝑃 = ⟨ ( 𝑥 ∈ 𝐵 ↦ ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ℎ ∈ ( 𝑥 𝐻 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ⟩ ) ) ⟩ )
8	2	fvexi	⊢ 𝐵 ∈ V
9	8	mptex	⊢ ( 𝑥 ∈ 𝐵 ↦ ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ) ∈ V
10	8 8	mpoex	⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ℎ ∈ ( 𝑥 𝐻 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ⟩ ) ) ∈ V
11	9 10	op1std	⊢ ( 𝑃 = ⟨ ( 𝑥 ∈ 𝐵 ↦ ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ℎ ∈ ( 𝑥 𝐻 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ⟩ ) ) ⟩ → ( 1^st ‘ 𝑃 ) = ( 𝑥 ∈ 𝐵 ↦ ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ) )
12	7 11	syl	⊢ ( 𝜑 → ( 1^st ‘ 𝑃 ) = ( 𝑥 ∈ 𝐵 ↦ ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ) )
13		simpr	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → 𝑥 = 𝑋 )
14	13	fveq2d	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) )
15	13	fveq2d	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) )
16	14 15	opeq12d	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ = ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ⟩ )
17		opex	⊢ ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ⟩ ∈ V
18	17	a1i	⊢ ( 𝜑 → ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ⟩ ∈ V )
19	12 16 6 18	fvmptd	⊢ ( 𝜑 → ( ( 1^st ‘ 𝑃 ) ‘ 𝑋 ) = ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ⟩ )