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

Proof

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