Metamath Proof Explorer

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 ⊢ F : A ⟶ B
f0cl.2 ⊢ ∅ ∈ B
Assertion f0cli ⊢ F ⁡ C ∈ B

Proof

Step Hyp Ref Expression
1 f0cl.1 ⊢ F : A ⟶ B
2 f0cl.2 ⊢ ∅ ∈ B
3 1 ffvelrni ⊢ C ∈ A → F ⁡ C ∈ B
4 1 fdmi ⊢ dom ⁡ F = A
5 4 eleq2i ⊢ C ∈ dom ⁡ F ↔ C ∈ A
6 ndmfv ⊢ ¬ C ∈ dom ⁡ F → F ⁡ C = ∅
7 6 2 eqeltrdi ⊢ ¬ C ∈ dom ⁡ F → F ⁡ C ∈ B
8 5 7 sylnbir ⊢ ¬ C ∈ A → F ⁡ C ∈ B
9 3 8 pm2.61i ⊢ F ⁡ C ∈ B