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 ⊢ A ∈ V ∧ B ∈ W → A B = ∅ ↔ A = ∅ ∧ B ≠ ∅

Proof

Step Hyp Ref Expression
1 n0 ⊢ A ≠ ∅ ↔ ∃ f f ∈ A
2 fconst6g ⊢ f ∈ A → B × f : B ⟶ A
3 elmapg ⊢ A ∈ V ∧ B ∈ W → B × f ∈ A B ↔ B × f : B ⟶ A
4 2 3 imbitrrid ⊢ A ∈ V ∧ B ∈ W → f ∈ A → B × f ∈ A B
5 ne0i ⊢ B × f ∈ A B → A B ≠ ∅
6 4 5 syl6 ⊢ A ∈ V ∧ B ∈ W → f ∈ A → A B ≠ ∅
7 6 exlimdv ⊢ A ∈ V ∧ B ∈ W → ∃ f f ∈ A → A B ≠ ∅
8 1 7 biimtrid ⊢ A ∈ V ∧ B ∈ W → A ≠ ∅ → A B ≠ ∅
9 8 necon4d ⊢ A ∈ V ∧ B ∈ W → A B = ∅ → A = ∅
10 f0 ⊢ ∅ : ∅ ⟶ A
11 feq2 ⊢ B = ∅ → ∅ : B ⟶ A ↔ ∅ : ∅ ⟶ A
12 10 11 mpbiri ⊢ B = ∅ → ∅ : B ⟶ A
13 elmapg ⊢ A ∈ V ∧ B ∈ W → ∅ ∈ A B ↔ ∅ : B ⟶ A
14 12 13 imbitrrid ⊢ A ∈ V ∧ B ∈ W → B = ∅ → ∅ ∈ A B
15 ne0i ⊢ ∅ ∈ A B → A B ≠ ∅
16 14 15 syl6 ⊢ A ∈ V ∧ B ∈ W → B = ∅ → A B ≠ ∅
17 16 necon2d ⊢ A ∈ V ∧ B ∈ W → A B = ∅ → B ≠ ∅
18 9 17 jcad ⊢ A ∈ V ∧ B ∈ W → A B = ∅ → A = ∅ ∧ B ≠ ∅
19 oveq1 ⊢ A = ∅ → A B = ∅ B
20 map0b ⊢ B ≠ ∅ → ∅ B = ∅
21 19 20 sylan9eq ⊢ A = ∅ ∧ B ≠ ∅ → A B = ∅
22 18 21 impbid1 ⊢ A ∈ V ∧ B ∈ W → A B = ∅ ↔ A = ∅ ∧ B ≠ ∅