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 difexg 
 |-  ( B e. _V -> ( B \ x ) e. _V )
32 30 31 syl 
 |-  ( ( ( A ~<_ B /\ C e. _V ) /\ ( C =/= (/) /\ ( A ~~ x /\ x C_ B ) ) ) -> ( B \ x ) e. _V )
33 map0g 
 |-  ( ( C e. _V /\ ( B \ x ) e. _V ) -> ( ( C ^m ( B \ x ) ) = (/) <-> ( C = (/) /\ ( B \ x ) =/= (/) ) ) )
34 simpl 
 |-  ( ( C = (/) /\ ( B \ x ) =/= (/) ) -> C = (/) )
35 33 34 syl6bi 
 |-  ( ( C e. _V /\ ( B \ x ) e. _V ) -> ( ( C ^m ( B \ x ) ) = (/) -> C = (/) ) )
36 35 necon3d 
 |-  ( ( C e. _V /\ ( B \ x ) e. _V ) -> ( C =/= (/) -> ( C ^m ( B \ x ) ) =/= (/) ) )
37 29 32 36 syl2anc 
 |-  ( ( ( A ~<_ B /\ C e. _V ) /\ ( C =/= (/) /\ ( A ~~ x /\ x C_ B ) ) ) -> ( C =/= (/) -> ( C ^m ( B \ x ) ) =/= (/) ) )
38 28 37 mpd 
 |-  ( ( ( A ~<_ B /\ C e. _V ) /\ ( C =/= (/) /\ ( A ~~ x /\ x C_ B ) ) ) -> ( C ^m ( B \ x ) ) =/= (/) )
39 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 ) ) ) )
40 26 27 38 39 syl3anc 
 |-  ( ( ( A ~<_ B /\ C e. _V ) /\ ( C =/= (/) /\ ( A ~~ x /\ x C_ B ) ) ) -> ( C ^m x ) ~<_ ( ( C ^m x ) X. ( C ^m ( B \ x ) ) ) )
41 vex 
 |-  x e. _V
42 41 a1i 
 |-  ( ( ( A ~<_ B /\ C e. _V ) /\ ( C =/= (/) /\ ( A ~~ x /\ x C_ B ) ) ) -> x e. _V )
43 disjdif 
 |-  ( x i^i ( B \ x ) ) = (/)
44 43 a1i 
 |-  ( ( ( A ~<_ B /\ C e. _V ) /\ ( C =/= (/) /\ ( A ~~ x /\ x C_ B ) ) ) -> ( x i^i ( B \ x ) ) = (/) )
45 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 ) ) ) )
46 42 32 29 44 45 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 ) ) ) )
47 46 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 ) ) ) )
48 simprrr 
 |-  ( ( ( A ~<_ B /\ C e. _V ) /\ ( C =/= (/) /\ ( A ~~ x /\ x C_ B ) ) ) -> x C_ B )
49 undif 
 |-  ( x C_ B <-> ( x u. ( B \ x ) ) = B )
50 48 49 sylib 
 |-  ( ( ( A ~<_ B /\ C e. _V ) /\ ( C =/= (/) /\ ( A ~~ x /\ x C_ B ) ) ) -> ( x u. ( B \ x ) ) = B )
51 50 oveq2d 
 |-  ( ( ( A ~<_ B /\ C e. _V ) /\ ( C =/= (/) /\ ( A ~~ x /\ x C_ B ) ) ) -> ( C ^m ( x u. ( B \ x ) ) ) = ( C ^m B ) )
52 47 51 breqtrd 
 |-  ( ( ( A ~<_ B /\ C e. _V ) /\ ( C =/= (/) /\ ( A ~~ x /\ x C_ B ) ) ) -> ( ( C ^m x ) X. ( C ^m ( B \ x ) ) ) ~~ ( C ^m B ) )
53 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 ) )
54 40 52 53 syl2anc 
 |-  ( ( ( A ~<_ B /\ C e. _V ) /\ ( C =/= (/) /\ ( A ~~ x /\ x C_ B ) ) ) -> ( C ^m x ) ~<_ ( C ^m B ) )
55 endomtr 
 |-  ( ( ( C ^m A ) ~~ ( C ^m x ) /\ ( C ^m x ) ~<_ ( C ^m B ) ) -> ( C ^m A ) ~<_ ( C ^m B ) )
56 25 54 55 syl2anc 
 |-  ( ( ( A ~<_ B /\ C e. _V ) /\ ( C =/= (/) /\ ( A ~~ x /\ x C_ B ) ) ) -> ( C ^m A ) ~<_ ( C ^m B ) )
57 56 expr 
 |-  ( ( ( A ~<_ B /\ C e. _V ) /\ C =/= (/) ) -> ( ( A ~~ x /\ x C_ B ) -> ( C ^m A ) ~<_ ( C ^m B ) ) )
58 57 exlimdv 
 |-  ( ( ( A ~<_ B /\ C e. _V ) /\ C =/= (/) ) -> ( E. x ( A ~~ x /\ x C_ B ) -> ( C ^m A ) ~<_ ( C ^m B ) ) )
59 20 58 mpd 
 |-  ( ( ( A ~<_ B /\ C e. _V ) /\ C =/= (/) ) -> ( C ^m A ) ~<_ ( C ^m B ) )
60 59 adantlr 
 |-  ( ( ( ( A ~<_ B /\ C e. _V ) /\ -. ( A = (/) /\ C = (/) ) ) /\ C =/= (/) ) -> ( C ^m A ) ~<_ ( C ^m B ) )
61 13 60 pm2.61dane 
 |-  ( ( ( A ~<_ B /\ C e. _V ) /\ -. ( A = (/) /\ C = (/) ) ) -> ( C ^m A ) ~<_ ( C ^m B ) )
62 61 an32s 
 |-  ( ( ( A ~<_ B /\ -. ( A = (/) /\ C = (/) ) ) /\ C e. _V ) -> ( C ^m A ) ~<_ ( C ^m B ) )
63 62 ex 
 |-  ( ( A ~<_ B /\ -. ( A = (/) /\ C = (/) ) ) -> ( C e. _V -> ( C ^m A ) ~<_ ( C ^m B ) ) )
64 reldmmap 
 |-  Rel dom ^m
65 64 ovprc1 
 |-  ( -. C e. _V -> ( C ^m A ) = (/) )
66 65 12 eqbrtrdi 
 |-  ( -. C e. _V -> ( C ^m A ) ~<_ ( C ^m B ) )
67 63 66 pm2.61d1 
 |-  ( ( A ~<_ B /\ -. ( A = (/) /\ C = (/) ) ) -> ( C ^m A ) ~<_ ( C ^m B ) )