Theorem mapdom1

Description: Order-preserving property of set exponentiation. Theorem 6L(c) of Enderton p. 149. (Contributed by NM, 27-Jul-2004) (Revised by Mario Carneiro, 9-Mar-2013)

	Ref	Expression
Assertion	mapdom1	|- ( A ~<_ B -> ( A ^m C ) ~<_ ( B ^m C ) )

Proof

Step	Hyp	Ref	Expression
1		reldom	|- Rel ~<_
2	1	brrelex2i	|- ( A ~<_ B -> B e. _V )
3		domeng	|- ( B e. _V -> ( A ~<_ B <-> E. x ( A ~~ x /\ x C_ B ) ) )
4	2 3	syl	|- ( A ~<_ B -> ( A ~<_ B <-> E. x ( A ~~ x /\ x C_ B ) ) )
5	4	ibi	|- ( A ~<_ B -> E. x ( A ~~ x /\ x C_ B ) )
6	5	adantr	|- ( ( A ~<_ B /\ C e. _V ) -> E. x ( A ~~ x /\ x C_ B ) )
7		simpl	|- ( ( A ~~ x /\ x C_ B ) -> A ~~ x )
8		enrefg	|- ( C e. _V -> C ~~ C )
9	8	adantl	|- ( ( A ~<_ B /\ C e. _V ) -> C ~~ C )
10		mapen	|- ( ( A ~~ x /\ C ~~ C ) -> ( A ^m C ) ~~ ( x ^m C ) )
11	7 9 10	syl2anr	|- ( ( ( A ~<_ B /\ C e. _V ) /\ ( A ~~ x /\ x C_ B ) ) -> ( A ^m C ) ~~ ( x ^m C ) )
12		ovex	|- ( B ^m C ) e. _V
13	2	ad2antrr	|- ( ( ( A ~<_ B /\ C e. _V ) /\ ( A ~~ x /\ x C_ B ) ) -> B e. _V )
14		simprr	|- ( ( ( A ~<_ B /\ C e. _V ) /\ ( A ~~ x /\ x C_ B ) ) -> x C_ B )
15		mapss	|- ( ( B e. _V /\ x C_ B ) -> ( x ^m C ) C_ ( B ^m C ) )
16	13 14 15	syl2anc	|- ( ( ( A ~<_ B /\ C e. _V ) /\ ( A ~~ x /\ x C_ B ) ) -> ( x ^m C ) C_ ( B ^m C ) )
17		ssdomg	|- ( ( B ^m C ) e. _V -> ( ( x ^m C ) C_ ( B ^m C ) -> ( x ^m C ) ~<_ ( B ^m C ) ) )
18	12 16 17	mpsyl	|- ( ( ( A ~<_ B /\ C e. _V ) /\ ( A ~~ x /\ x C_ B ) ) -> ( x ^m C ) ~<_ ( B ^m C ) )
19		endomtr	|- ( ( ( A ^m C ) ~~ ( x ^m C ) /\ ( x ^m C ) ~<_ ( B ^m C ) ) -> ( A ^m C ) ~<_ ( B ^m C ) )
20	11 18 19	syl2anc	|- ( ( ( A ~<_ B /\ C e. _V ) /\ ( A ~~ x /\ x C_ B ) ) -> ( A ^m C ) ~<_ ( B ^m C ) )
21	6 20	exlimddv	|- ( ( A ~<_ B /\ C e. _V ) -> ( A ^m C ) ~<_ ( B ^m C ) )
22		elmapex	|- ( x e. ( A ^m C ) -> ( A e. _V /\ C e. _V ) )
23	22	simprd	|- ( x e. ( A ^m C ) -> C e. _V )
24	23	con3i	|- ( -. C e. _V -> -. x e. ( A ^m C ) )
25	24	eq0rdv	|- ( -. C e. _V -> ( A ^m C ) = (/) )
26	25	adantl	|- ( ( A ~<_ B /\ -. C e. _V ) -> ( A ^m C ) = (/) )
27	12	0dom	|- (/) ~<_ ( B ^m C )
28	26 27	eqbrtrdi	|- ( ( A ~<_ B /\ -. C e. _V ) -> ( A ^m C ) ~<_ ( B ^m C ) )
29	21 28	pm2.61dan	|- ( A ~<_ B -> ( A ^m C ) ~<_ ( B ^m C ) )