Theorem map0g

Description: Set exponentiation is empty iff the base is empty and the exponent is not empty. Theorem 97 of Suppes p. 89. (Contributed by Mario Carneiro, 30-Apr-2015)

	Ref	Expression
Assertion	map0g	$$⊢\left(A\in V\wedge B\in W\right)\to \left(A^B=\varnothing \leftrightarrow \left(A=\varnothing \wedge B\ne \varnothing \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		n0	$$⊢A\ne \varnothing \leftrightarrow \exists ff\in A$$
2		fconst6g	$$⊢f\in A\to \left(B\times \left\{f\right\}\right):B⟶A$$
3		elmapg	$$⊢\left(A\in V\wedge B\in W\right)\to \left(B\times \left\{f\right\}\in \left(A^B\right)\leftrightarrow \left(B\times \left\{f\right\}\right):B⟶A\right)$$
4	2 3	imbitrrid	$$⊢\left(A\in V\wedge B\in W\right)\to \left(f\in A\to B\times \left\{f\right\}\in \left(A^B\right)\right)$$
5		ne0i	$$⊢B\times \left\{f\right\}\in \left(A^B\right)\to A^B\ne \varnothing$$
6	4 5	syl6	$$⊢\left(A\in V\wedge B\in W\right)\to \left(f\in A\to A^B\ne \varnothing \right)$$
7	6	exlimdv	$$⊢\left(A\in V\wedge B\in W\right)\to \left(\exists ff\in A\to A^B\ne \varnothing \right)$$
8	1 7	biimtrid	$$⊢\left(A\in V\wedge B\in W\right)\to \left(A\ne \varnothing \to A^B\ne \varnothing \right)$$
9	8	necon4d	$$⊢\left(A\in V\wedge B\in W\right)\to \left(A^B=\varnothing \to A=\varnothing \right)$$
10		f0	$$⊢\varnothing :\varnothing ⟶A$$
11		feq2	$$⊢B=\varnothing \to \left(\varnothing :B⟶A\leftrightarrow \varnothing :\varnothing ⟶A\right)$$
12	10 11	mpbiri	$$⊢B=\varnothing \to \varnothing :B⟶A$$
13		elmapg	$$⊢\left(A\in V\wedge B\in W\right)\to \left(\varnothing \in \left(A^B\right)\leftrightarrow \varnothing :B⟶A\right)$$
14	12 13	imbitrrid	$$⊢\left(A\in V\wedge B\in W\right)\to \left(B=\varnothing \to \varnothing \in \left(A^B\right)\right)$$
15		ne0i	$$⊢\varnothing \in \left(A^B\right)\to A^B\ne \varnothing$$
16	14 15	syl6	$$⊢\left(A\in V\wedge B\in W\right)\to \left(B=\varnothing \to A^B\ne \varnothing \right)$$
17	16	necon2d	$$⊢\left(A\in V\wedge B\in W\right)\to \left(A^B=\varnothing \to B\ne \varnothing \right)$$
18	9 17	jcad	$$⊢\left(A\in V\wedge B\in W\right)\to \left(A^B=\varnothing \to \left(A=\varnothing \wedge B\ne \varnothing \right)\right)$$
19		oveq1	$$⊢A=\varnothing \to A^B={\varnothing }^B$$
20		map0b	$$⊢B\ne \varnothing \to {\varnothing }^B=\varnothing$$
21	19 20	sylan9eq	$$⊢\left(A=\varnothing \wedge B\ne \varnothing \right)\to A^B=\varnothing$$
22	18 21	impbid1	$$⊢\left(A\in V\wedge B\in W\right)\to \left(A^B=\varnothing \leftrightarrow \left(A=\varnothing \wedge B\ne \varnothing \right)\right)$$