Metamath Proof Explorer

Theorem fucoelvv

Description: A functor composition bifunctor is an ordered pair. Enables 1st2ndb . (Contributed by Zhi Wang, 29-Sep-2025)

		Ref	Expression
	Hypotheses	fucofval.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑇 )
		fucofval.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑈 )
		fucofval.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑉 )
		fucofval.o	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) = ⚬ )
	Assertion	fucoelvv	⊢ ( 𝜑 → ⚬ ∈ ( V × V ) )

Proof

Step	Hyp	Ref	Expression
1		fucofval.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑇 )
2		fucofval.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑈 )
3		fucofval.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑉 )
4		fucofval.o	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) = ⚬ )
5		eqidd	⊢ ( 𝜑 → ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) = ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) )
6	1 2 3 4 5	fucofval	⊢ ( 𝜑 → ⚬ = ⟨ ( ∘_func ↾ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) , ( 𝑢 ∈ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) , 𝑣 ∈ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ↦ ⦋ ( 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		df-cofu	⊢ ∘_func = ( 𝑔 ∈ V , 𝑓 ∈ V ↦ ⟨ ( ( 1^st ‘ 𝑔 ) ∘ ( 1^st ‘ 𝑓 ) ) , ( 𝑥 ∈ dom dom ( 2^nd ‘ 𝑓 ) , 𝑦 ∈ dom dom ( 2^nd ‘ 𝑓 ) ↦ ( ( ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ( 2^nd ‘ 𝑔 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ) ) ⟩ )
8	7	mpofun	⊢ Fun ∘_func
9		ovex	⊢ ( 𝐷 Func 𝐸 ) ∈ V
10		ovex	⊢ ( 𝐶 Func 𝐷 ) ∈ V
11	9 10	xpex	⊢ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ∈ V
12		resfunexg	⊢ ( ( Fun ∘_func ∧ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ∈ V ) → ( ∘_func ↾ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) ∈ V )
13	8 11 12	mp2an	⊢ ( ∘_func ↾ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) ∈ V
14	11 11	mpoex	⊢ ( 𝑢 ∈ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) , 𝑣 ∈ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ↦ ⦋ ( 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	13 14	opelvv	⊢ ⟨ ( ∘_func ↾ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) , ( 𝑢 ∈ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) , 𝑣 ∈ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ↦ ⦋ ( 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 × V )
16	6 15	eqeltrdi	⊢ ( 𝜑 → ⚬ ∈ ( V × V ) )