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

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 = ( 𝑡 ∈ 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 )