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) Avoid ax-pow . (Revised by BTernaryTau, 4-Dec-2024)

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