of0r

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

		Ref	Expression
	Assertion	of0r	$⊢ F R_{f} \emptyset = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		df-of	$⊢ \circ_{f} R = (f \in V, g \in V ⟼ (x \in (dom f \cap dom g) ⟼ f (x) R g (x)))$
2	1	a1i	$⊢ F \in V \to \circ_{f} R = (f \in V, g \in V ⟼ (x \in (dom f \cap dom g) ⟼ f (x) R g (x)))$
3		dmeq	$⊢ f = F \to dom f = dom F$
4		dmeq	$⊢ g = \emptyset \to dom g = dom \emptyset$
5	3 4	ineqan12d	$⊢ (f = F \land g = \emptyset) \to dom f \cap dom g = dom F \cap dom \emptyset$
6	5	mpteq1d	$⊢ (f = F \land g = \emptyset) \to (x \in (dom f \cap dom g) ⟼ f (x) R g (x)) = (x \in (dom F \cap dom \emptyset) ⟼ f (x) R g (x))$
7	6	adantl	$⊢ (F \in V \land (f = F \land g = \emptyset)) \to (x \in (dom f \cap dom g) ⟼ f (x) R g (x)) = (x \in (dom F \cap dom \emptyset) ⟼ f (x) R g (x))$
8		dm0	$⊢ dom \emptyset = \emptyset$
9	8	ineq2i	$⊢ dom F \cap dom \emptyset = dom F \cap \emptyset$
10		in0	$⊢ dom F \cap \emptyset = \emptyset$
11	9 10	eqtri	$⊢ dom F \cap dom \emptyset = \emptyset$
12	11	a1i	$⊢ (F \in V \land (f = F \land g = \emptyset)) \to dom F \cap dom \emptyset = \emptyset$
13	12	mpteq1d	$⊢ (F \in V \land (f = F \land g = \emptyset)) \to (x \in (dom F \cap dom \emptyset) ⟼ f (x) R g (x)) = (x \in \emptyset ⟼ f (x) R g (x))$
14		mpt0	$⊢ (x \in \emptyset ⟼ f (x) R g (x)) = \emptyset$
15	14	a1i	$⊢ (F \in V \land (f = F \land g = \emptyset)) \to (x \in \emptyset ⟼ f (x) R g (x)) = \emptyset$
16	7 13 15	3eqtrd	$⊢ (F \in V \land (f = F \land g = \emptyset)) \to (x \in (dom f \cap dom g) ⟼ f (x) R g (x)) = \emptyset$
17		id	$⊢ F \in V \to F \in V$
18		0ex	$⊢ \emptyset \in V$
19	18	a1i	$⊢ F \in V \to \emptyset \in V$
20	2 16 17 19 19	ovmpod	$⊢ F \in V \to F R_{f} \emptyset = \emptyset$
21	1	reldmmpo	$⊢ Rel dom \circ_{f} R$
22	21	ovprc1	$⊢ \neg F \in V \to F R_{f} \emptyset = \emptyset$
23	20 22	pm2.61i	$⊢ F R_{f} \emptyset = \emptyset$

Metamath Proof Explorer

Theorem of0r

Proof