Metamath Proof Explorer

Theorem mapdom2

Description: Order-preserving property of set exponentiation. Theorem 6L(d) of Enderton p. 149. (Contributed by NM, 23-Sep-2004) (Revised by Mario Carneiro, 30-Apr-2015)

Ref Expression
Assertion mapdom2 
|- ( ( A ~<_ B /\ -. ( A = (/) /\ C = (/) ) ) -> ( C ^m A ) ~<_ ( C ^m B ) )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( ( ( A ~<_ B /\ C e. _V ) /\ -. ( A = (/) /\ C = (/) ) ) /\ C = (/) ) -> C = (/) )
2 1 oveq1d 
 |-  ( ( ( ( A ~<_ B /\ C e. _V ) /\ -. ( A = (/) /\ C = (/) ) ) /\ C = (/) ) -> ( C ^m A ) = ( (/) ^m A ) )
3 simplr 
 |-  ( ( ( ( A ~<_ B /\ C e. _V ) /\ -. ( A = (/) /\ C = (/) ) ) /\ C = (/) ) -> -. ( A = (/) /\ C = (/) ) )
4 idd 
 |-  ( ( ( ( A ~<_ B /\ C e. _V ) /\ -. ( A = (/) /\ C = (/) ) ) /\ C = (/) ) -> ( A = (/) -> A = (/) ) )
5 4 1 jctird 
 |-  ( ( ( ( A ~<_ B /\ C e. _V ) /\ -. ( A = (/) /\ C = (/) ) ) /\ C = (/) ) -> ( A = (/) -> ( A = (/) /\ C = (/) ) ) )
6 3 5 mtod 
 |-  ( ( ( ( A ~<_ B /\ C e. _V ) /\ -. ( A = (/) /\ C = (/) ) ) /\ C = (/) ) -> -. A = (/) )
7 6 neqned 
 |-  ( ( ( ( A ~<_ B /\ C e. _V ) /\ -. ( A = (/) /\ C = (/) ) ) /\ C = (/) ) -> A =/= (/) )
8 map0b 
 |-  ( A =/= (/) -> ( (/) ^m A ) = (/) )
9 7 8 syl 
 |-  ( ( ( ( A ~<_ B /\ C e. _V ) /\ -. ( A = (/) /\ C = (/) ) ) /\ C = (/) ) -> ( (/) ^m A ) = (/) )
10 2 9 eqtrd 
 |-  ( ( ( ( A ~<_ B /\ C e. _V ) /\ -. ( A = (/) /\ C = (/) ) ) /\ C = (/) ) -> ( C ^m A ) = (/) )
11 ovex 
 |-  ( C ^m B ) e. _V
12 11 0dom 
 |-  (/) ~<_ ( C ^m B )
13 10 12 eqbrtrdi 
 |-  ( ( ( ( A ~<_ B /\ C e. _V ) /\ -. ( A = (/) /\ C = (/) ) ) /\ C = (/) ) -> ( C ^m A ) ~<_ ( C ^m B ) )
14 simpll 
 |-  ( ( ( A ~<_ B /\ C e. _V ) /\ C =/= (/) ) -> A ~<_ B )
15 reldom 
 |-  Rel ~<_
16 15 brrelex2i 
 |-  ( A ~<_ B -> B e. _V )
17 16 ad2antrr 
 |-  ( ( ( A ~<_ B /\ C e. _V ) /\ C =/= (/) ) -> B e. _V )
18 domeng 
 |-  ( B e. _V -> ( A ~<_ B <-> E. x ( A ~~ x /\ x C_ B ) ) )
19 17 18 syl 
 |-  ( ( ( A ~<_ B /\ C e. _V ) /\ C =/= (/) ) -> ( A ~<_ B <-> E. x ( A ~~ x /\ x C_ B ) ) )
20 14 19 mpbid 
 |-  ( ( ( A ~<_ B /\ C e. _V ) /\ C =/= (/) ) -> E. x ( A ~~ x /\ x C_ B ) )
21 enrefg 
 |-  ( C e. _V -> C ~~ C )
22 21 ad2antlr 
 |-  ( ( ( A ~<_ B /\ C e. _V ) /\ ( C =/= (/) /\ ( A ~~ x /\ x C_ B ) ) ) -> C ~~ C )
23 simprrl 
 |-  ( ( ( A ~<_ B /\ C e. _V ) /\ ( C =/= (/) /\ ( A ~~ x /\ x C_ B ) ) ) -> A ~~ x )
24 mapen 
 |-  ( ( C ~~ C /\ A ~~ x ) -> ( C ^m A ) ~~ ( C ^m x ) )
