# Metamath Proof Explorer

## Theorem mapdom3

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

Ref Expression
Assertion mapdom3 ${⊢}\left({A}\in {V}\wedge {B}\in {W}\wedge {B}\ne \varnothing \right)\to {A}\preccurlyeq \left({{A}}^{{B}}\right)$

### Proof

Step Hyp Ref Expression
1 n0 ${⊢}{B}\ne \varnothing ↔\exists {x}\phantom{\rule{.4em}{0ex}}{x}\in {B}$
2 simp1 ${⊢}\left({A}\in {V}\wedge {B}\in {W}\wedge {x}\in {B}\right)\to {A}\in {V}$
3 simp3 ${⊢}\left({A}\in {V}\wedge {B}\in {W}\wedge {x}\in {B}\right)\to {x}\in {B}$
4 2 3 mapsnend ${⊢}\left({A}\in {V}\wedge {B}\in {W}\wedge {x}\in {B}\right)\to \left({{A}}^{\left\{{x}\right\}}\right)\approx {A}$
5 4 ensymd ${⊢}\left({A}\in {V}\wedge {B}\in {W}\wedge {x}\in {B}\right)\to {A}\approx \left({{A}}^{\left\{{x}\right\}}\right)$
6 simp2 ${⊢}\left({A}\in {V}\wedge {B}\in {W}\wedge {x}\in {B}\right)\to {B}\in {W}$
7 3 snssd ${⊢}\left({A}\in {V}\wedge {B}\in {W}\wedge {x}\in {B}\right)\to \left\{{x}\right\}\subseteq {B}$
8 ssdomg ${⊢}{B}\in {W}\to \left(\left\{{x}\right\}\subseteq {B}\to \left\{{x}\right\}\preccurlyeq {B}\right)$
9 6 7 8 sylc ${⊢}\left({A}\in {V}\wedge {B}\in {W}\wedge {x}\in {B}\right)\to \left\{{x}\right\}\preccurlyeq {B}$
10 vex ${⊢}{x}\in \mathrm{V}$
11 10 snnz ${⊢}\left\{{x}\right\}\ne \varnothing$
12 simpl ${⊢}\left(\left\{{x}\right\}=\varnothing \wedge {A}=\varnothing \right)\to \left\{{x}\right\}=\varnothing$
13 12 necon3ai ${⊢}\left\{{x}\right\}\ne \varnothing \to ¬\left(\left\{{x}\right\}=\varnothing \wedge {A}=\varnothing \right)$
14 11 13 ax-mp ${⊢}¬\left(\left\{{x}\right\}=\varnothing \wedge {A}=\varnothing \right)$
15 mapdom2 ${⊢}\left(\left\{{x}\right\}\preccurlyeq {B}\wedge ¬\left(\left\{{x}\right\}=\varnothing \wedge {A}=\varnothing \right)\right)\to \left({{A}}^{\left\{{x}\right\}}\right)\preccurlyeq \left({{A}}^{{B}}\right)$
16 9 14 15 sylancl ${⊢}\left({A}\in {V}\wedge {B}\in {W}\wedge {x}\in {B}\right)\to \left({{A}}^{\left\{{x}\right\}}\right)\preccurlyeq \left({{A}}^{{B}}\right)$
17 endomtr ${⊢}\left({A}\approx \left({{A}}^{\left\{{x}\right\}}\right)\wedge \left({{A}}^{\left\{{x}\right\}}\right)\preccurlyeq \left({{A}}^{{B}}\right)\right)\to {A}\preccurlyeq \left({{A}}^{{B}}\right)$
18 5 16 17 syl2anc ${⊢}\left({A}\in {V}\wedge {B}\in {W}\wedge {x}\in {B}\right)\to {A}\preccurlyeq \left({{A}}^{{B}}\right)$
19 18 3expia ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \left({x}\in {B}\to {A}\preccurlyeq \left({{A}}^{{B}}\right)\right)$
20 19 exlimdv ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}{x}\in {B}\to {A}\preccurlyeq \left({{A}}^{{B}}\right)\right)$
21 1 20 syl5bi ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \left({B}\ne \varnothing \to {A}\preccurlyeq \left({{A}}^{{B}}\right)\right)$
22 21 3impia ${⊢}\left({A}\in {V}\wedge {B}\in {W}\wedge {B}\ne \varnothing \right)\to {A}\preccurlyeq \left({{A}}^{{B}}\right)$