Theorem f0cli

Description: Unconditional closure of a function when the codomain includes the empty set. (Contributed by Mario Carneiro, 12-Sep-2013)

	Ref	Expression
Hypotheses	f0cl.1	$$⊢F:A⟶B$$
	f0cl.2	$$⊢\varnothing \in B$$
Assertion	f0cli	$$⊢F\left(C\right)\in B$$

Proof

Step	Hyp	Ref	Expression
1		f0cl.1	$$⊢F:A⟶B$$
2		f0cl.2	$$⊢\varnothing \in B$$
3	1	ffvelcdmi	$$⊢C\in A\to F\left(C\right)\in B$$
4	1	fdmi	$$⊢\mathrm{dom}F=A$$
5	4	eleq2i	$$⊢C\in \mathrm{dom}F\leftrightarrow C\in A$$
6		ndmfv	$$⊢\neg C\in \mathrm{dom}F\to F\left(C\right)=\varnothing$$
7	6 2	eqeltrdi	$$⊢\neg C\in \mathrm{dom}F\to F\left(C\right)\in B$$
8	5 7	sylnbir	$$⊢\neg C\in A\to F\left(C\right)\in B$$
9	3 8	pm2.61i	$$⊢F\left(C\right)\in B$$