25 22 23 24 syl2anc 
 |-  ( ( ( A ~<_ B /\ C e. _V ) /\ ( C =/= (/) /\ ( A ~~ x /\ x C_ B ) ) ) -> ( C ^m A ) ~~ ( C ^m x ) )
26 ovexd 
 |-  ( ( ( A ~<_ B /\ C e. _V ) /\ ( C =/= (/) /\ ( A ~~ x /\ x C_ B ) ) ) -> ( C ^m x ) e. _V )
27 ovexd 
 |-  ( ( ( A ~<_ B /\ C e. _V ) /\ ( C =/= (/) /\ ( A ~~ x /\ x C_ B ) ) ) -> ( C ^m ( B \ x ) ) e. _V )
28 simprl 
 |-  ( ( ( A ~<_ B /\ C e. _V ) /\ ( C =/= (/) /\ ( A ~~ x /\ x C_ B ) ) ) -> C =/= (/) )
29 simplr 
 |-  ( ( ( A ~<_ B /\ C e. _V ) /\ ( C =/= (/) /\ ( A ~~ x /\ x C_ B ) ) ) -> C e. _V )
30 16 ad2antrr 
 |-  ( ( ( A ~<_ B /\ C e. _V ) /\ ( C =/= (/) /\ ( A ~~ x /\ x C_ B ) ) ) -> B e. _V )
31 30 difexd 
 |-  ( ( ( A ~<_ B /\ C e. _V ) /\ ( C =/= (/) /\ ( A ~~ x /\ x C_ B ) ) ) -> ( B \ x ) e. _V )
32 map0g 
 |-  ( ( C e. _V /\ ( B \ x ) e. _V ) -> ( ( C ^m ( B \ x ) ) = (/) <-> ( C = (/) /\ ( B \ x ) =/= (/) ) ) )
33 simpl 
 |-  ( ( C = (/) /\ ( B \ x ) =/= (/) ) -> C = (/) )
34 32 33 biimtrdi 
 |-  ( ( C e. _V /\ ( B \ x ) e. _V ) -> ( ( C ^m ( B \ x ) ) = (/) -> C = (/) ) )
35 34 necon3d 
 |-  ( ( C e. _V /\ ( B \ x ) e. _V ) -> ( C =/= (/) -> ( C ^m ( B \ x ) ) =/= (/) ) )
36 29 31 35 syl2anc 
 |-  ( ( ( A ~<_ B /\ C e. _V ) /\ ( C =/= (/) /\ ( A ~~ x /\ x C_ B ) ) ) -> ( C =/= (/) -> ( C ^m ( B \ x ) ) =/= (/) ) )
37 28 36 mpd 
 |-  ( ( ( A ~<_ B /\ C e. _V ) /\ ( C =/= (/) /\ ( A ~~ x /\ x C_ B ) ) ) -> ( C ^m ( B \ x ) ) =/= (/) )
38 xpdom3 
 |-  ( ( ( C ^m x ) e. _V /\ ( C ^m ( B \ x ) ) e. _V /\ ( C ^m ( B \ x ) ) =/= (/) ) -> ( C ^m x ) ~<_ ( ( C ^m x ) X. ( C ^m ( B \ x ) ) ) )
39 26 27 37 38 syl3anc 
 |-  ( ( ( A ~<_ B /\ C e. _V ) /\ ( C =/= (/) /\ ( A ~~ x /\ x C_ B ) ) ) -> ( C ^m x ) ~<_ ( ( C ^m x ) X. ( C ^m ( B \ x ) ) ) )
40 vex 
 |-  x e. _V
41 40 a1i 
 |-  ( ( ( A ~<_ B /\ C e. _V ) /\ ( C =/= (/) /\ ( A ~~ x /\ x C_ B ) ) ) -> x e. _V )
42 disjdif 
 |-  ( x i^i ( B \ x ) ) = (/)
43 42 a1i 
 |-  ( ( ( A ~<_ B /\ C e. _V ) /\ ( C =/= (/) /\ ( A ~~ x /\ x C_ B ) ) ) -> ( x i^i ( B \ x ) ) = (/) )
44 mapunen 
 |-  ( ( ( x e. _V /\ ( B \ x ) e. _V /\ C e. _V ) /\ ( x i^i ( B \ x ) ) = (/) ) -> ( C ^m ( x u. ( B \ x ) ) ) ~~ ( ( C ^m x ) X. ( C ^m ( B \ x ) ) ) )
45 41 31 29 43 44 syl31anc 
 |-  ( ( ( A ~<_ B /\ C e. _V ) /\ ( C =/= (/) /\ ( A ~~ x /\ x C_ B ) ) ) -> ( C ^m ( x u. ( B \ x ) ) ) ~~ ( ( C ^m x ) X. ( C ^m ( B \ x ) ) ) )
