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

Metamath Proof Explorer

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