This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐹 : 𝐴 ⟶ ∅ ↔ ( 𝐹 = ∅ ∧ 𝐴 = ∅ ) )

Proof

Step Hyp Ref Expression
1 ffun ⊢ ( 𝐹 : 𝐴 ⟶ ∅ → Fun 𝐹 )
2 frn ⊢ ( 𝐹 : 𝐴 ⟶ ∅ → ran 𝐹 ⊆ ∅ )
3 ss0 ⊢ ( ran 𝐹 ⊆ ∅ → ran 𝐹 = ∅ )
4 2 3 syl ⊢ ( 𝐹 : 𝐴 ⟶ ∅ → ran 𝐹 = ∅ )
5 dm0rn0 ⊢ ( dom 𝐹 = ∅ ↔ ran 𝐹 = ∅ )
6 4 5 sylibr ⊢ ( 𝐹 : 𝐴 ⟶ ∅ → dom 𝐹 = ∅ )
7 df-fn ⊢ ( 𝐹 Fn ∅ ↔ ( Fun 𝐹 ∧ dom 𝐹 = ∅ ) )
8 1 6 7 sylanbrc ⊢ ( 𝐹 : 𝐴 ⟶ ∅ → 𝐹 Fn ∅ )
9 fn0 ⊢ ( 𝐹 Fn ∅ ↔ 𝐹 = ∅ )
10 8 9 sylib ⊢ ( 𝐹 : 𝐴 ⟶ ∅ → 𝐹 = ∅ )
11 fdm ⊢ ( 𝐹 : 𝐴 ⟶ ∅ → dom 𝐹 = 𝐴 )
12 11 6 eqtr3d ⊢ ( 𝐹 : 𝐴 ⟶ ∅ → 𝐴 = ∅ )
13 10 12 jca ⊢ ( 𝐹 : 𝐴 ⟶ ∅ → ( 𝐹 = ∅ ∧ 𝐴 = ∅ ) )
14 f0 ⊢ ∅ : ∅ ⟶ ∅
15 feq1 ⊢ ( 𝐹 = ∅ → ( 𝐹 : 𝐴 ⟶ ∅ ↔ ∅ : 𝐴 ⟶ ∅ ) )
16 feq2 ⊢ ( 𝐴 = ∅ → ( ∅ : 𝐴 ⟶ ∅ ↔ ∅ : ∅ ⟶ ∅ ) )
17 15 16 sylan9bb ⊢ ( ( 𝐹 = ∅ ∧ 𝐴 = ∅ ) → ( 𝐹 : 𝐴 ⟶ ∅ ↔ ∅ : ∅ ⟶ ∅ ) )
18 14 17 mpbiri ⊢ ( ( 𝐹 = ∅ ∧ 𝐴 = ∅ ) → 𝐹 : 𝐴 ⟶ ∅ )
19 13 18 impbii ⊢ ( 𝐹 : 𝐴 ⟶ ∅ ↔ ( 𝐹 = ∅ ∧ 𝐴 = ∅ ) )