Theorem of0r

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

	Ref	Expression
Assertion	of0r	⊢ ( 𝐹 ∘f 𝑅 ∅ ) = ∅

Proof

Step	Hyp	Ref	Expression
1		df-of	⊢ ∘f 𝑅 = ( 𝑓 ∈ V , 𝑔 ∈ V ↦ ( 𝑥 ∈ ( dom 𝑓 ∩ dom 𝑔 ) ↦ ( ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) ) )
2	1	a1i	⊢ ( 𝐹 ∈ V → ∘f 𝑅 = ( 𝑓 ∈ V , 𝑔 ∈ V ↦ ( 𝑥 ∈ ( dom 𝑓 ∩ dom 𝑔 ) ↦ ( ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) ) ) )
3		dmeq	⊢ ( 𝑓 = 𝐹 → dom 𝑓 = dom 𝐹 )
4		dmeq	⊢ ( 𝑔 = ∅ → dom 𝑔 = dom ∅ )
5	3 4	ineqan12d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = ∅ ) → ( dom 𝑓 ∩ dom 𝑔 ) = ( dom 𝐹 ∩ dom ∅ ) )
6	5	mpteq1d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = ∅ ) → ( 𝑥 ∈ ( dom 𝑓 ∩ dom 𝑔 ) ↦ ( ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( dom 𝐹 ∩ dom ∅ ) ↦ ( ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) ) )
7	6	adantl	⊢ ( ( 𝐹 ∈ V ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = ∅ ) ) → ( 𝑥 ∈ ( dom 𝑓 ∩ dom 𝑔 ) ↦ ( ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( dom 𝐹 ∩ dom ∅ ) ↦ ( ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) ) )
8		dm0	⊢ dom ∅ = ∅
9	8	ineq2i	⊢ ( dom 𝐹 ∩ dom ∅ ) = ( dom 𝐹 ∩ ∅ )
10		in0	⊢ ( dom 𝐹 ∩ ∅ ) = ∅
11	9 10	eqtri	⊢ ( dom 𝐹 ∩ dom ∅ ) = ∅
12	11	a1i	⊢ ( ( 𝐹 ∈ V ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = ∅ ) ) → ( dom 𝐹 ∩ dom ∅ ) = ∅ )
13	12	mpteq1d	⊢ ( ( 𝐹 ∈ V ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = ∅ ) ) → ( 𝑥 ∈ ( dom 𝐹 ∩ dom ∅ ) ↦ ( ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ∅ ↦ ( ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) ) )
14		mpt0	⊢ ( 𝑥 ∈ ∅ ↦ ( ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) ) = ∅
15	14	a1i	⊢ ( ( 𝐹 ∈ V ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = ∅ ) ) → ( 𝑥 ∈ ∅ ↦ ( ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) ) = ∅ )
16	7 13 15	3eqtrd	⊢ ( ( 𝐹 ∈ V ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = ∅ ) ) → ( 𝑥 ∈ ( dom 𝑓 ∩ dom 𝑔 ) ↦ ( ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) ) = ∅ )
17		id	⊢ ( 𝐹 ∈ V → 𝐹 ∈ V )
18		0ex	⊢ ∅ ∈ V
19	18	a1i	⊢ ( 𝐹 ∈ V → ∅ ∈ V )
20	2 16 17 19 19	ovmpod	⊢ ( 𝐹 ∈ V → ( 𝐹 ∘f 𝑅 ∅ ) = ∅ )
21	1	reldmmpo	⊢ Rel dom ∘f 𝑅
22	21	ovprc1	⊢ ( ¬ 𝐹 ∈ V → ( 𝐹 ∘f 𝑅 ∅ ) = ∅ )
23	20 22	pm2.61i	⊢ ( 𝐹 ∘f 𝑅 ∅ ) = ∅