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

Metamath Proof Explorer

Theorem fnxpc

Description: The binary product of categories is a two-argument function. (Contributed by Mario Carneiro, 10-Jan-2017)

Ref Expression
Assertion fnxpc ⊢ × c Fn V × V

Proof

Step Hyp Ref Expression
1 df-xpc ⊢ × c = r ∈ V , s ∈ V ⟼ ⦋ Base r × Base s / b⦌ ⦋ u ∈ b , v ∈ b ⟼ 1 st ⁡ u Hom ⁡ r 1 st ⁡ v × 2 nd ⁡ u Hom ⁡ s 2 nd ⁡ v / h⦌ Base ndx b Hom ⁡ ndx h comp ⁡ ndx x ∈ b × b , y ∈ b ⟼ g ∈ 2 nd ⁡ x h y , f ∈ h ⁡ x ⟼ 1 st ⁡ g 1 st ⁡ 1 st ⁡ x 1 st ⁡ 2 nd ⁡ x comp ⁡ r 1 st ⁡ y 1 st ⁡ f 2 nd ⁡ g 2 nd ⁡ 1 st ⁡ x 2 nd ⁡ 2 nd ⁡ x comp ⁡ s 2 nd ⁡ y 2 nd ⁡ f
2 tpex ⊢ Base ndx b Hom ⁡ ndx h comp ⁡ ndx x ∈ b × b , y ∈ b ⟼ g ∈ 2 nd ⁡ x h y , f ∈ h ⁡ x ⟼ 1 st ⁡ g 1 st ⁡ 1 st ⁡ x 1 st ⁡ 2 nd ⁡ x comp ⁡ r 1 st ⁡ y 1 st ⁡ f 2 nd ⁡ g 2 nd ⁡ 1 st ⁡ x 2 nd ⁡ 2 nd ⁡ x comp ⁡ s 2 nd ⁡ y 2 nd ⁡ f ∈ V
3 2 csbex ⊢ ⦋ u ∈ b , v ∈ b ⟼ 1 st ⁡ u Hom ⁡ r 1 st ⁡ v × 2 nd ⁡ u Hom ⁡ s 2 nd ⁡ v / h⦌ Base ndx b Hom ⁡ ndx h comp ⁡ ndx x ∈ b × b , y ∈ b ⟼ g ∈ 2 nd ⁡ x h y , f ∈ h ⁡ x ⟼ 1 st ⁡ g 1 st ⁡ 1 st ⁡ x 1 st ⁡ 2 nd ⁡ x comp ⁡ r 1 st ⁡ y 1 st ⁡ f 2 nd ⁡ g 2 nd ⁡ 1 st ⁡ x 2 nd ⁡ 2 nd ⁡ x comp ⁡ s 2 nd ⁡ y 2 nd ⁡ f ∈ V
4 3 csbex ⊢ ⦋ Base r × Base s / b⦌ ⦋ u ∈ b , v ∈ b ⟼ 1 st ⁡ u Hom ⁡ r 1 st ⁡ v × 2 nd ⁡ u Hom ⁡ s 2 nd ⁡ v / h⦌ Base ndx b Hom ⁡ ndx h comp ⁡ ndx x ∈ b × b , y ∈ b ⟼ g ∈ 2 nd ⁡ x h y , f ∈ h ⁡ x ⟼ 1 st ⁡ g 1 st ⁡ 1 st ⁡ x 1 st ⁡ 2 nd ⁡ x comp ⁡ r 1 st ⁡ y 1 st ⁡ f 2 nd ⁡ g 2 nd ⁡ 1 st ⁡ x 2 nd ⁡ 2 nd ⁡ x comp ⁡ s 2 nd ⁡ y 2 nd ⁡ f ∈ V
5 1 4 fnmpoi ⊢ × c Fn V × V