This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐵 ) = ∅ ↔ ( 𝐴 = ∅ ∧ 𝐵 ≠ ∅ ) ) )