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	|- ( ( 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	syl5bi	|- ( ( 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 ) )