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 ⊢ P = F ⟨,⟩ F G
prfval.b ⊢ B = Base C
prfval.h ⊢ H = Hom ⁡ C
prfval.c ⊢ φ → F ∈ C Func D
prfval.d ⊢ φ → G ∈ C Func E
prf1.x ⊢ φ → X ∈ B
prf2.y ⊢ φ → Y ∈ B
prf2.k ⊢ φ → K ∈ X H Y
Assertion prf2 ⊢ φ → X 2 nd ⁡ P Y ⁡ K = X 2 nd ⁡ F Y ⁡ K X 2 nd ⁡ G Y ⁡ K

Proof

Step Hyp Ref Expression
1 prfval.k ⊢ P = F ⟨,⟩ F G
2 prfval.b ⊢ B = Base C
3 prfval.h ⊢ H = Hom ⁡ C
4 prfval.c ⊢ φ → F ∈ C Func D
5 prfval.d ⊢ φ → G ∈ C Func E
6 prf1.x ⊢ φ → X ∈ B
7 prf2.y ⊢ φ → Y ∈ B
8 prf2.k ⊢ φ → K ∈ X H Y
9 1 2 3 4 5 6 7 prf2fval ⊢ φ → X 2 nd ⁡ P Y = h ∈ X H Y ⟼ X 2 nd ⁡ F Y ⁡ h X 2 nd ⁡ G Y ⁡ h
10 simpr ⊢ φ ∧ h = K → h = K
11 10 fveq2d ⊢ φ ∧ h = K → X 2 nd ⁡ F Y ⁡ h = X 2 nd ⁡ F Y ⁡ K
12 10 fveq2d ⊢ φ ∧ h = K → X 2 nd ⁡ G Y ⁡ h = X 2 nd ⁡ G Y ⁡ K
13 11 12 opeq12d ⊢ φ ∧ h = K → X 2 nd ⁡ F Y ⁡ h X 2 nd ⁡ G Y ⁡ h = X 2 nd ⁡ F Y ⁡ K X 2 nd ⁡ G Y ⁡ K
14 opex ⊢ X 2 nd ⁡ F Y ⁡ K X 2 nd ⁡ G Y ⁡ K ∈ V
15 14 a1i ⊢ φ → X 2 nd ⁡ F Y ⁡ K X 2 nd ⁡ G Y ⁡ K ∈ V
16 9 13 8 15 fvmptd ⊢ φ → X 2 nd ⁡ P Y ⁡ K = X 2 nd ⁡ F Y ⁡ K X 2 nd ⁡ G Y ⁡ K