46 45 ensymd 
 |-  ( ( ( A ~<_ B /\ C e. _V ) /\ ( C =/= (/) /\ ( A ~~ x /\ x C_ B ) ) ) -> ( ( C ^m x ) X. ( C ^m ( B \ x ) ) ) ~~ ( C ^m ( x u. ( B \ x ) ) ) )
47 simprrr 
 |-  ( ( ( A ~<_ B /\ C e. _V ) /\ ( C =/= (/) /\ ( A ~~ x /\ x C_ B ) ) ) -> x C_ B )
48 undif 
 |-  ( x C_ B <-> ( x u. ( B \ x ) ) = B )
49 47 48 sylib 
 |-  ( ( ( A ~<_ B /\ C e. _V ) /\ ( C =/= (/) /\ ( A ~~ x /\ x C_ B ) ) ) -> ( x u. ( B \ x ) ) = B )
50 49 oveq2d 
 |-  ( ( ( A ~<_ B /\ C e. _V ) /\ ( C =/= (/) /\ ( A ~~ x /\ x C_ B ) ) ) -> ( C ^m ( x u. ( B \ x ) ) ) = ( C ^m B ) )
51 46 50 breqtrd 
 |-  ( ( ( A ~<_ B /\ C e. _V ) /\ ( C =/= (/) /\ ( A ~~ x /\ x C_ B ) ) ) -> ( ( C ^m x ) X. ( C ^m ( B \ x ) ) ) ~~ ( C ^m B ) )
52 domentr 
 |-  ( ( ( C ^m x ) ~<_ ( ( C ^m x ) X. ( C ^m ( B \ x ) ) ) /\ ( ( C ^m x ) X. ( C ^m ( B \ x ) ) ) ~~ ( C ^m B ) ) -> ( C ^m x ) ~<_ ( C ^m B ) )
53 39 51 52 syl2anc 
 |-  ( ( ( A ~<_ B /\ C e. _V ) /\ ( C =/= (/) /\ ( A ~~ x /\ x C_ B ) ) ) -> ( C ^m x ) ~<_ ( C ^m B ) )
54 endomtr 
 |-  ( ( ( C ^m A ) ~~ ( C ^m x ) /\ ( C ^m x ) ~<_ ( C ^m B ) ) -> ( C ^m A ) ~<_ ( C ^m B ) )
55 25 53 54 syl2anc 
 |-  ( ( ( A ~<_ B /\ C e. _V ) /\ ( C =/= (/) /\ ( A ~~ x /\ x C_ B ) ) ) -> ( C ^m A ) ~<_ ( C ^m B ) )
56 55 expr 
 |-  ( ( ( A ~<_ B /\ C e. _V ) /\ C =/= (/) ) -> ( ( A ~~ x /\ x C_ B ) -> ( C ^m A ) ~<_ ( C ^m B ) ) )
57 56 exlimdv 
 |-  ( ( ( A ~<_ B /\ C e. _V ) /\ C =/= (/) ) -> ( E. x ( A ~~ x /\ x C_ B ) -> ( C ^m A ) ~<_ ( C ^m B ) ) )
58 20 57 mpd 
 |-  ( ( ( A ~<_ B /\ C e. _V ) /\ C =/= (/) ) -> ( C ^m A ) ~<_ ( C ^m B ) )
59 58 adantlr 
 |-  ( ( ( ( A ~<_ B /\ C e. _V ) /\ -. ( A = (/) /\ C = (/) ) ) /\ C =/= (/) ) -> ( C ^m A ) ~<_ ( C ^m B ) )
60 13 59 pm2.61dane 
 |-  ( ( ( A ~<_ B /\ C e. _V ) /\ -. ( A = (/) /\ C = (/) ) ) -> ( C ^m A ) ~<_ ( C ^m B ) )
61 60 an32s 
 |-  ( ( ( A ~<_ B /\ -. ( A = (/) /\ C = (/) ) ) /\ C e. _V ) -> ( C ^m A ) ~<_ ( C ^m B ) )
62 61 ex 
 |-  ( ( A ~<_ B /\ -. ( A = (/) /\ C = (/) ) ) -> ( C e. _V -> ( C ^m A ) ~<_ ( C ^m B ) ) )
63 reldmmap 
 |-  Rel dom ^m
64 63 ovprc1 
 |-  ( -. C e. _V -> ( C ^m A ) = (/) )
65 64 12 eqbrtrdi 
 |-  ( -. C e. _V -> ( C ^m A ) ~<_ ( C ^m B ) )
66 62 65 pm2.61d1 
 |-  ( ( A ~<_ B /\ -. ( A = (/) /\ C = (/) ) ) -> ( C ^m A ) ~<_ ( C ^m B ) )