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

Metamath Proof Explorer

Theorem map0b

Description: Set exponentiation with an empty base is the empty set, provided the exponent is nonempty. Theorem 96 of Suppes p. 89. (Contributed by NM, 10-Dec-2003) (Revised by Mario Carneiro, 26-Apr-2015)

		Ref	Expression
	Assertion	map0b	$⊢ A \neq \emptyset \to \emptyset^{A} = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		elmapi	$⊢ f \in (\emptyset^{A}) \to f : A ⟶ \emptyset$
2		fdm	$⊢ f : A ⟶ \emptyset \to dom f = A$
3		frn	$⊢ f : A ⟶ \emptyset \to ran f \subseteq \emptyset$
4		ss0	$⊢ ran f \subseteq \emptyset \to ran f = \emptyset$
5	3 4	syl	$⊢ f : A ⟶ \emptyset \to ran f = \emptyset$
6		dm0rn0	$⊢ dom f = \emptyset \leftrightarrow ran f = \emptyset$
7	5 6	sylibr	$⊢ f : A ⟶ \emptyset \to dom f = \emptyset$
8	2 7	eqtr3d	$⊢ f : A ⟶ \emptyset \to A = \emptyset$
9	1 8	syl	$⊢ f \in (\emptyset^{A}) \to A = \emptyset$
10	9	necon3ai	$⊢ A \neq \emptyset \to \neg f \in (\emptyset^{A})$
11	10	eq0rdv	$⊢ A \neq \emptyset \to \emptyset^{A} = \emptyset$