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 𝐹 : 𝐴𝐵
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 eqeltrdi ( ¬ 𝐶 ∈ dom 𝐹 → ( 𝐹𝐶 ) ∈ 𝐵 )
8 5 7 sylnbir ( ¬ 𝐶𝐴 → ( 𝐹𝐶 ) ∈ 𝐵 )
9 3 8 pm2.61i ( 𝐹𝐶 ) ∈ 𝐵