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

Metamath Proof Explorer

Theorem mapdom3

Description: Set exponentiation dominates the base. (Contributed by Mario Carneiro, 30-Apr-2015) (Proof shortened by AV, 17-Jul-2022)

Ref Expression
Assertion mapdom3 ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐵 ≠ ∅ ) → 𝐴 ≼ ( 𝐴 ↑m 𝐵 ) )

Proof

Step Hyp Ref Expression
1 n0 ⊢ ( 𝐵 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝐵 )
2 simp1 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝑥 ∈ 𝐵 ) → 𝐴 ∈ 𝑉 )
3 simp3 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
4 2 3 mapsnend ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝑥 ∈ 𝐵 ) → ( 𝐴 ↑m { 𝑥 } ) ≈ 𝐴 )
5 4 ensymd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝑥 ∈ 𝐵 ) → 𝐴 ≈ ( 𝐴 ↑m { 𝑥 } ) )
6 simp2 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝑥 ∈ 𝐵 ) → 𝐵 ∈ 𝑊 )
7 3 snssd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝑥 ∈ 𝐵 ) → { 𝑥 } ⊆ 𝐵 )
8 ssdomg ⊢ ( 𝐵 ∈ 𝑊 → ( { 𝑥 } ⊆ 𝐵 → { 𝑥 } ≼ 𝐵 ) )
9 6 7 8 sylc ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝑥 ∈ 𝐵 ) → { 𝑥 } ≼ 𝐵 )
10 vex ⊢ 𝑥 ∈ V
11 10 snnz ⊢ { 𝑥 } ≠ ∅
12 simpl ⊢ ( ( { 𝑥 } = ∅ ∧ 𝐴 = ∅ ) → { 𝑥 } = ∅ )
13 12 necon3ai ⊢ ( { 𝑥 } ≠ ∅ → ¬ ( { 𝑥 } = ∅ ∧ 𝐴 = ∅ ) )
14 11 13 ax-mp ⊢ ¬ ( { 𝑥 } = ∅ ∧ 𝐴 = ∅ )
15 mapdom2 ⊢ ( ( { 𝑥 } ≼ 𝐵 ∧ ¬ ( { 𝑥 } = ∅ ∧ 𝐴 = ∅ ) ) → ( 𝐴 ↑m { 𝑥 } ) ≼ ( 𝐴 ↑m 𝐵 ) )
16 9 14 15 sylancl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝑥 ∈ 𝐵 ) → ( 𝐴 ↑m { 𝑥 } ) ≼ ( 𝐴 ↑m 𝐵 ) )
17 endomtr ⊢ ( ( 𝐴 ≈ ( 𝐴 ↑m { 𝑥 } ) ∧ ( 𝐴 ↑m { 𝑥 } ) ≼ ( 𝐴 ↑m 𝐵 ) ) → 𝐴 ≼ ( 𝐴 ↑m 𝐵 ) )
18 5 16 17 syl2anc ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝑥 ∈ 𝐵 ) → 𝐴 ≼ ( 𝐴 ↑m 𝐵 ) )
19 18 3expia ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝑥 ∈ 𝐵 → 𝐴 ≼ ( 𝐴 ↑m 𝐵 ) ) )
20 19 exlimdv ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ∃ 𝑥 𝑥 ∈ 𝐵 → 𝐴 ≼ ( 𝐴 ↑m 𝐵 ) ) )
21 1 20 biimtrid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐵 ≠ ∅ → 𝐴 ≼ ( 𝐴 ↑m 𝐵 ) ) )
22 21 3impia ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐵 ≠ ∅ ) → 𝐴 ≼ ( 𝐴 ↑m 𝐵 ) )