# 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 ${⊢}\left({A}\in \mathrm{On}\wedge \mathrm{\omega }\subseteq {A}\right)\to {A}\approx \mathrm{suc}{A}$

### Proof

Step Hyp Ref Expression
1 onprc ${⊢}¬\mathrm{On}\in \mathrm{V}$
2 eleq1 ${⊢}\mathrm{\omega }=\mathrm{On}\to \left(\mathrm{\omega }\in \mathrm{V}↔\mathrm{On}\in \mathrm{V}\right)$
3 1 2 mtbiri ${⊢}\mathrm{\omega }=\mathrm{On}\to ¬\mathrm{\omega }\in \mathrm{V}$
4 ssexg ${⊢}\left(\mathrm{\omega }\subseteq {A}\wedge {A}\in \mathrm{On}\right)\to \mathrm{\omega }\in \mathrm{V}$
5 4 ancoms ${⊢}\left({A}\in \mathrm{On}\wedge \mathrm{\omega }\subseteq {A}\right)\to \mathrm{\omega }\in \mathrm{V}$
6 3 5 nsyl3 ${⊢}\left({A}\in \mathrm{On}\wedge \mathrm{\omega }\subseteq {A}\right)\to ¬\mathrm{\omega }=\mathrm{On}$
7 omon ${⊢}\left(\mathrm{\omega }\in \mathrm{On}\vee \mathrm{\omega }=\mathrm{On}\right)$
8 7 ori ${⊢}¬\mathrm{\omega }\in \mathrm{On}\to \mathrm{\omega }=\mathrm{On}$
9 6 8 nsyl2 ${⊢}\left({A}\in \mathrm{On}\wedge \mathrm{\omega }\subseteq {A}\right)\to \mathrm{\omega }\in \mathrm{On}$
10 id ${⊢}{x}=\mathrm{\omega }\to {x}=\mathrm{\omega }$
11 suceq ${⊢}{x}=\mathrm{\omega }\to \mathrm{suc}{x}=\mathrm{suc}\mathrm{\omega }$
12 10 11 breq12d ${⊢}{x}=\mathrm{\omega }\to \left({x}\approx \mathrm{suc}{x}↔\mathrm{\omega }\approx \mathrm{suc}\mathrm{\omega }\right)$
13 id ${⊢}{x}={y}\to {x}={y}$
14 suceq ${⊢}{x}={y}\to \mathrm{suc}{x}=\mathrm{suc}{y}$
15 13 14 breq12d ${⊢}{x}={y}\to \left({x}\approx \mathrm{suc}{x}↔{y}\approx \mathrm{suc}{y}\right)$
16 id ${⊢}{x}=\mathrm{suc}{y}\to {x}=\mathrm{suc}{y}$
17 suceq ${⊢}{x}=\mathrm{suc}{y}\to \mathrm{suc}{x}=\mathrm{suc}\mathrm{suc}{y}$
18 16 17 breq12d ${⊢}{x}=\mathrm{suc}{y}\to \left({x}\approx \mathrm{suc}{x}↔\mathrm{suc}{y}\approx \mathrm{suc}\mathrm{suc}{y}\right)$
19 id ${⊢}{x}={A}\to {x}={A}$
20 suceq ${⊢}{x}={A}\to \mathrm{suc}{x}=\mathrm{suc}{A}$
21 19 20 breq12d ${⊢}{x}={A}\to \left({x}\approx \mathrm{suc}{x}↔{A}\approx \mathrm{suc}{A}\right)$
22 limom ${⊢}\mathrm{Lim}\mathrm{\omega }$
23 22 limensuci ${⊢}\mathrm{\omega }\in \mathrm{On}\to \mathrm{\omega }\approx \mathrm{suc}\mathrm{\omega }$
24 vex ${⊢}{y}\in \mathrm{V}$
25 24 sucex ${⊢}\mathrm{suc}{y}\in \mathrm{V}$
26 en2sn ${⊢}\left({y}\in \mathrm{V}\wedge \mathrm{suc}{y}\in \mathrm{V}\right)\to \left\{{y}\right\}\approx \left\{\mathrm{suc}{y}\right\}$
27 24 25 26 mp2an ${⊢}\left\{{y}\right\}\approx \left\{\mathrm{suc}{y}\right\}$
28 eloni ${⊢}{y}\in \mathrm{On}\to \mathrm{Ord}{y}$
29 ordirr ${⊢}\mathrm{Ord}{y}\to ¬{y}\in {y}$
30 28 29 syl ${⊢}{y}\in \mathrm{On}\to ¬{y}\in {y}$
31 disjsn ${⊢}{y}\cap \left\{{y}\right\}=\varnothing ↔¬{y}\in {y}$
32 30 31 sylibr ${⊢}{y}\in \mathrm{On}\to {y}\cap \left\{{y}\right\}=\varnothing$
33 eloni ${⊢}\mathrm{suc}{y}\in \mathrm{On}\to \mathrm{Ord}\mathrm{suc}{y}$
34 ordirr ${⊢}\mathrm{Ord}\mathrm{suc}{y}\to ¬\mathrm{suc}{y}\in \mathrm{suc}{y}$
35 33 34 syl ${⊢}\mathrm{suc}{y}\in \mathrm{On}\to ¬\mathrm{suc}{y}\in \mathrm{suc}{y}$
36 sucelon ${⊢}{y}\in \mathrm{On}↔\mathrm{suc}{y}\in \mathrm{On}$
37 disjsn ${⊢}\mathrm{suc}{y}\cap \left\{\mathrm{suc}{y}\right\}=\varnothing ↔¬\mathrm{suc}{y}\in \mathrm{suc}{y}$
38 35 36 37 3imtr4i ${⊢}{y}\in \mathrm{On}\to \mathrm{suc}{y}\cap \left\{\mathrm{suc}{y}\right\}=\varnothing$
39 32 38 jca ${⊢}{y}\in \mathrm{On}\to \left({y}\cap \left\{{y}\right\}=\varnothing \wedge \mathrm{suc}{y}\cap \left\{\mathrm{suc}{y}\right\}=\varnothing \right)$
40 unen ${⊢}\left(\left({y}\approx \mathrm{suc}{y}\wedge \left\{{y}\right\}\approx \left\{\mathrm{suc}{y}\right\}\right)\wedge \left({y}\cap \left\{{y}\right\}=\varnothing \wedge \mathrm{suc}{y}\cap \left\{\mathrm{suc}{y}\right\}=\varnothing \right)\right)\to \left({y}\cup \left\{{y}\right\}\right)\approx \left(\mathrm{suc}{y}\cup \left\{\mathrm{suc}{y}\right\}\right)$
41 df-suc ${⊢}\mathrm{suc}{y}={y}\cup \left\{{y}\right\}$
42 df-suc ${⊢}\mathrm{suc}\mathrm{suc}{y}=\mathrm{suc}{y}\cup \left\{\mathrm{suc}{y}\right\}$
43 40 41 42 3brtr4g ${⊢}\left(\left({y}\approx \mathrm{suc}{y}\wedge \left\{{y}\right\}\approx \left\{\mathrm{suc}{y}\right\}\right)\wedge \left({y}\cap \left\{{y}\right\}=\varnothing \wedge \mathrm{suc}{y}\cap \left\{\mathrm{suc}{y}\right\}=\varnothing \right)\right)\to \mathrm{suc}{y}\approx \mathrm{suc}\mathrm{suc}{y}$
44 43 ex ${⊢}\left({y}\approx \mathrm{suc}{y}\wedge \left\{{y}\right\}\approx \left\{\mathrm{suc}{y}\right\}\right)\to \left(\left({y}\cap \left\{{y}\right\}=\varnothing \wedge \mathrm{suc}{y}\cap \left\{\mathrm{suc}{y}\right\}=\varnothing \right)\to \mathrm{suc}{y}\approx \mathrm{suc}\mathrm{suc}{y}\right)$
45 39 44 syl5 ${⊢}\left({y}\approx \mathrm{suc}{y}\wedge \left\{{y}\right\}\approx \left\{\mathrm{suc}{y}\right\}\right)\to \left({y}\in \mathrm{On}\to \mathrm{suc}{y}\approx \mathrm{suc}\mathrm{suc}{y}\right)$
46 27 45 mpan2 ${⊢}{y}\approx \mathrm{suc}{y}\to \left({y}\in \mathrm{On}\to \mathrm{suc}{y}\approx \mathrm{suc}\mathrm{suc}{y}\right)$
47 46 com12 ${⊢}{y}\in \mathrm{On}\to \left({y}\approx \mathrm{suc}{y}\to \mathrm{suc}{y}\approx \mathrm{suc}\mathrm{suc}{y}\right)$
48 47 ad2antrr ${⊢}\left(\left({y}\in \mathrm{On}\wedge \mathrm{\omega }\in \mathrm{On}\right)\wedge \mathrm{\omega }\subseteq {y}\right)\to \left({y}\approx \mathrm{suc}{y}\to \mathrm{suc}{y}\approx \mathrm{suc}\mathrm{suc}{y}\right)$
49 vex ${⊢}{x}\in \mathrm{V}$
50 limensuc ${⊢}\left({x}\in \mathrm{V}\wedge \mathrm{Lim}{x}\right)\to {x}\approx \mathrm{suc}{x}$
51 49 50 mpan ${⊢}\mathrm{Lim}{x}\to {x}\approx \mathrm{suc}{x}$
52 51 ad2antrr ${⊢}\left(\left(\mathrm{Lim}{x}\wedge \mathrm{\omega }\in \mathrm{On}\right)\wedge \mathrm{\omega }\subseteq {x}\right)\to {x}\approx \mathrm{suc}{x}$
53 52 a1d ${⊢}\left(\left(\mathrm{Lim}{x}\wedge \mathrm{\omega }\in \mathrm{On}\right)\wedge \mathrm{\omega }\subseteq {x}\right)\to \left(\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\left(\mathrm{\omega }\subseteq {y}\to {y}\approx \mathrm{suc}{y}\right)\to {x}\approx \mathrm{suc}{x}\right)$
54 12 15 18 21 23 48 53 tfindsg ${⊢}\left(\left({A}\in \mathrm{On}\wedge \mathrm{\omega }\in \mathrm{On}\right)\wedge \mathrm{\omega }\subseteq {A}\right)\to {A}\approx \mathrm{suc}{A}$
55 54 exp31 ${⊢}{A}\in \mathrm{On}\to \left(\mathrm{\omega }\in \mathrm{On}\to \left(\mathrm{\omega }\subseteq {A}\to {A}\approx \mathrm{suc}{A}\right)\right)$
56 55 com23 ${⊢}{A}\in \mathrm{On}\to \left(\mathrm{\omega }\subseteq {A}\to \left(\mathrm{\omega }\in \mathrm{On}\to {A}\approx \mathrm{suc}{A}\right)\right)$
57 56 imp ${⊢}\left({A}\in \mathrm{On}\wedge \mathrm{\omega }\subseteq {A}\right)\to \left(\mathrm{\omega }\in \mathrm{On}\to {A}\approx \mathrm{suc}{A}\right)$
58 9 57 mpd ${⊢}\left({A}\in \mathrm{On}\wedge \mathrm{\omega }\subseteq {A}\right)\to {A}\approx \mathrm{suc}{A}$