Metamath Proof Explorer

Theorem fucofn2

Description: The morphism part of the functor composition bifunctor is a function on the Cartesian square of the base set. (Contributed by Zhi Wang, 29-Sep-2025)

		Ref	Expression
	Hypotheses	fucofval.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑇 )
		fucofval.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑈 )
		fucofval.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑉 )
		fuco1.o	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) = ⟨ 𝑂 , 𝑃 ⟩ )
		fuco1.w	⊢ ( 𝜑 → 𝑊 = ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) )
	Assertion	fucofn2	⊢ ( 𝜑 → 𝑃 Fn ( 𝑊 × 𝑊 ) )

Proof

Step	Hyp	Ref	Expression
1		fucofval.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑇 )
2		fucofval.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑈 )
3		fucofval.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑉 )
4		fuco1.o	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) = ⟨ 𝑂 , 𝑃 ⟩ )
5		fuco1.w	⊢ ( 𝜑 → 𝑊 = ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) )
6		eqid	⊢ ( 𝑢 ∈ 𝑊 , 𝑣 ∈ 𝑊 ↦ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑢 ) ) / 𝑓 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑢 ) ) / 𝑘 ⦌ ⦋ ( 2^nd ‘ ( 1^st ‘ 𝑢 ) ) / 𝑙 ⦌ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑣 ) ) / 𝑚 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑣 ) ) / 𝑟 ⦌ ( 𝑏 ∈ ( ( 1^st ‘ 𝑢 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑣 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑢 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) = ( 𝑢 ∈ 𝑊 , 𝑣 ∈ 𝑊 ↦ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑢 ) ) / 𝑓 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑢 ) ) / 𝑘 ⦌ ⦋ ( 2^nd ‘ ( 1^st ‘ 𝑢 ) ) / 𝑙 ⦌ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑣 ) ) / 𝑚 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑣 ) ) / 𝑟 ⦌ ( 𝑏 ∈ ( ( 1^st ‘ 𝑢 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑣 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑢 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) )
7		ovex	⊢ ( ( 1^st ‘ 𝑢 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑣 ) ) ∈ V
8		ovex	⊢ ( ( 2^nd ‘ 𝑢 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ∈ V
9	7 8	mpoex	⊢ ( 𝑏 ∈ ( ( 1^st ‘ 𝑢 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑣 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑢 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ∈ V
10	9	csbex	⊢ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑣 ) ) / 𝑟 ⦌ ( 𝑏 ∈ ( ( 1^st ‘ 𝑢 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑣 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑢 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ∈ V
11	10	csbex	⊢ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑣 ) ) / 𝑚 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑣 ) ) / 𝑟 ⦌ ( 𝑏 ∈ ( ( 1^st ‘ 𝑢 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑣 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑢 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ∈ V
12	11	csbex	⊢ ⦋ ( 2^nd ‘ ( 1^st ‘ 𝑢 ) ) / 𝑙 ⦌ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑣 ) ) / 𝑚 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑣 ) ) / 𝑟 ⦌ ( 𝑏 ∈ ( ( 1^st ‘ 𝑢 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑣 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑢 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ∈ V
13	12	csbex	⊢ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑢 ) ) / 𝑘 ⦌ ⦋ ( 2^nd ‘ ( 1^st ‘ 𝑢 ) ) / 𝑙 ⦌ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑣 ) ) / 𝑚 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑣 ) ) / 𝑟 ⦌ ( 𝑏 ∈ ( ( 1^st ‘ 𝑢 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑣 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑢 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ∈ V
14	13	csbex	⊢ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑢 ) ) / 𝑓 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑢 ) ) / 𝑘 ⦌ ⦋ ( 2^nd ‘ ( 1^st ‘ 𝑢 ) ) / 𝑙 ⦌ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑣 ) ) / 𝑚 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑣 ) ) / 𝑟 ⦌ ( 𝑏 ∈ ( ( 1^st ‘ 𝑢 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑣 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑢 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ∈ V
15	6 14	fnmpoi	⊢ ( 𝑢 ∈ 𝑊 , 𝑣 ∈ 𝑊 ↦ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑢 ) ) / 𝑓 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑢 ) ) / 𝑘 ⦌ ⦋ ( 2^nd ‘ ( 1^st ‘ 𝑢 ) ) / 𝑙 ⦌ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑣 ) ) / 𝑚 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑣 ) ) / 𝑟 ⦌ ( 𝑏 ∈ ( ( 1^st ‘ 𝑢 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑣 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑢 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) Fn ( 𝑊 × 𝑊 )
16	1 2 3 4 5	fuco2	⊢ ( 𝜑 → 𝑃 = ( 𝑢 ∈ 𝑊 , 𝑣 ∈ 𝑊 ↦ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑢 ) ) / 𝑓 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑢 ) ) / 𝑘 ⦌ ⦋ ( 2^nd ‘ ( 1^st ‘ 𝑢 ) ) / 𝑙 ⦌ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑣 ) ) / 𝑚 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑣 ) ) / 𝑟 ⦌ ( 𝑏 ∈ ( ( 1^st ‘ 𝑢 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑣 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑢 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) )
17	16	fneq1d	⊢ ( 𝜑 → ( 𝑃 Fn ( 𝑊 × 𝑊 ) ↔ ( 𝑢 ∈ 𝑊 , 𝑣 ∈ 𝑊 ↦ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑢 ) ) / 𝑓 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑢 ) ) / 𝑘 ⦌ ⦋ ( 2^nd ‘ ( 1^st ‘ 𝑢 ) ) / 𝑙 ⦌ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑣 ) ) / 𝑚 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑣 ) ) / 𝑟 ⦌ ( 𝑏 ∈ ( ( 1^st ‘ 𝑢 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑣 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑢 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) Fn ( 𝑊 × 𝑊 ) ) )
18	15 17	mpbiri	⊢ ( 𝜑 → 𝑃 Fn ( 𝑊 × 𝑊 ) )