Theorem infensuc 8407

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

Assertion

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

Proof of Theorem infensuc

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		onprc 7245	. . . . 5 ⊢ ¬ On ∈ V
2		eleq1 2894	. . . . 5 ⊢ (ω = On → (ω ∈ V ↔ On ∈ V))
3	1, 2	mtbiri 319	. . . 4 ⊢ (ω = On → ¬ ω ∈ V)
4		ssexg 5029	. . . . 5 ⊢ ((ω ⊆ 𝐴 ∧ 𝐴 ∈ On) → ω ∈ V)
5	4	ancoms 452	. . . 4 ⊢ ((𝐴 ∈ On ∧ ω ⊆ 𝐴) → ω ∈ V)
6	3, 5	nsyl3 136	. . 3 ⊢ ((𝐴 ∈ On ∧ ω ⊆ 𝐴) → ¬ ω = On)
7		omon 7337	. . . 4 ⊢ (ω ∈ On ∨ ω = On)
8	7	ori 892	. . 3 ⊢ (¬ ω ∈ On → ω = On)
9	6, 8	nsyl2 145	. 2 ⊢ ((𝐴 ∈ On ∧ ω ⊆ 𝐴) → ω ∈ On)
10		id 22	. . . . . . 7 ⊢ (𝑥 = ω → 𝑥 = ω)
11		suceq 6028	. . . . . . 7 ⊢ (𝑥 = ω → suc 𝑥 = suc ω)
12	10, 11	breq12d 4886	. . . . . 6 ⊢ (𝑥 = ω → (𝑥 ≈ suc 𝑥 ↔ ω ≈ suc ω))
13		id 22	. . . . . . 7 ⊢ (𝑥 = 𝑦 → 𝑥 = 𝑦)
14		suceq 6028	. . . . . . 7 ⊢ (𝑥 = 𝑦 → suc 𝑥 = suc 𝑦)
15	13, 14	breq12d 4886	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝑥 ≈ suc 𝑥 ↔ 𝑦 ≈ suc 𝑦))
16		id 22	. . . . . . 7 ⊢ (𝑥 = suc 𝑦 → 𝑥 = suc 𝑦)
17		suceq 6028	. . . . . . 7 ⊢ (𝑥 = suc 𝑦 → suc 𝑥 = suc suc 𝑦)
18	16, 17	breq12d 4886	. . . . . 6 ⊢ (𝑥 = suc 𝑦 → (𝑥 ≈ suc 𝑥 ↔ suc 𝑦 ≈ suc suc 𝑦))
19		id 22	. . . . . . 7 ⊢ (𝑥 = 𝐴 → 𝑥 = 𝐴)
20		suceq 6028	. . . . . . 7 ⊢ (𝑥 = 𝐴 → suc 𝑥 = suc 𝐴)
21	19, 20	breq12d 4886	. . . . . 6 ⊢ (𝑥 = 𝐴 → (𝑥 ≈ suc 𝑥 ↔ 𝐴 ≈ suc 𝐴))
22		limom 7341	. . . . . . 7 ⊢ Lim ω
23	22	limensuci 8405	. . . . . 6 ⊢ (ω ∈ On → ω ≈ suc ω)
24		vex 3417	. . . . . . . . . 10 ⊢ 𝑦 ∈ V
25	24	sucex 7272	. . . . . . . . . 10 ⊢ suc 𝑦 ∈ V
26		en2sn 8306	. . . . . . . . . 10 ⊢ ((𝑦 ∈ V ∧ suc 𝑦 ∈ V) → {𝑦} ≈ {suc 𝑦})
27	24, 25, 26	mp2an 683	. . . . . . . . 9 ⊢ {𝑦} ≈ {suc 𝑦}
28		eloni 5973	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ On → Ord 𝑦)
29		ordirr 5981	. . . . . . . . . . . . 13 ⊢ (Ord 𝑦 → ¬ 𝑦 ∈ 𝑦)
30	28, 29	syl 17	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ On → ¬ 𝑦 ∈ 𝑦)
31		disjsn 4465	. . . . . . . . . . . 12 ⊢ ((𝑦 ∩ {𝑦}) = ∅ ↔ ¬ 𝑦 ∈ 𝑦)
32	30, 31	sylibr 226	. . . . . . . . . . 11 ⊢ (𝑦 ∈ On → (𝑦 ∩ {𝑦}) = ∅)
33		eloni 5973	. . . . . . . . . . . . 13 ⊢ (suc 𝑦 ∈ On → Ord suc 𝑦)
34		ordirr 5981	. . . . . . . . . . . . 13 ⊢ (Ord suc 𝑦 → ¬ suc 𝑦 ∈ suc 𝑦)
35	33, 34	syl 17	. . . . . . . . . . . 12 ⊢ (suc 𝑦 ∈ On → ¬ suc 𝑦 ∈ suc 𝑦)
36		sucelon 7278	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ On ↔ suc 𝑦 ∈ On)
37		disjsn 4465	. . . . . . . . . . . 12 ⊢ ((suc 𝑦 ∩ {suc 𝑦}) = ∅ ↔ ¬ suc 𝑦 ∈ suc 𝑦)
38	35, 36, 37	3imtr4i 284	. . . . . . . . . . 11 ⊢ (𝑦 ∈ On → (suc 𝑦 ∩ {suc 𝑦}) = ∅)
39	32, 38	jca 507	. . . . . . . . . 10 ⊢ (𝑦 ∈ On → ((𝑦 ∩ {𝑦}) = ∅ ∧ (suc 𝑦 ∩ {suc 𝑦}) = ∅))
40		unen 8309	. . . . . . . . . . . 12 ⊢ (((𝑦 ≈ suc 𝑦 ∧ {𝑦} ≈ {suc 𝑦}) ∧ ((𝑦 ∩ {𝑦}) = ∅ ∧ (suc 𝑦 ∩ {suc 𝑦}) = ∅)) → (𝑦 ∪ {𝑦}) ≈ (suc 𝑦 ∪ {suc 𝑦}))
41		df-suc 5969	. . . . . . . . . . . 12 ⊢ suc 𝑦 = (𝑦 ∪ {𝑦})
42		df-suc 5969	. . . . . . . . . . . 12 ⊢ suc suc 𝑦 = (suc 𝑦 ∪ {suc 𝑦})
43	40, 41, 42	3brtr4g 4907	. . . . . . . . . . 11 ⊢ (((𝑦 ≈ suc 𝑦 ∧ {𝑦} ≈ {suc 𝑦}) ∧ ((𝑦 ∩ {𝑦}) = ∅ ∧ (suc 𝑦 ∩ {suc 𝑦}) = ∅)) → suc 𝑦 ≈ suc suc 𝑦)
44	43	ex 403	. . . . . . . . . 10 ⊢ ((𝑦 ≈ suc 𝑦 ∧ {𝑦} ≈ {suc 𝑦}) → (((𝑦 ∩ {𝑦}) = ∅ ∧ (suc 𝑦 ∩ {suc 𝑦}) = ∅) → suc 𝑦 ≈ suc suc 𝑦))
45	39, 44	syl5 34	. . . . . . . . 9 ⊢ ((𝑦 ≈ suc 𝑦 ∧ {𝑦} ≈ {suc 𝑦}) → (𝑦 ∈ On → suc 𝑦 ≈ suc suc 𝑦))
46	27, 45	mpan2 682	. . . . . . . 8 ⊢ (𝑦 ≈ suc 𝑦 → (𝑦 ∈ On → suc 𝑦 ≈ suc suc 𝑦))
47	46	com12 32	. . . . . . 7 ⊢ (𝑦 ∈ On → (𝑦 ≈ suc 𝑦 → suc 𝑦 ≈ suc suc 𝑦))
48	47	ad2antrr 717	. . . . . 6 ⊢ (((𝑦 ∈ On ∧ ω ∈ On) ∧ ω ⊆ 𝑦) → (𝑦 ≈ suc 𝑦 → suc 𝑦 ≈ suc suc 𝑦))
49		vex 3417	. . . . . . . . 9 ⊢ 𝑥 ∈ V
50		limensuc 8406	. . . . . . . . 9 ⊢ ((𝑥 ∈ V ∧ Lim 𝑥) → 𝑥 ≈ suc 𝑥)
51	49, 50	mpan 681	. . . . . . . 8 ⊢ (Lim 𝑥 → 𝑥 ≈ suc 𝑥)
52	51	ad2antrr 717	. . . . . . 7 ⊢ (((Lim 𝑥 ∧ ω ∈ On) ∧ ω ⊆ 𝑥) → 𝑥 ≈ suc 𝑥)
53	52	a1d 25	. . . . . 6 ⊢ (((Lim 𝑥 ∧ ω ∈ On) ∧ ω ⊆ 𝑥) → (∀𝑦 ∈ 𝑥 (ω ⊆ 𝑦 → 𝑦 ≈ suc 𝑦) → 𝑥 ≈ suc 𝑥))
54	12, 15, 18, 21, 23, 48, 53	tfindsg 7321	. . . . 5 ⊢ (((𝐴 ∈ On ∧ ω ∈ On) ∧ ω ⊆ 𝐴) → 𝐴 ≈ suc 𝐴)
55	54	exp31 412	. . . 4 ⊢ (𝐴 ∈ On → (ω ∈ On → (ω ⊆ 𝐴 → 𝐴 ≈ suc 𝐴)))
56	55	com23 86	. . 3 ⊢ (𝐴 ∈ On → (ω ⊆ 𝐴 → (ω ∈ On → 𝐴 ≈ suc 𝐴)))
57	56	imp 397	. 2 ⊢ ((𝐴 ∈ On ∧ ω ⊆ 𝐴) → (ω ∈ On → 𝐴 ≈ suc 𝐴))
58	9, 57	mpd 15	1 ⊢ ((𝐴 ∈ On ∧ ω ⊆ 𝐴) → 𝐴 ≈ suc 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 386   = wceq 1656   ∈ wcel 2164  ∀wral 3117  Vcvv 3414   ∪ cun 3796   ∩ cin 3797   ⊆ wss 3798  ∅c0 4144  {csn 4397   class class class wbr 4873  Ord word 5962  Oncon0 5963  Lim wlim 5964  suc csuc 5965  ωcom 7326   ≈ cen 8219

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-8 2166  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803  ax-sep 5005  ax-nul 5013  ax-pow 5065  ax-pr 5127  ax-un 7209

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3or 1112  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-ral 3122  df-rex 3123  df-rab 3126  df-v 3416  df-sbc 3663  df-csb 3758  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-pss 3814  df-nul 4145  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-tp 4402  df-op 4404  df-uni 4659  df-br 4874  df-opab 4936  df-mpt 4953  df-tr 4976  df-id 5250  df-eprel 5255  df-po 5263  df-so 5264  df-fr 5301  df-we 5303  df-xp 5348  df-rel 5349  df-cnv 5350  df-co 5351  df-dm 5352  df-rn 5353  df-res 5354  df-ima 5355  df-ord 5966  df-on 5967  df-lim 5968  df-suc 5969  df-iota 6086  df-fun 6125  df-fn 6126  df-f 6127  df-f1 6128  df-fo 6129  df-f1o 6130  df-fv 6131  df-om 7327  df-1o 7826  df-er 8009  df-en 8223  df-dom 8224

This theorem is referenced by:  cardlim  9111  cardsucinf  9123