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