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 ( 𝐴 ≺ 𝐵 → suc 𝐴 ≼ 𝐵 )

Proof

Step Hyp Ref Expression
1 sdomdom ⊢ ( 𝐴 ≺ 𝐵 → 𝐴 ≼ 𝐵 )
2 brdomi ⊢ ( 𝐴 ≼ 𝐵 → ∃ 𝑓 𝑓 : 𝐴 –1-1→ 𝐵 )
3 1 2 syl ⊢ ( 𝐴 ≺ 𝐵 → ∃ 𝑓 𝑓 : 𝐴 –1-1→ 𝐵 )
4 vex ⊢ 𝑓 ∈ V
5 4 rnex ⊢ ran 𝑓 ∈ V
6 f1f1orn ⊢ ( 𝑓 : 𝐴 –1-1→ 𝐵 → 𝑓 : 𝐴 –1-1-onto→ ran 𝑓 )
7 6 adantl ⊢ ( ( 𝐴 ≺ 𝐵 ∧ 𝑓 : 𝐴 –1-1→ 𝐵 ) → 𝑓 : 𝐴 –1-1-onto→ ran 𝑓 )
8 f1of1 ⊢ ( 𝑓 : 𝐴 –1-1-onto→ ran 𝑓 → 𝑓 : 𝐴 –1-1→ ran 𝑓 )
9 7 8 syl ⊢ ( ( 𝐴 ≺ 𝐵 ∧ 𝑓 : 𝐴 –1-1→ 𝐵 ) → 𝑓 : 𝐴 –1-1→ ran 𝑓 )
10 f1dom3g ⊢ ( ( 𝑓 ∈ V ∧ ran 𝑓 ∈ V ∧ 𝑓 : 𝐴 –1-1→ ran 𝑓 ) → 𝐴 ≼ ran 𝑓 )
11 4 5 9 10 mp3an12i ⊢ ( ( 𝐴 ≺ 𝐵 ∧ 𝑓 : 𝐴 –1-1→ 𝐵 ) → 𝐴 ≼ ran 𝑓 )
12 sdomnen ⊢ ( 𝐴 ≺ 𝐵 → ¬ 𝐴 ≈ 𝐵 )
13 12 adantr ⊢ ( ( 𝐴 ≺ 𝐵 ∧ 𝑓 : 𝐴 –1-1→ 𝐵 ) → ¬ 𝐴 ≈ 𝐵 )
14 ssdif0 ⊢ ( 𝐵 ⊆ ran 𝑓 ↔ ( 𝐵 ∖ ran 𝑓 ) = ∅ )
15 simplr ⊢ ( ( ( 𝐴 ≺ 𝐵 ∧ 𝑓 : 𝐴 –1-1→ 𝐵 ) ∧ 𝐵 ⊆ ran 𝑓 ) → 𝑓 : 𝐴 –1-1→ 𝐵 )
16 f1f ⊢ ( 𝑓 : 𝐴 –1-1→ 𝐵 → 𝑓 : 𝐴 ⟶ 𝐵 )
17 16 frnd ⊢ ( 𝑓 : 𝐴 –1-1→ 𝐵 → ran 𝑓 ⊆ 𝐵 )
18 15 17 syl ⊢ ( ( ( 𝐴 ≺ 𝐵 ∧ 𝑓 : 𝐴 –1-1→ 𝐵 ) ∧ 𝐵 ⊆ ran 𝑓 ) → ran 𝑓 ⊆ 𝐵 )
19 simpr ⊢ ( ( ( 𝐴 ≺ 𝐵 ∧ 𝑓 : 𝐴 –1-1→ 𝐵 ) ∧ 𝐵 ⊆ ran 𝑓 ) → 𝐵 ⊆ ran 𝑓 )
20 18 19 eqssd ⊢ ( ( ( 𝐴 ≺ 𝐵 ∧ 𝑓 : 𝐴 –1-1→ 𝐵 ) ∧ 𝐵 ⊆ ran 𝑓 ) → ran 𝑓 = 𝐵 )
21 dff1o5 ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ↔ ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ ran 𝑓 = 𝐵 ) )
22 15 20 21 sylanbrc ⊢ ( ( ( 𝐴 ≺ 𝐵 ∧ 𝑓 : 𝐴 –1-1→ 𝐵 ) ∧ 𝐵 ⊆ ran 𝑓 ) → 𝑓 : 𝐴 –1-1-onto→ 𝐵 )
23 f1oen3g ⊢ ( ( 𝑓 ∈ V ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) → 𝐴 ≈ 𝐵 )
24 4 22 23 sylancr ⊢ ( ( ( 𝐴 ≺ 𝐵 ∧ 𝑓 : 𝐴 –1-1→ 𝐵 ) ∧ 𝐵 ⊆ ran 𝑓 ) → 𝐴 ≈ 𝐵 )
25 24 ex ⊢ ( ( 𝐴 ≺ 𝐵 ∧ 𝑓 : 𝐴 –1-1→ 𝐵 ) → ( 𝐵 ⊆ ran 𝑓 → 𝐴 ≈ 𝐵 ) )
26 14 25 biimtrrid ⊢ ( ( 𝐴 ≺ 𝐵 ∧ 𝑓 : 𝐴 –1-1→ 𝐵 ) → ( ( 𝐵 ∖ ran 𝑓 ) = ∅ → 𝐴 ≈ 𝐵 ) )
27 13 26 mtod ⊢ ( ( 𝐴 ≺ 𝐵 ∧ 𝑓 : 𝐴 –1-1→ 𝐵 ) → ¬ ( 𝐵 ∖ ran 𝑓 ) = ∅ )
28 neq0 ⊢ ( ¬ ( 𝐵 ∖ ran 𝑓 ) = ∅ ↔ ∃ 𝑤 𝑤 ∈ ( 𝐵 ∖ ran 𝑓 ) )
29 27 28 sylib ⊢ ( ( 𝐴 ≺ 𝐵 ∧ 𝑓 : 𝐴 –1-1→ 𝐵 ) → ∃ 𝑤 𝑤 ∈ ( 𝐵 ∖ ran 𝑓 ) )
30 snssi ⊢ ( 𝑤 ∈ ( 𝐵 ∖ ran 𝑓 ) → { 𝑤 } ⊆ ( 𝐵 ∖ ran 𝑓 ) )
31 relsdom ⊢ Rel ≺
32 31 brrelex1i ⊢ ( 𝐴 ≺ 𝐵 → 𝐴 ∈ V )
33 32 adantr ⊢ ( ( 𝐴 ≺ 𝐵 ∧ 𝑓 : 𝐴 –1-1→ 𝐵 ) → 𝐴 ∈ V )
34 vex ⊢ 𝑤 ∈ V
35 en2sn ⊢ ( ( 𝐴 ∈ V ∧ 𝑤 ∈ V ) → { 𝐴 } ≈ { 𝑤 } )
36 33 34 35 sylancl ⊢ ( ( 𝐴 ≺ 𝐵 ∧ 𝑓 : 𝐴 –1-1→ 𝐵 ) → { 𝐴 } ≈ { 𝑤 } )
37 31 brrelex2i ⊢ ( 𝐴 ≺ 𝐵 → 𝐵 ∈ V )
38 37 adantr ⊢ ( ( 𝐴 ≺ 𝐵 ∧ 𝑓 : 𝐴 –1-1→ 𝐵 ) → 𝐵 ∈ V )
39 difexg ⊢ ( 𝐵 ∈ V → ( 𝐵 ∖ ran 𝑓 ) ∈ V )
40 snfi ⊢ { 𝑤 } ∈ Fin
41 ssdomfi2 ⊢ ( ( { 𝑤 } ∈ Fin ∧ ( 𝐵 ∖ ran 𝑓 ) ∈ V ∧ { 𝑤 } ⊆ ( 𝐵 ∖ ran 𝑓 ) ) → { 𝑤 } ≼ ( 𝐵 ∖ ran 𝑓 ) )
42 40 41 mp3an1 ⊢ ( ( ( 𝐵 ∖ ran 𝑓 ) ∈ V ∧ { 𝑤 } ⊆ ( 𝐵 ∖ ran 𝑓 ) ) → { 𝑤 } ≼ ( 𝐵 ∖ ran 𝑓 ) )
43 42 ex ⊢ ( ( 𝐵 ∖ ran 𝑓 ) ∈ V → ( { 𝑤 } ⊆ ( 𝐵 ∖ ran 𝑓 ) → { 𝑤 } ≼ ( 𝐵 ∖ ran 𝑓 ) ) )
44 38 39 43 3syl ⊢ ( ( 𝐴 ≺ 𝐵 ∧ 𝑓 : 𝐴 –1-1→ 𝐵 ) → ( { 𝑤 } ⊆ ( 𝐵 ∖ ran 𝑓 ) → { 𝑤 } ≼ ( 𝐵 ∖ ran 𝑓 ) ) )
45 endom ⊢ ( { 𝐴 } ≈ { 𝑤 } → { 𝐴 } ≼ { 𝑤 } )
46 domtrfi ⊢ ( ( { 𝑤 } ∈ Fin ∧ { 𝐴 } ≼ { 𝑤 } ∧ { 𝑤 } ≼ ( 𝐵 ∖ ran 𝑓 ) ) → { 𝐴 } ≼ ( 𝐵 ∖ ran 𝑓 ) )
47 40 46 mp3an1 ⊢ ( ( { 𝐴 } ≼ { 𝑤 } ∧ { 𝑤 } ≼ ( 𝐵 ∖ ran 𝑓 ) ) → { 𝐴 } ≼ ( 𝐵 ∖ ran 𝑓 ) )
48 45 47 sylan ⊢ ( ( { 𝐴 } ≈ { 𝑤 } ∧ { 𝑤 } ≼ ( 𝐵 ∖ ran 𝑓 ) ) → { 𝐴 } ≼ ( 𝐵 ∖ ran 𝑓 ) )
49 36 44 48 syl6an ⊢ ( ( 𝐴 ≺ 𝐵 ∧ 𝑓 : 𝐴 –1-1→ 𝐵 ) → ( { 𝑤 } ⊆ ( 𝐵 ∖ ran 𝑓 ) → { 𝐴 } ≼ ( 𝐵 ∖ ran 𝑓 ) ) )
50 30 49 syl5 ⊢ ( ( 𝐴 ≺ 𝐵 ∧ 𝑓 : 𝐴 –1-1→ 𝐵 ) → ( 𝑤 ∈ ( 𝐵 ∖ ran 𝑓 ) → { 𝐴 } ≼ ( 𝐵 ∖ ran 𝑓 ) ) )
51 50 exlimdv ⊢ ( ( 𝐴 ≺ 𝐵 ∧ 𝑓 : 𝐴 –1-1→ 𝐵 ) → ( ∃ 𝑤 𝑤 ∈ ( 𝐵 ∖ ran 𝑓 ) → { 𝐴 } ≼ ( 𝐵 ∖ ran 𝑓 ) ) )
52 29 51 mpd ⊢ ( ( 𝐴 ≺ 𝐵 ∧ 𝑓 : 𝐴 –1-1→ 𝐵 ) → { 𝐴 } ≼ ( 𝐵 ∖ ran 𝑓 ) )
53 disjdif ⊢ ( ran 𝑓 ∩ ( 𝐵 ∖ ran 𝑓 ) ) = ∅
54 53 a1i ⊢ ( ( 𝐴 ≺ 𝐵 ∧ 𝑓 : 𝐴 –1-1→ 𝐵 ) → ( ran 𝑓 ∩ ( 𝐵 ∖ ran 𝑓 ) ) = ∅ )
55 undom ⊢ ( ( ( 𝐴 ≼ ran 𝑓 ∧ { 𝐴 } ≼ ( 𝐵 ∖ ran 𝑓 ) ) ∧ ( ran 𝑓 ∩ ( 𝐵 ∖ ran 𝑓 ) ) = ∅ ) → ( 𝐴 ∪ { 𝐴 } ) ≼ ( ran 𝑓 ∪ ( 𝐵 ∖ ran 𝑓 ) ) )
56 11 52 54 55 syl21anc ⊢ ( ( 𝐴 ≺ 𝐵 ∧ 𝑓 : 𝐴 –1-1→ 𝐵 ) → ( 𝐴 ∪ { 𝐴 } ) ≼ ( ran 𝑓 ∪ ( 𝐵 ∖ ran 𝑓 ) ) )
57 df-suc ⊢ suc 𝐴 = ( 𝐴 ∪ { 𝐴 } )
58 57 a1i ⊢ ( ( 𝐴 ≺ 𝐵 ∧ 𝑓 : 𝐴 –1-1→ 𝐵 ) → suc 𝐴 = ( 𝐴 ∪ { 𝐴 } ) )
59 undif2 ⊢ ( ran 𝑓 ∪ ( 𝐵 ∖ ran 𝑓 ) ) = ( ran 𝑓 ∪ 𝐵 )
60 17 adantl ⊢ ( ( 𝐴 ≺ 𝐵 ∧ 𝑓 : 𝐴 –1-1→ 𝐵 ) → ran 𝑓 ⊆ 𝐵 )
61 ssequn1 ⊢ ( ran 𝑓 ⊆ 𝐵 ↔ ( ran 𝑓 ∪ 𝐵 ) = 𝐵 )
62 60 61 sylib ⊢ ( ( 𝐴 ≺ 𝐵 ∧ 𝑓 : 𝐴 –1-1→ 𝐵 ) → ( ran 𝑓 ∪ 𝐵 ) = 𝐵 )
63 59 62 eqtr2id ⊢ ( ( 𝐴 ≺ 𝐵 ∧ 𝑓 : 𝐴 –1-1→ 𝐵 ) → 𝐵 = ( ran 𝑓 ∪ ( 𝐵 ∖ ran 𝑓 ) ) )
64 56 58 63 3brtr4d ⊢ ( ( 𝐴 ≺ 𝐵 ∧ 𝑓 : 𝐴 –1-1→ 𝐵 ) → suc 𝐴 ≼ 𝐵 )
65 3 64 exlimddv ⊢ ( 𝐴 ≺ 𝐵 → suc 𝐴 ≼ 𝐵 )