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 𝐴 )