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