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 f f : A 1-1 B
3 1 2 syl A B f f : A 1-1 B
4 relsdom Rel
5 4 brrelex1i A B A V
6 5 adantr A B f : A 1-1 B A V
7 vex f V
8 7 rnex ran f V
9 8 a1i A B f : A 1-1 B ran f 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 V ran f 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 ran f B ran f =
19 simplr A B f : A 1-1 B B 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 B
22 19 21 syl A B f : A 1-1 B B ran f ran f B
23 simpr A B f : A 1-1 B B ran f B ran f
24 22 23 eqssd A B f : A 1-1 B B 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 ran f f : A 1-1 onto B
27 f1oen3g f V f : A 1-1 onto B A B
28 7 26 27 sylancr A B f : A 1-1 B B ran f A B
29 28 ex A B f : A 1-1 B B 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 = w w B ran f
33 31 32 sylib A B f : A 1-1 B w w B ran f
34 snssi w B ran f w B ran f
35 vex w V
36 en2sn A V w V A w
37 6 35 36 sylancl A B f : A 1-1 B A w
38 4 brrelex2i A B B V
39 38 adantr A B f : A 1-1 B B V
40 difexg B V B ran f V
41 ssdomg B ran f V w B ran f w B ran f
42 39 40 41 3syl A B f : A 1-1 B w 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 B ran f A B ran f
45 34 44 syl5 A B f : A 1-1 B w B ran f A B ran f
46 45 exlimdv A B f : A 1-1 B w w 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 B ran f =
49 48 a1i A B f : A 1-1 B ran f B ran f =
50 undom A ran f A B ran f ran f B ran f = A A ran f B ran f
51 15 47 49 50 syl21anc A B f : A 1-1 B A A ran f B ran f
52 df-suc suc A = A A
53 52 a1i A B f : A 1-1 B suc A = A A
54 undif2 ran f B ran f = ran f B
55 21 adantl A B f : A 1-1 B ran f B
56 ssequn1 ran f B ran f B = B
57 55 56 sylib A B f : A 1-1 B ran f B = B
58 54 57 eqtr2id A B f : A 1-1 B B = ran f 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