# Metamath Proof Explorer

## Theorem f00

Description: A class is a function with empty codomain iff it and its domain are empty. (Contributed by NM, 10-Dec-2003)

Ref Expression
Assertion f00 ${⊢}{F}:{A}⟶\varnothing ↔\left({F}=\varnothing \wedge {A}=\varnothing \right)$

### Proof

Step Hyp Ref Expression
1 ffun ${⊢}{F}:{A}⟶\varnothing \to \mathrm{Fun}{F}$
2 frn ${⊢}{F}:{A}⟶\varnothing \to \mathrm{ran}{F}\subseteq \varnothing$
3 ss0 ${⊢}\mathrm{ran}{F}\subseteq \varnothing \to \mathrm{ran}{F}=\varnothing$
4 2 3 syl ${⊢}{F}:{A}⟶\varnothing \to \mathrm{ran}{F}=\varnothing$
5 dm0rn0 ${⊢}\mathrm{dom}{F}=\varnothing ↔\mathrm{ran}{F}=\varnothing$
6 4 5 sylibr ${⊢}{F}:{A}⟶\varnothing \to \mathrm{dom}{F}=\varnothing$
7 df-fn ${⊢}{F}Fn\varnothing ↔\left(\mathrm{Fun}{F}\wedge \mathrm{dom}{F}=\varnothing \right)$
8 1 6 7 sylanbrc ${⊢}{F}:{A}⟶\varnothing \to {F}Fn\varnothing$
9 fn0 ${⊢}{F}Fn\varnothing ↔{F}=\varnothing$
10 8 9 sylib ${⊢}{F}:{A}⟶\varnothing \to {F}=\varnothing$
11 fdm ${⊢}{F}:{A}⟶\varnothing \to \mathrm{dom}{F}={A}$
12 11 6 eqtr3d ${⊢}{F}:{A}⟶\varnothing \to {A}=\varnothing$
13 10 12 jca ${⊢}{F}:{A}⟶\varnothing \to \left({F}=\varnothing \wedge {A}=\varnothing \right)$
14 f0 ${⊢}\varnothing :\varnothing ⟶\varnothing$
15 feq1 ${⊢}{F}=\varnothing \to \left({F}:{A}⟶\varnothing ↔\varnothing :{A}⟶\varnothing \right)$
16 feq2 ${⊢}{A}=\varnothing \to \left(\varnothing :{A}⟶\varnothing ↔\varnothing :\varnothing ⟶\varnothing \right)$
17 15 16 sylan9bb ${⊢}\left({F}=\varnothing \wedge {A}=\varnothing \right)\to \left({F}:{A}⟶\varnothing ↔\varnothing :\varnothing ⟶\varnothing \right)$
18 14 17 mpbiri ${⊢}\left({F}=\varnothing \wedge {A}=\varnothing \right)\to {F}:{A}⟶\varnothing$
19 13 18 impbii ${⊢}{F}:{A}⟶\varnothing ↔\left({F}=\varnothing \wedge {A}=\varnothing \right)$