Metamath Proof Explorer

Theorem sucdom2

Description: Strict dominance of a set over another set implies dominance over its successor. (Contributed by Mario Carneiro, 12-Jan-2013) (Proof shortened by Mario Carneiro, 27-Apr-2015)

Ref Expression
Assertion sucdom2 
|- ( A ~< B -> suc A ~<_ B )

Proof

Step Hyp Ref Expression
1 sdomdom 
 |-  ( A ~< B -> A ~<_ B )
2 brdomi 
 |-  ( A ~<_ B -> E. f f : A -1-1-> B )
3 1 2 syl 
 |-  ( A ~< B -> E. f f : A -1-1-> B )
4 relsdom 
 |-  Rel ~<
5 4 brrelex1i 
 |-  ( A ~< B -> A e. _V )
6 5 adantr 
 |-  ( ( A ~< B /\ f : A -1-1-> B ) -> A e. _V )
7 vex 
 |-  f e. _V
8 7 rnex 
 |-  ran f e. _V
9 8 a1i 
 |-  ( ( A ~< B /\ f : A -1-1-> B ) -> ran f e. _V )
10 f1f1orn 
 |-  ( f : A -1-1-> B -> f : A -1-1-onto-> ran f )
11 10 adantl 
 |-  ( ( A ~< B /\ f : A -1-1-> B ) -> f : A -1-1-onto-> ran f )
12 f1of1 
 |-  ( f : A -1-1-onto-> ran f -> f : A -1-1-> ran f )
13 11 12 syl 
 |-  ( ( A ~< B /\ f : A -1-1-> B ) -> f : A -1-1-> ran f )
14 f1dom2g 
 |-  ( ( A e. _V /\ ran f e. _V /\ f : A -1-1-> ran f ) -> A ~<_ ran f )
15 6 9 13 14 syl3anc 
 |-  ( ( A ~< B /\ f : A -1-1-> B ) -> A ~<_ ran f )
16 sdomnen 
 |-  ( A ~< B -> -. A ~~ B )
17 16 adantr 
 |-  ( ( A ~< B /\ f : A -1-1-> B ) -> -. A ~~ B )
18 ssdif0 
 |-  ( B C_ ran f <-> ( B \ ran f ) = (/) )
19 simplr 
 |-  ( ( ( A ~< B /\ f : A -1-1-> B ) /\ B C_ ran f ) -> f : A -1-1-> B )
20 f1f 
 |-  ( f : A -1-1-> B -> f : A --> B )
21 20 frnd 
 |-  ( f : A -1-1-> B -> ran f C_ B )
22 19 21 syl 
 |-  ( ( ( A ~< B /\ f : A -1-1-> B ) /\ B C_ ran f ) -> ran f C_ B )
23 simpr 
 |-  ( ( ( A ~< B /\ f : A -1-1-> B ) /\ B C_ ran f ) -> B C_ ran f )
24 22 23 eqssd 
 |-  ( ( ( A ~< B /\ f : A -1-1-> B ) /\ B C_ ran f ) -> ran f = B )
25 dff1o5 
 |-  ( f : A -1-1-onto-> B <-> ( f : A -1-1-> B /\ ran f = B ) )
26 19 24 25 sylanbrc 
 |-  ( ( ( A ~< B /\ f : A -1-1-> B ) /\ B C_ ran f ) -> f : A -1-1-onto-> B )
27 f1oen3g 
 |-  ( ( f e. _V /\ f : A -1-1-onto-> B ) -> A ~~ B )
28 7 26 27 sylancr 
 |-  ( ( ( A ~< B /\ f : A -1-1-> B ) /\ B C_ ran f ) -> A ~~ B )
29 28 ex 
 |-  ( ( A ~< B /\ f : A -1-1-> B ) -> ( B C_ ran f -> A ~~ B ) )
30 18 29 syl5bir 
 |-  ( ( A ~< B /\ f : A -1-1-> B ) -> ( ( B \ ran f ) = (/) -> A ~~ B ) )
31 17 30 mtod 
 |-  ( ( A ~< B /\ f : A -1-1-> B ) -> -. ( B \ ran f ) = (/) )
