Theorem reldmprcof1

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

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

Proof

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