Theorem reldmprcof2

Description: The domain of the morphism part of the pre-composition functor is a relation. (Contributed by Zhi Wang, 2-Nov-2025)

	Ref	Expression
Assertion	reldmprcof2	Could not format assertion : No typesetting found for |- Rel dom ( 2nd ` ( P -o.F F ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\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)=\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)$$
2	1	reldmmpo	$$⊢\mathrm{Rel}\mathrm{dom}\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)$$
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		simpr	$$⊢\left(P\in \mathrm{V}\wedge F\in \mathrm{V}\right)\to F\in \mathrm{V}$$
6		simpl	$$⊢\left(P\in \mathrm{V}\wedge F\in \mathrm{V}\right)\to P\in \mathrm{V}$$
7		eqidd	$$⊢\left(P\in \mathrm{V}\wedge F\in \mathrm{V}\right)\to 1^{st}\left(P\right)=1^{st}\left(P\right)$$
8		eqidd	$$⊢\left(P\in \mathrm{V}\wedge F\in \mathrm{V}\right)\to 2^{nd}\left(P\right)=2^{nd}\left(P\right)$$
9	3 4 5 6 7 8	prcofvalg	Could not format ( ( P e. _V /\ F e. _V ) -> ( 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 |- ( ( P e. _V /\ F e. _V ) -> ( 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 |-
10		ovex	$$⊢1^{st}\left(P\right)\mathrm{Func}{2}^{nd}\left(P\right)\in \mathrm{V}$$
11	10	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}$$
12	10 10	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}$$
13	11 12	op2ndd	Could not format ( ( 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 ) ) ) ) >. -> ( 2nd ` ( P -o.F 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 |- ( ( 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 ) ) ) ) >. -> ( 2nd ` ( P -o.F 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 |-
14	9 13	syl	Could not format ( ( P e. _V /\ F e. _V ) -> ( 2nd ` ( P -o.F 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 |- ( ( P e. _V /\ F e. _V ) -> ( 2nd ` ( P -o.F 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 |-
15	14	dmeqd	Could not format ( ( P e. _V /\ F e. _V ) -> dom ( 2nd ` ( P -o.F F ) ) = dom ( 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 |- ( ( P e. _V /\ F e. _V ) -> dom ( 2nd ` ( P -o.F F ) ) = dom ( 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 |-
16	15	releqd	Could not format ( ( P e. _V /\ F e. _V ) -> ( Rel dom ( 2nd ` ( P -o.F F ) ) <-> Rel dom ( 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 |- ( ( P e. _V /\ F e. _V ) -> ( Rel dom ( 2nd ` ( P -o.F F ) ) <-> Rel dom ( 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 |-
17	2 16	mpbiri	Could not format ( ( P e. _V /\ F e. _V ) -> Rel dom ( 2nd ` ( P -o.F F ) ) ) : No typesetting found for |- ( ( P e. _V /\ F e. _V ) -> Rel dom ( 2nd ` ( P -o.F F ) ) ) with typecode |-
18		rel0	$$⊢\mathrm{Rel}\varnothing$$
19		reldmprcof	Could not format Rel dom -o.F : No typesetting found for |- Rel dom -o.F with typecode |-
20	19	ovprc	Could not format ( -. ( P e. _V /\ F e. _V ) -> ( P -o.F F ) = (/) ) : No typesetting found for |- ( -. ( P e. _V /\ F e. _V ) -> ( P -o.F F ) = (/) ) with typecode |-
21	20	fveq2d	Could not format ( -. ( P e. _V /\ F e. _V ) -> ( 2nd ` ( P -o.F F ) ) = ( 2nd ` (/) ) ) : No typesetting found for |- ( -. ( P e. _V /\ F e. _V ) -> ( 2nd ` ( P -o.F F ) ) = ( 2nd ` (/) ) ) with typecode |-
22		2nd0	$$⊢2^{nd}\left(\varnothing \right)=\varnothing$$
23	21 22	eqtrdi	Could not format ( -. ( P e. _V /\ F e. _V ) -> ( 2nd ` ( P -o.F F ) ) = (/) ) : No typesetting found for |- ( -. ( P e. _V /\ F e. _V ) -> ( 2nd ` ( P -o.F F ) ) = (/) ) with typecode |-
24	23	dmeqd	Could not format ( -. ( P e. _V /\ F e. _V ) -> dom ( 2nd ` ( P -o.F F ) ) = dom (/) ) : No typesetting found for |- ( -. ( P e. _V /\ F e. _V ) -> dom ( 2nd ` ( P -o.F F ) ) = dom (/) ) with typecode |-
25		dm0	$$⊢\mathrm{dom}\varnothing =\varnothing$$
26	24 25	eqtrdi	Could not format ( -. ( P e. _V /\ F e. _V ) -> dom ( 2nd ` ( P -o.F F ) ) = (/) ) : No typesetting found for |- ( -. ( P e. _V /\ F e. _V ) -> dom ( 2nd ` ( P -o.F F ) ) = (/) ) with typecode |-
27	26	releqd	Could not format ( -. ( P e. _V /\ F e. _V ) -> ( Rel dom ( 2nd ` ( P -o.F F ) ) <-> Rel (/) ) ) : No typesetting found for |- ( -. ( P e. _V /\ F e. _V ) -> ( Rel dom ( 2nd ` ( P -o.F F ) ) <-> Rel (/) ) ) with typecode |-
28	18 27	mpbiri	Could not format ( -. ( P e. _V /\ F e. _V ) -> Rel dom ( 2nd ` ( P -o.F F ) ) ) : No typesetting found for |- ( -. ( P e. _V /\ F e. _V ) -> Rel dom ( 2nd ` ( P -o.F F ) ) ) with typecode |-
29	17 28	pm2.61i	Could not format Rel dom ( 2nd ` ( P -o.F F ) ) : No typesetting found for |- Rel dom ( 2nd ` ( P -o.F F ) ) with typecode |-