32 neq0 
 |-  ( -. ( B \ ran f ) = (/) <-> E. w w e. ( B \ ran f ) )
33 31 32 sylib 
 |-  ( ( A ~< B /\ f : A -1-1-> B ) -> E. w w e. ( B \ ran f ) )
34 snssi 
 |-  ( w e. ( B \ ran f ) -> { w } C_ ( B \ ran f ) )
35 vex 
 |-  w e. _V
36 en2sn 
 |-  ( ( A e. _V /\ w e. _V ) -> { A } ~~ { w } )
37 6 35 36 sylancl 
 |-  ( ( A ~< B /\ f : A -1-1-> B ) -> { A } ~~ { w } )
38 4 brrelex2i 
 |-  ( A ~< B -> B e. _V )
39 38 adantr 
 |-  ( ( A ~< B /\ f : A -1-1-> B ) -> B e. _V )
40 difexg 
 |-  ( B e. _V -> ( B \ ran f ) e. _V )
41 ssdomg 
 |-  ( ( B \ ran f ) e. _V -> ( { w } C_ ( B \ ran f ) -> { w } ~<_ ( B \ ran f ) ) )
42 39 40 41 3syl 
 |-  ( ( A ~< B /\ f : A -1-1-> B ) -> ( { w } C_ ( B \ ran f ) -> { w } ~<_ ( B \ ran f ) ) )
43 endomtr 
 |-  ( ( { A } ~~ { w } /\ { w } ~<_ ( B \ ran f ) ) -> { A } ~<_ ( B \ ran f ) )
44 37 42 43 syl6an 
 |-  ( ( A ~< B /\ f : A -1-1-> B ) -> ( { w } C_ ( B \ ran f ) -> { A } ~<_ ( B \ ran f ) ) )
45 34 44 syl5 
 |-  ( ( A ~< B /\ f : A -1-1-> B ) -> ( w e. ( B \ ran f ) -> { A } ~<_ ( B \ ran f ) ) )
46 45 exlimdv 
 |-  ( ( A ~< B /\ f : A -1-1-> B ) -> ( E. w w e. ( B \ ran f ) -> { A } ~<_ ( B \ ran f ) ) )
47 33 46 mpd 
 |-  ( ( A ~< B /\ f : A -1-1-> B ) -> { A } ~<_ ( B \ ran f ) )
48 disjdif 
 |-  ( ran f i^i ( B \ ran f ) ) = (/)
49 48 a1i 
 |-  ( ( A ~< B /\ f : A -1-1-> B ) -> ( ran f i^i ( B \ ran f ) ) = (/) )
50 undom 
 |-  ( ( ( A ~<_ ran f /\ { A } ~<_ ( B \ ran f ) ) /\ ( ran f i^i ( B \ ran f ) ) = (/) ) -> ( A u. { A } ) ~<_ ( ran f u. ( B \ ran f ) ) )
51 15 47 49 50 syl21anc 
 |-  ( ( A ~< B /\ f : A -1-1-> B ) -> ( A u. { A } ) ~<_ ( ran f u. ( B \ ran f ) ) )
52 df-suc 
 |-  suc A = ( A u. { A } )
53 52 a1i 
 |-  ( ( A ~< B /\ f : A -1-1-> B ) -> suc A = ( A u. { A } ) )
54 undif2 
 |-  ( ran f u. ( B \ ran f ) ) = ( ran f u. B )
55 21 adantl 
 |-  ( ( A ~< B /\ f : A -1-1-> B ) -> ran f C_ B )
56 ssequn1 
 |-  ( ran f C_ B <-> ( ran f u. B ) = B )
57 55 56 sylib 
 |-  ( ( A ~< B /\ f : A -1-1-> B ) -> ( ran f u. B ) = B )
58 54 57 syl5req 
 |-  ( ( A ~< B /\ f : A -1-1-> B ) -> B = ( ran f u. ( B \ ran f ) ) )
59 51 53 58 3brtr4d 
 |-  ( ( A ~< B /\ f : A -1-1-> B ) -> suc A ~<_ B )
60 3 59 exlimddv 
 |-  ( A ~< B -> suc A ~<_ B )