map0cor

Description: A function exists iff an empty codomain is accompanied with an empty domain. (Contributed by Zhi Wang, 1-Oct-2024)

	Ref	Expression
Hypotheses	map0cor.1	$⊢ φ \to A \in V$
	map0cor.2	$⊢ φ \to B \in W$
Assertion	map0cor	$⊢ φ \to ((B = \emptyset \to A = \emptyset) \leftrightarrow \exists f f : A ⟶ B)$

Step	Hyp	Ref	Expression
1		map0cor.1	$⊢ φ \to A \in V$
2		map0cor.2	$⊢ φ \to B \in W$
3		biid	$⊢ A \neq \emptyset \leftrightarrow A \neq \emptyset$
4	3	necon2bbii	$⊢ A = \emptyset \leftrightarrow \neg A \neq \emptyset$
5	4	imbi2i	$⊢ (B = \emptyset \to A = \emptyset) \leftrightarrow (B = \emptyset \to \neg A \neq \emptyset)$
6		imnan	$⊢ (B = \emptyset \to \neg A \neq \emptyset) \leftrightarrow \neg (B = \emptyset \land A \neq \emptyset)$
7	5 6	bitri	$⊢ (B = \emptyset \to A = \emptyset) \leftrightarrow \neg (B = \emptyset \land A \neq \emptyset)$
8		map0g	$⊢ (B \in W \land A \in V) \to (B^{A} = \emptyset \leftrightarrow (B = \emptyset \land A \neq \emptyset))$
9	8	notbid	$⊢ (B \in W \land A \in V) \to (\neg B^{A} = \emptyset \leftrightarrow \neg (B = \emptyset \land A \neq \emptyset))$
10	7 9	bitr4id	$⊢ (B \in W \land A \in V) \to ((B = \emptyset \to A = \emptyset) \leftrightarrow \neg B^{A} = \emptyset)$
11		neq0	$⊢ \neg B^{A} = \emptyset \leftrightarrow \exists f f \in (B^{A})$
12	11	a1i	$⊢ (B \in W \land A \in V) \to (\neg B^{A} = \emptyset \leftrightarrow \exists f f \in (B^{A}))$
13		elmapg	$⊢ (B \in W \land A \in V) \to (f \in (B^{A}) \leftrightarrow f : A ⟶ B)$
14	13	exbidv	$⊢ (B \in W \land A \in V) \to (\exists f f \in (B^{A}) \leftrightarrow \exists f f : A ⟶ B)$
15	10 12 14	3bitrd	$⊢ (B \in W \land A \in V) \to ((B = \emptyset \to A = \emptyset) \leftrightarrow \exists f f : A ⟶ B)$
16	2 1 15	syl2anc	$⊢ φ \to ((B = \emptyset \to A = \emptyset) \leftrightarrow \exists f f : A ⟶ B)$

Metamath Proof Explorer