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 
|- ( ( A e. V /\ B e. W /\ B =/= (/) ) -> A ~<_ ( A ^m B ) )

Proof

Step Hyp Ref Expression
1 n0 
 |-  ( B =/= (/) <-> E. x x e. B )
2 simp1 
 |-  ( ( A e. V /\ B e. W /\ x e. B ) -> A e. V )
3 simp3 
 |-  ( ( A e. V /\ B e. W /\ x e. B ) -> x e. B )
4 2 3 mapsnend 
 |-  ( ( A e. V /\ B e. W /\ x e. B ) -> ( A ^m { x } ) ~~ A )
5 4 ensymd 
 |-  ( ( A e. V /\ B e. W /\ x e. B ) -> A ~~ ( A ^m { x } ) )
6 simp2 
 |-  ( ( A e. V /\ B e. W /\ x e. B ) -> B e. W )
7 3 snssd 
 |-  ( ( A e. V /\ B e. W /\ x e. B ) -> { x } C_ B )
8 ssdomg 
 |-  ( B e. W -> ( { x } C_ B -> { x } ~<_ B ) )
9 6 7 8 sylc 
 |-  ( ( A e. V /\ B e. W /\ x e. B ) -> { x } ~<_ B )
10 vex 
 |-  x e. _V
11 10 snnz 
 |-  { x } =/= (/)
12 simpl 
 |-  ( ( { x } = (/) /\ A = (/) ) -> { x } = (/) )
13 12 necon3ai 
 |-  ( { x } =/= (/) -> -. ( { x } = (/) /\ A = (/) ) )
14 11 13 ax-mp 
 |-  -. ( { x } = (/) /\ A = (/) )
15 mapdom2 
 |-  ( ( { x } ~<_ B /\ -. ( { x } = (/) /\ A = (/) ) ) -> ( A ^m { x } ) ~<_ ( A ^m B ) )
16 9 14 15 sylancl 
 |-  ( ( A e. V /\ B e. W /\ x e. B ) -> ( A ^m { x } ) ~<_ ( A ^m B ) )
17 endomtr 
 |-  ( ( A ~~ ( A ^m { x } ) /\ ( A ^m { x } ) ~<_ ( A ^m B ) ) -> A ~<_ ( A ^m B ) )
18 5 16 17 syl2anc 
 |-  ( ( A e. V /\ B e. W /\ x e. B ) -> A ~<_ ( A ^m B ) )
19 18 3expia 
 |-  ( ( A e. V /\ B e. W ) -> ( x e. B -> A ~<_ ( A ^m B ) ) )
20 19 exlimdv 
 |-  ( ( A e. V /\ B e. W ) -> ( E. x x e. B -> A ~<_ ( A ^m B ) ) )
21 1 20 biimtrid 
 |-  ( ( A e. V /\ B e. W ) -> ( B =/= (/) -> A ~<_ ( A ^m B ) ) )
22 21 3impia 
 |-  ( ( A e. V /\ B e. W /\ B =/= (/) ) -> A ~<_ ( A ^m B ) )