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 = ( 𝑡 ∈ Cat , 𝑢 ∈ Cat ↦ { ⟨ ( Base ‘ ndx ) , ( 𝑡 Func 𝑢 ) ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑡 Nat 𝑢 ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( ( 𝑡 Func 𝑢 ) × ( 𝑡 Func 𝑢 ) ) , ℎ ∈ ( 𝑡 Func 𝑢 ) ↦ ⦋ ( 1st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝑡 Nat 𝑢 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝑡 Nat 𝑢 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑡 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑢 ) ( ( 1st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) ⟩ } )
2		tpex	⊢ { ⟨ ( Base ‘ ndx ) , ( 𝑡 Func 𝑢 ) ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑡 Nat 𝑢 ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( ( 𝑡 Func 𝑢 ) × ( 𝑡 Func 𝑢 ) ) , ℎ ∈ ( 𝑡 Func 𝑢 ) ↦ ⦋ ( 1st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝑡 Nat 𝑢 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝑡 Nat 𝑢 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑡 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑢 ) ( ( 1st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) ⟩ } ∈ V
3	1 2	fnmpoi	⊢ FuncCat Fn ( Cat × Cat )