Theorem prcofelvv

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

	Ref	Expression
Hypotheses	prcofelvv.f	$$⊢\phi \to F\in U$$
	prcofelvv.p	$$⊢\phi \to P\in V$$
Assertion	prcofelvv	Could not format assertion : No typesetting found for |- ( ph -> ( P -o.F F ) e. ( _V X. _V ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		prcofelvv.f	$$⊢\phi \to F\in U$$
2		prcofelvv.p	$$⊢\phi \to P\in V$$
3		eqid	$$⊢1^{st}\left(P\right)\mathrm{Func}{2}^{nd}\left(P\right)=1^{st}\left(P\right)\mathrm{Func}{2}^{nd}\left(P\right)$$
4		eqid	$$⊢1^{st}\left(P\right)\mathrm{Nat}{2}^{nd}\left(P\right)=1^{st}\left(P\right)\mathrm{Nat}{2}^{nd}\left(P\right)$$
5		eqidd	$$⊢\phi \to 1^{st}\left(P\right)=1^{st}\left(P\right)$$
6		eqidd	$$⊢\phi \to 2^{nd}\left(P\right)=2^{nd}\left(P\right)$$
7	3 4 1 2 5 6	prcofvalg	Could not format ( ph -> ( P -o.F F ) = <. ( k e. ( ( 1st ` P ) Func ( 2nd ` P ) ) |-> ( k o.func F ) ) , ( k e. ( ( 1st ` P ) Func ( 2nd ` P ) ) , l e. ( ( 1st ` P ) Func ( 2nd ` P ) ) |-> ( a e. ( k ( ( 1st ` P ) Nat ( 2nd ` P ) ) l ) |-> ( a o. ( 1st ` F ) ) ) ) >. ) : No typesetting found for |- ( ph -> ( P -o.F F ) = <. ( k e. ( ( 1st ` P ) Func ( 2nd ` P ) ) |-> ( k o.func F ) ) , ( k e. ( ( 1st ` P ) Func ( 2nd ` P ) ) , l e. ( ( 1st ` P ) Func ( 2nd ` P ) ) |-> ( a e. ( k ( ( 1st ` P ) Nat ( 2nd ` P ) ) l ) |-> ( a o. ( 1st ` F ) ) ) ) >. ) with typecode |-
8		ovex	$$⊢1^{st}\left(P\right)\mathrm{Func}{2}^{nd}\left(P\right)\in \mathrm{V}$$
9	8	mptex	$$⊢\left(k\in \left(1^{st}\left(P\right)\mathrm{Func}{2}^{nd}\left(P\right)\right)⟼k{\circ }_{\mathrm{func}}F\right)\in \mathrm{V}$$
10	8 8	mpoex	$$⊢\left(k\in \left(1^{st}\left(P\right)\mathrm{Func}{2}^{nd}\left(P\right)\right),l\in \left(1^{st}\left(P\right)\mathrm{Func}{2}^{nd}\left(P\right)\right)⟼\left(a\in \left(k\left(1^{st}\left(P\right)\mathrm{Nat}{2}^{nd}\left(P\right)\right)l\right)⟼a\circ 1^{st}\left(F\right)\right)\right)\in \mathrm{V}$$
11	9 10	opelvv	$$⊢⟨\left(k\in \left(1^{st}\left(P\right)\mathrm{Func}{2}^{nd}\left(P\right)\right)⟼k{\circ }_{\mathrm{func}}F\right),\left(k\in \left(1^{st}\left(P\right)\mathrm{Func}{2}^{nd}\left(P\right)\right),l\in \left(1^{st}\left(P\right)\mathrm{Func}{2}^{nd}\left(P\right)\right)⟼\left(a\in \left(k\left(1^{st}\left(P\right)\mathrm{Nat}{2}^{nd}\left(P\right)\right)l\right)⟼a\circ 1^{st}\left(F\right)\right)\right)⟩\in \left(\mathrm{V}\times \mathrm{V}\right)$$
12	7 11	eqeltrdi	Could not format ( ph -> ( P -o.F F ) e. ( _V X. _V ) ) : No typesetting found for |- ( ph -> ( P -o.F F ) e. ( _V X. _V ) ) with typecode |-