Metamath Proof Explorer

Theorem fnfuc

Description: The FuncCat operation is a well-defined function on categories. (Contributed by Mario Carneiro, 12-Jan-2017)

Ref Expression
Assertion fnfuc ⊢ FuncCat Fn Cat × Cat

Proof

Step Hyp Ref Expression
1 df-fuc ⊢ FuncCat = t ∈ Cat , u ∈ Cat ⟼ Base ndx t Func u Hom ⁡ ndx t Nat u comp ⁡ ndx v ∈ t Func u × t Func u , h ∈ t Func u ⟼ ⦋ 1 st ⁡ v / f⦌ ⦋ 2 nd ⁡ v / g⦌ b ∈ g t Nat u h , a ∈ f t Nat u g ⟼ x ∈ Base t ⟼ b ⁡ x 1 st ⁡ f ⁡ x 1 st ⁡ g ⁡ x comp ⁡ u 1 st ⁡ h ⁡ x a ⁡ x
2 tpex ⊢ Base ndx t Func u Hom ⁡ ndx t Nat u comp ⁡ ndx v ∈ t Func u × t Func u , h ∈ t Func u ⟼ ⦋ 1 st ⁡ v / f⦌ ⦋ 2 nd ⁡ v / g⦌ b ∈ g t Nat u h , a ∈ f t Nat u g ⟼ x ∈ Base t ⟼ b ⁡ x 1 st ⁡ f ⁡ x 1 st ⁡ g ⁡ x comp ⁡ u 1 st ⁡ h ⁡ x a ⁡ x ∈ V
3 1 2 fnmpoi ⊢ FuncCat Fn Cat × Cat