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	⊢ ( 𝐴 ≠ ∅ → ( ∅ ↑m 𝐴 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		elmapi	⊢ ( 𝑓 ∈ ( ∅ ↑m 𝐴 ) → 𝑓 : 𝐴 ⟶ ∅ )
2		fdm	⊢ ( 𝑓 : 𝐴 ⟶ ∅ → dom 𝑓 = 𝐴 )
3		frn	⊢ ( 𝑓 : 𝐴 ⟶ ∅ → ran 𝑓 ⊆ ∅ )
4		ss0	⊢ ( ran 𝑓 ⊆ ∅ → ran 𝑓 = ∅ )
5	3 4	syl	⊢ ( 𝑓 : 𝐴 ⟶ ∅ → ran 𝑓 = ∅ )
6		dm0rn0	⊢ ( dom 𝑓 = ∅ ↔ ran 𝑓 = ∅ )
7	5 6	sylibr	⊢ ( 𝑓 : 𝐴 ⟶ ∅ → dom 𝑓 = ∅ )
8	2 7	eqtr3d	⊢ ( 𝑓 : 𝐴 ⟶ ∅ → 𝐴 = ∅ )
9	1 8	syl	⊢ ( 𝑓 ∈ ( ∅ ↑m 𝐴 ) → 𝐴 = ∅ )
10	9	necon3ai	⊢ ( 𝐴 ≠ ∅ → ¬ 𝑓 ∈ ( ∅ ↑m 𝐴 ) )
11	10	eq0rdv	⊢ ( 𝐴 ≠ ∅ → ( ∅ ↑m 𝐴 ) = ∅ )