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

Metamath Proof Explorer

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	$⊢ φ \to F : A ⟶ B$
	Assertion	f002	$⊢ φ \to (B = \emptyset \to A = \emptyset)$

Step	Hyp	Ref	Expression
1		f002.1	$⊢ φ \to F : A ⟶ B$
2		feq3	$⊢ B = \emptyset \to (F : A ⟶ B \leftrightarrow F : A ⟶ \emptyset)$
3		f00	$⊢ F : A ⟶ \emptyset \leftrightarrow (F = \emptyset \land A = \emptyset)$
4	3	simprbi	$⊢ F : A ⟶ \emptyset \to A = \emptyset$
5	2 4	biimtrdi	$⊢ B = \emptyset \to (F : A ⟶ B \to A = \emptyset)$
6	1 5	syl5com	$⊢ φ \to (B = \emptyset \to A = \emptyset)$