This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem infensuc

Description: Any infinite ordinal is equinumerous to its successor. Exercise 7 of TakeutiZaring p. 88. Proved without the Axiom of Infinity. (Contributed by NM, 30-Oct-2003) (Revised by Mario Carneiro, 13-Jan-2013)

Ref Expression
Assertion infensuc ( ( 𝐴 ∈ On ∧ ω ⊆ 𝐴 ) → 𝐴 ≈ suc 𝐴 )

Proof

Step Hyp Ref Expression
1 onprc ⊢ ¬ On ∈ V
2 eleq1 ⊢ ( ω = On → ( ω ∈ V ↔ On ∈ V ) )
3 1 2 mtbiri ⊢ ( ω = On → ¬ ω ∈ V )
4 ssexg ⊢ ( ( ω ⊆ 𝐴 ∧ 𝐴 ∈ On ) → ω ∈ V )
5 4 ancoms ⊢ ( ( 𝐴 ∈ On ∧ ω ⊆ 𝐴 ) → ω ∈ V )
6 3 5 nsyl3 ⊢ ( ( 𝐴 ∈ On ∧ ω ⊆ 𝐴 ) → ¬ ω = On )
7 omon ⊢ ( ω ∈ On ∨ ω = On )
8 7 ori ⊢ ( ¬ ω ∈ On → ω = On )
9 6 8 nsyl2 ⊢ ( ( 𝐴 ∈ On ∧ ω ⊆ 𝐴 ) → ω ∈ On )
10 id ⊢ ( 𝑥 = ω → 𝑥 = ω )
11 suceq ⊢ ( 𝑥 = ω → suc 𝑥 = suc ω )
12 10 11 breq12d ⊢ ( 𝑥 = ω → ( 𝑥 ≈ suc 𝑥 ↔ ω ≈ suc ω ) )
13 id ⊢ ( 𝑥 = 𝑦 → 𝑥 = 𝑦 )
14 suceq ⊢ ( 𝑥 = 𝑦 → suc 𝑥 = suc 𝑦 )
15 13 14 breq12d ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ≈ suc 𝑥 ↔ 𝑦 ≈ suc 𝑦 ) )
16 id ⊢ ( 𝑥 = suc 𝑦 → 𝑥 = suc 𝑦 )
17 suceq ⊢ ( 𝑥 = suc 𝑦 → suc 𝑥 = suc suc 𝑦 )
18 16 17 breq12d ⊢ ( 𝑥 = suc 𝑦 → ( 𝑥 ≈ suc 𝑥 ↔ suc 𝑦 ≈ suc suc 𝑦 ) )
19 id ⊢ ( 𝑥 = 𝐴 → 𝑥 = 𝐴 )
20 suceq ⊢ ( 𝑥 = 𝐴 → suc 𝑥 = suc 𝐴 )
21 19 20 breq12d ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ≈ suc 𝑥 ↔ 𝐴 ≈ suc 𝐴 ) )
22 limom ⊢ Lim ω
23 22 limensuci ⊢ ( ω ∈ On → ω ≈ suc ω )
24 vex ⊢ 𝑦 ∈ V
25 24 sucex ⊢ suc 𝑦 ∈ V
26 en2sn ⊢ ( ( 𝑦 ∈ V ∧ suc 𝑦 ∈ V ) → { 𝑦 } ≈ { suc 𝑦 } )
27 24 25 26 mp2an ⊢ { 𝑦 } ≈ { suc 𝑦 }
28 eloni ⊢ ( 𝑦 ∈ On → Ord 𝑦 )
29 ordirr ⊢ ( Ord 𝑦 → ¬ 𝑦 ∈ 𝑦 )
30 28 29 syl ⊢ ( 𝑦 ∈ On → ¬ 𝑦 ∈ 𝑦 )
31 disjsn ⊢ ( ( 𝑦 ∩ { 𝑦 } ) = ∅ ↔ ¬ 𝑦 ∈ 𝑦 )
32 30 31 sylibr ⊢ ( 𝑦 ∈ On → ( 𝑦 ∩ { 𝑦 } ) = ∅ )
33 eloni ⊢ ( suc 𝑦 ∈ On → Ord suc 𝑦 )
34 ordirr ⊢ ( Ord suc 𝑦 → ¬ suc 𝑦 ∈ suc 𝑦 )
35 33 34 syl ⊢ ( suc 𝑦 ∈ On → ¬ suc 𝑦 ∈ suc 𝑦 )
36 onsucb ⊢ ( 𝑦 ∈ On ↔ suc 𝑦 ∈ On )
37 disjsn ⊢ ( ( suc 𝑦 ∩ { suc 𝑦 } ) = ∅ ↔ ¬ suc 𝑦 ∈ suc 𝑦 )
38 35 36 37 3imtr4i ⊢ ( 𝑦 ∈ On → ( suc 𝑦 ∩ { suc 𝑦 } ) = ∅ )
39 32 38 jca ⊢ ( 𝑦 ∈ On → ( ( 𝑦 ∩ { 𝑦 } ) = ∅ ∧ ( suc 𝑦 ∩ { suc 𝑦 } ) = ∅ ) )
40 unen ⊢ ( ( ( 𝑦 ≈ suc 𝑦 ∧ { 𝑦 } ≈ { suc 𝑦 } ) ∧ ( ( 𝑦 ∩ { 𝑦 } ) = ∅ ∧ ( suc 𝑦 ∩ { suc 𝑦 } ) = ∅ ) ) → ( 𝑦 ∪ { 𝑦 } ) ≈ ( suc 𝑦 ∪ { suc 𝑦 } ) )
41 df-suc ⊢ suc 𝑦 = ( 𝑦 ∪ { 𝑦 } )
42 df-suc ⊢ suc suc 𝑦 = ( suc 𝑦 ∪ { suc 𝑦 } )
43 40 41 42 3brtr4g ⊢ ( ( ( 𝑦 ≈ suc 𝑦 ∧ { 𝑦 } ≈ { suc 𝑦 } ) ∧ ( ( 𝑦 ∩ { 𝑦 } ) = ∅ ∧ ( suc 𝑦 ∩ { suc 𝑦 } ) = ∅ ) ) → suc 𝑦 ≈ suc suc 𝑦 )
44 43 ex ⊢ ( ( 𝑦 ≈ suc 𝑦 ∧ { 𝑦 } ≈ { suc 𝑦 } ) → ( ( ( 𝑦 ∩ { 𝑦 } ) = ∅ ∧ ( suc 𝑦 ∩ { suc 𝑦 } ) = ∅ ) → suc 𝑦 ≈ suc suc 𝑦 ) )
45 39 44 syl5 ⊢ ( ( 𝑦 ≈ suc 𝑦 ∧ { 𝑦 } ≈ { suc 𝑦 } ) → ( 𝑦 ∈ On → suc 𝑦 ≈ suc suc 𝑦 ) )
46 27 45 mpan2 ⊢ ( 𝑦 ≈ suc 𝑦 → ( 𝑦 ∈ On → suc 𝑦 ≈ suc suc 𝑦 ) )
47 46 com12 ⊢ ( 𝑦 ∈ On → ( 𝑦 ≈ suc 𝑦 → suc 𝑦 ≈ suc suc 𝑦 ) )
48 47 ad2antrr ⊢ ( ( ( 𝑦 ∈ On ∧ ω ∈ On ) ∧ ω ⊆ 𝑦 ) → ( 𝑦 ≈ suc 𝑦 → suc 𝑦 ≈ suc suc 𝑦 ) )
49 vex ⊢ 𝑥 ∈ V
50 limensuc ⊢ ( ( 𝑥 ∈ V ∧ Lim 𝑥 ) → 𝑥 ≈ suc 𝑥 )
51 49 50 mpan ⊢ ( Lim 𝑥 → 𝑥 ≈ suc 𝑥 )
52 51 ad2antrr ⊢ ( ( ( Lim 𝑥 ∧ ω ∈ On ) ∧ ω ⊆ 𝑥 ) → 𝑥 ≈ suc 𝑥 )
53 52 a1d ⊢ ( ( ( Lim 𝑥 ∧ ω ∈ On ) ∧ ω ⊆ 𝑥 ) → ( ∀ 𝑦 ∈ 𝑥 ( ω ⊆ 𝑦 → 𝑦 ≈ suc 𝑦 ) → 𝑥 ≈ suc 𝑥 ) )
54 12 15 18 21 23 48 53 tfindsg ⊢ ( ( ( 𝐴 ∈ On ∧ ω ∈ On ) ∧ ω ⊆ 𝐴 ) → 𝐴 ≈ suc 𝐴 )
55 54 exp31 ⊢ ( 𝐴 ∈ On → ( ω ∈ On → ( ω ⊆ 𝐴 → 𝐴 ≈ suc 𝐴 ) ) )
56 55 com23 ⊢ ( 𝐴 ∈ On → ( ω ⊆ 𝐴 → ( ω ∈ On → 𝐴 ≈ suc 𝐴 ) ) )
57 56 imp ⊢ ( ( 𝐴 ∈ On ∧ ω ⊆ 𝐴 ) → ( ω ∈ On → 𝐴 ≈ suc 𝐴 ) )
58 9 57 mpd ⊢ ( ( 𝐴 ∈ On ∧ ω ⊆ 𝐴 ) → 𝐴 ≈ suc 𝐴 )