Theorem of0r

Description: Function operation with the empty function. (Contributed by Thierry Arnoux, 27-May-2025)

	Ref	Expression
Assertion	of0r	|- ( F oF R (/) ) = (/)

Proof

Step	Hyp	Ref	Expression
1		df-of	|- oF R = ( f e. _V , g e. _V |-> ( x e. ( dom f i^i dom g ) |-> ( ( f ` x ) R ( g ` x ) ) ) )
2	1	a1i	|- ( F e. _V -> oF R = ( f e. _V , g e. _V |-> ( x e. ( dom f i^i dom g ) |-> ( ( f ` x ) R ( g ` x ) ) ) ) )
3		dmeq	|- ( f = F -> dom f = dom F )
4		dmeq	|- ( g = (/) -> dom g = dom (/) )
5	3 4	ineqan12d	|- ( ( f = F /\ g = (/) ) -> ( dom f i^i dom g ) = ( dom F i^i dom (/) ) )
6	5	mpteq1d	|- ( ( f = F /\ g = (/) ) -> ( x e. ( dom f i^i dom g ) |-> ( ( f ` x ) R ( g ` x ) ) ) = ( x e. ( dom F i^i dom (/) ) |-> ( ( f ` x ) R ( g ` x ) ) ) )
7	6	adantl	|- ( ( F e. _V /\ ( f = F /\ g = (/) ) ) -> ( x e. ( dom f i^i dom g ) |-> ( ( f ` x ) R ( g ` x ) ) ) = ( x e. ( dom F i^i dom (/) ) |-> ( ( f ` x ) R ( g ` x ) ) ) )
8		dm0	|- dom (/) = (/)
9	8	ineq2i	|- ( dom F i^i dom (/) ) = ( dom F i^i (/) )
10		in0	|- ( dom F i^i (/) ) = (/)
11	9 10	eqtri	|- ( dom F i^i dom (/) ) = (/)
12	11	a1i	|- ( ( F e. _V /\ ( f = F /\ g = (/) ) ) -> ( dom F i^i dom (/) ) = (/) )
13	12	mpteq1d	|- ( ( F e. _V /\ ( f = F /\ g = (/) ) ) -> ( x e. ( dom F i^i dom (/) ) |-> ( ( f ` x ) R ( g ` x ) ) ) = ( x e. (/) |-> ( ( f ` x ) R ( g ` x ) ) ) )
14		mpt0	|- ( x e. (/) |-> ( ( f ` x ) R ( g ` x ) ) ) = (/)
15	14	a1i	|- ( ( F e. _V /\ ( f = F /\ g = (/) ) ) -> ( x e. (/) |-> ( ( f ` x ) R ( g ` x ) ) ) = (/) )
16	7 13 15	3eqtrd	|- ( ( F e. _V /\ ( f = F /\ g = (/) ) ) -> ( x e. ( dom f i^i dom g ) |-> ( ( f ` x ) R ( g ` x ) ) ) = (/) )
17		id	|- ( F e. _V -> F e. _V )
18		0ex	|- (/) e. _V
19	18	a1i	|- ( F e. _V -> (/) e. _V )
20	2 16 17 19 19	ovmpod	|- ( F e. _V -> ( F oF R (/) ) = (/) )
21	1	reldmmpo	|- Rel dom oF R
22	21	ovprc1	|- ( -. F e. _V -> ( F oF R (/) ) = (/) )
23	20 22	pm2.61i	|- ( F oF R (/) ) = (/)