Theorem f002

Description: A function with an empty codomain must have empty domain. (Contributed by Zhi Wang, 1-Oct-2024)

	Ref	Expression
Hypothesis	f002.1	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
Assertion	f002	⊢ ( 𝜑 → ( 𝐵 = ∅ → 𝐴 = ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		f002.1	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
2		feq3	⊢ ( 𝐵 = ∅ → ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ 𝐹 : 𝐴 ⟶ ∅ ) )
3		f00	⊢ ( 𝐹 : 𝐴 ⟶ ∅ ↔ ( 𝐹 = ∅ ∧ 𝐴 = ∅ ) )
4	3	simprbi	⊢ ( 𝐹 : 𝐴 ⟶ ∅ → 𝐴 = ∅ )
5	2 4	biimtrdi	⊢ ( 𝐵 = ∅ → ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐴 = ∅ ) )
6	1 5	syl5com	⊢ ( 𝜑 → ( 𝐵 = ∅ → 𝐴 = ∅ ) )