# 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 = ( 𝑟 ∈ V , 𝑠 ∈ V ↦ ( ( Base ‘ 𝑟 ) × ( Base ‘ 𝑠 ) ) / 𝑏 ( 𝑢𝑏 , 𝑣𝑏 ↦ ( ( ( 1st𝑢 ) ( Hom ‘ 𝑟 ) ( 1st𝑣 ) ) × ( ( 2nd𝑢 ) ( Hom ‘ 𝑠 ) ( 2nd𝑣 ) ) ) ) / { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( Hom ‘ ndx ) , ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑥 ∈ ( 𝑏 × 𝑏 ) , 𝑦𝑏 ↦ ( 𝑔 ∈ ( ( 2nd𝑥 ) 𝑦 ) , 𝑓 ∈ ( 𝑥 ) ↦ ⟨ ( ( 1st𝑔 ) ( ⟨ ( 1st ‘ ( 1st𝑥 ) ) , ( 1st ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑟 ) ( 1st𝑦 ) ) ( 1st𝑓 ) ) , ( ( 2nd𝑔 ) ( ⟨ ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑠 ) ( 2nd𝑦 ) ) ( 2nd𝑓 ) ) ⟩ ) ) ⟩ } )
2 tpex { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( Hom ‘ ndx ) , ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑥 ∈ ( 𝑏 × 𝑏 ) , 𝑦𝑏 ↦ ( 𝑔 ∈ ( ( 2nd𝑥 ) 𝑦 ) , 𝑓 ∈ ( 𝑥 ) ↦ ⟨ ( ( 1st𝑔 ) ( ⟨ ( 1st ‘ ( 1st𝑥 ) ) , ( 1st ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑟 ) ( 1st𝑦 ) ) ( 1st𝑓 ) ) , ( ( 2nd𝑔 ) ( ⟨ ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑠 ) ( 2nd𝑦 ) ) ( 2nd𝑓 ) ) ⟩ ) ) ⟩ } ∈ V
3 2 csbex ( 𝑢𝑏 , 𝑣𝑏 ↦ ( ( ( 1st𝑢 ) ( Hom ‘ 𝑟 ) ( 1st𝑣 ) ) × ( ( 2nd𝑢 ) ( Hom ‘ 𝑠 ) ( 2nd𝑣 ) ) ) ) / { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( Hom ‘ ndx ) , ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑥 ∈ ( 𝑏 × 𝑏 ) , 𝑦𝑏 ↦ ( 𝑔 ∈ ( ( 2nd𝑥 ) 𝑦 ) , 𝑓 ∈ ( 𝑥 ) ↦ ⟨ ( ( 1st𝑔 ) ( ⟨ ( 1st ‘ ( 1st𝑥 ) ) , ( 1st ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑟 ) ( 1st𝑦 ) ) ( 1st𝑓 ) ) , ( ( 2nd𝑔 ) ( ⟨ ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑠 ) ( 2nd𝑦 ) ) ( 2nd𝑓 ) ) ⟩ ) ) ⟩ } ∈ V
4 3 csbex ( ( Base ‘ 𝑟 ) × ( Base ‘ 𝑠 ) ) / 𝑏 ( 𝑢𝑏 , 𝑣𝑏 ↦ ( ( ( 1st𝑢 ) ( Hom ‘ 𝑟 ) ( 1st𝑣 ) ) × ( ( 2nd𝑢 ) ( Hom ‘ 𝑠 ) ( 2nd𝑣 ) ) ) ) / { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( Hom ‘ ndx ) , ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑥 ∈ ( 𝑏 × 𝑏 ) , 𝑦𝑏 ↦ ( 𝑔 ∈ ( ( 2nd𝑥 ) 𝑦 ) , 𝑓 ∈ ( 𝑥 ) ↦ ⟨ ( ( 1st𝑔 ) ( ⟨ ( 1st ‘ ( 1st𝑥 ) ) , ( 1st ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑟 ) ( 1st𝑦 ) ) ( 1st𝑓 ) ) , ( ( 2nd𝑔 ) ( ⟨ ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑠 ) ( 2nd𝑦 ) ) ( 2nd𝑓 ) ) ⟩ ) ) ⟩ } ∈ V
5 1 4 fnmpoi ×c Fn ( V × V )