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	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( 𝐴 ↑m 𝐵 ) = ∅ ↔ ( 𝐴 = ∅ ∧ 𝐵 ≠ ∅ ) ) )

Proof

Step	Hyp	Ref	Expression
1		n0	⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑓 𝑓 ∈ 𝐴 )
2		fconst6g	⊢ ( 𝑓 ∈ 𝐴 → ( 𝐵 × { 𝑓 } ) : 𝐵 ⟶ 𝐴 )
3		elmapg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( 𝐵 × { 𝑓 } ) ∈ ( 𝐴 ↑m 𝐵 ) ↔ ( 𝐵 × { 𝑓 } ) : 𝐵 ⟶ 𝐴 ) )
4	2 3	imbitrrid	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝑓 ∈ 𝐴 → ( 𝐵 × { 𝑓 } ) ∈ ( 𝐴 ↑m 𝐵 ) ) )
5		ne0i	⊢ ( ( 𝐵 × { 𝑓 } ) ∈ ( 𝐴 ↑m 𝐵 ) → ( 𝐴 ↑m 𝐵 ) ≠ ∅ )
6	4 5	syl6	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝑓 ∈ 𝐴 → ( 𝐴 ↑m 𝐵 ) ≠ ∅ ) )
7	6	exlimdv	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ∃ 𝑓 𝑓 ∈ 𝐴 → ( 𝐴 ↑m 𝐵 ) ≠ ∅ ) )
8	1 7	biimtrid	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ≠ ∅ → ( 𝐴 ↑m 𝐵 ) ≠ ∅ ) )
9	8	necon4d	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( 𝐴 ↑m 𝐵 ) = ∅ → 𝐴 = ∅ ) )
10		f0	⊢ ∅ : ∅ ⟶ 𝐴
11		feq2	⊢ ( 𝐵 = ∅ → ( ∅ : 𝐵 ⟶ 𝐴 ↔ ∅ : ∅ ⟶ 𝐴 ) )
12	10 11	mpbiri	⊢ ( 𝐵 = ∅ → ∅ : 𝐵 ⟶ 𝐴 )
13		elmapg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ∅ ∈ ( 𝐴 ↑m 𝐵 ) ↔ ∅ : 𝐵 ⟶ 𝐴 ) )
14	12 13	imbitrrid	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐵 = ∅ → ∅ ∈ ( 𝐴 ↑m 𝐵 ) ) )
15		ne0i	⊢ ( ∅ ∈ ( 𝐴 ↑m 𝐵 ) → ( 𝐴 ↑m 𝐵 ) ≠ ∅ )
16	14 15	syl6	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐵 = ∅ → ( 𝐴 ↑m 𝐵 ) ≠ ∅ ) )
17	16	necon2d	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( 𝐴 ↑m 𝐵 ) = ∅ → 𝐵 ≠ ∅ ) )
18	9 17	jcad	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( 𝐴 ↑m 𝐵 ) = ∅ → ( 𝐴 = ∅ ∧ 𝐵 ≠ ∅ ) ) )
19		oveq1	⊢ ( 𝐴 = ∅ → ( 𝐴 ↑m 𝐵 ) = ( ∅ ↑m 𝐵 ) )
20		map0b	⊢ ( 𝐵 ≠ ∅ → ( ∅ ↑m 𝐵 ) = ∅ )
21	19 20	sylan9eq	⊢ ( ( 𝐴 = ∅ ∧ 𝐵 ≠ ∅ ) → ( 𝐴 ↑m 𝐵 ) = ∅ )
22	18 21	impbid1	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( 𝐴 ↑m 𝐵 ) = ∅ ↔ ( 𝐴 = ∅ ∧ 𝐵 ≠ ∅ ) ) )