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