Metamath Proof Explorer

Theorem prcofelvv

Description: The pre-composition functor is an ordered pair. (Contributed by Zhi Wang, 4-Nov-2025)

		Ref	Expression
	Hypotheses	prcofelvv.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑈 )
		prcofelvv.p	⊢ ( 𝜑 → 𝑃 ∈ 𝑉 )
	Assertion	prcofelvv	⊢ ( 𝜑 → ( 𝑃 −∘_F 𝐹 ) ∈ ( V × V ) )

Proof

Step	Hyp	Ref	Expression
1		prcofelvv.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑈 )
2		prcofelvv.p	⊢ ( 𝜑 → 𝑃 ∈ 𝑉 )
3		eqid	⊢ ( ( 1^st ‘ 𝑃 ) Func ( 2^nd ‘ 𝑃 ) ) = ( ( 1^st ‘ 𝑃 ) Func ( 2^nd ‘ 𝑃 ) )
4		eqid	⊢ ( ( 1^st ‘ 𝑃 ) Nat ( 2^nd ‘ 𝑃 ) ) = ( ( 1^st ‘ 𝑃 ) Nat ( 2^nd ‘ 𝑃 ) )
5		eqidd	⊢ ( 𝜑 → ( 1^st ‘ 𝑃 ) = ( 1^st ‘ 𝑃 ) )
6		eqidd	⊢ ( 𝜑 → ( 2^nd ‘ 𝑃 ) = ( 2^nd ‘ 𝑃 ) )
7	3 4 1 2 5 6	prcofvalg	⊢ ( 𝜑 → ( 𝑃 −∘_F 𝐹 ) = ⟨ ( 𝑘 ∈ ( ( 1^st ‘ 𝑃 ) Func ( 2^nd ‘ 𝑃 ) ) ↦ ( 𝑘 ∘_func 𝐹 ) ) , ( 𝑘 ∈ ( ( 1^st ‘ 𝑃 ) Func ( 2^nd ‘ 𝑃 ) ) , 𝑙 ∈ ( ( 1^st ‘ 𝑃 ) Func ( 2^nd ‘ 𝑃 ) ) ↦ ( 𝑎 ∈ ( 𝑘 ( ( 1^st ‘ 𝑃 ) Nat ( 2^nd ‘ 𝑃 ) ) 𝑙 ) ↦ ( 𝑎 ∘ ( 1^st ‘ 𝐹 ) ) ) ) ⟩ )
8		ovex	⊢ ( ( 1^st ‘ 𝑃 ) Func ( 2^nd ‘ 𝑃 ) ) ∈ V
9	8	mptex	⊢ ( 𝑘 ∈ ( ( 1^st ‘ 𝑃 ) Func ( 2^nd ‘ 𝑃 ) ) ↦ ( 𝑘 ∘_func 𝐹 ) ) ∈ V
10	8 8	mpoex	⊢ ( 𝑘 ∈ ( ( 1^st ‘ 𝑃 ) Func ( 2^nd ‘ 𝑃 ) ) , 𝑙 ∈ ( ( 1^st ‘ 𝑃 ) Func ( 2^nd ‘ 𝑃 ) ) ↦ ( 𝑎 ∈ ( 𝑘 ( ( 1^st ‘ 𝑃 ) Nat ( 2^nd ‘ 𝑃 ) ) 𝑙 ) ↦ ( 𝑎 ∘ ( 1^st ‘ 𝐹 ) ) ) ) ∈ V
11	9 10	opelvv	⊢ ⟨ ( 𝑘 ∈ ( ( 1^st ‘ 𝑃 ) Func ( 2^nd ‘ 𝑃 ) ) ↦ ( 𝑘 ∘_func 𝐹 ) ) , ( 𝑘 ∈ ( ( 1^st ‘ 𝑃 ) Func ( 2^nd ‘ 𝑃 ) ) , 𝑙 ∈ ( ( 1^st ‘ 𝑃 ) Func ( 2^nd ‘ 𝑃 ) ) ↦ ( 𝑎 ∈ ( 𝑘 ( ( 1^st ‘ 𝑃 ) Nat ( 2^nd ‘ 𝑃 ) ) 𝑙 ) ↦ ( 𝑎 ∘ ( 1^st ‘ 𝐹 ) ) ) ) ⟩ ∈ ( V × V )
12	7 11	eqeltrdi	⊢ ( 𝜑 → ( 𝑃 −∘_F 𝐹 ) ∈ ( V × V ) )