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\ne \varnothing \to {\varnothing }^A=\varnothing$$

Proof

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