Theorem f0cli

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

	Ref	Expression
Hypotheses	f0cl.1	⊢ 𝐹 : 𝐴 ⟶ 𝐵
	f0cl.2	⊢ ∅ ∈ 𝐵
Assertion	f0cli	⊢ ( 𝐹 ‘ 𝐶 ) ∈ 𝐵

Proof

Step	Hyp	Ref	Expression
1		f0cl.1	⊢ 𝐹 : 𝐴 ⟶ 𝐵
2		f0cl.2	⊢ ∅ ∈ 𝐵
3	1	ffvelrni	⊢ ( 𝐶 ∈ 𝐴 → ( 𝐹 ‘ 𝐶 ) ∈ 𝐵 )
4	1	fdmi	⊢ dom 𝐹 = 𝐴
5	4	eleq2i	⊢ ( 𝐶 ∈ dom 𝐹 ↔ 𝐶 ∈ 𝐴 )
6		ndmfv	⊢ ( ¬ 𝐶 ∈ dom 𝐹 → ( 𝐹 ‘ 𝐶 ) = ∅ )
7	6 2	syl6eqel	⊢ ( ¬ 𝐶 ∈ dom 𝐹 → ( 𝐹 ‘ 𝐶 ) ∈ 𝐵 )
8	5 7	sylnbir	⊢ ( ¬ 𝐶 ∈ 𝐴 → ( 𝐹 ‘ 𝐶 ) ∈ 𝐵 )
9	3 8	pm2.61i	⊢ ( 𝐹 ‘ 𝐶 ) ∈ 𝐵