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 =/= (/) -> ( (/) ^m A ) = (/) )

Proof

Step	Hyp	Ref	Expression
1		elmapi	|- ( f e. ( (/) ^m A ) -> f : A --> (/) )
2		fdm	|- ( f : A --> (/) -> dom f = A )
3		frn	|- ( f : A --> (/) -> ran f C_ (/) )
4		ss0	|- ( ran f C_ (/) -> ran f = (/) )
5	3 4	syl	|- ( f : A --> (/) -> ran f = (/) )
6		dm0rn0	|- ( dom f = (/) <-> ran f = (/) )
7	5 6	sylibr	|- ( f : A --> (/) -> dom f = (/) )
8	2 7	eqtr3d	|- ( f : A --> (/) -> A = (/) )
9	1 8	syl	|- ( f e. ( (/) ^m A ) -> A = (/) )
10	9	necon3ai	|- ( A =/= (/) -> -. f e. ( (/) ^m A ) )
11	10	eq0rdv	|- ( A =/= (/) -> ( (/) ^m A ) = (/) )