Theorem infensuc 3484

Description: Any infinite ordinal is equinumerous to its successor. Exercise 7 of [TakeutiZaring] p. 88.

Assertion

Ref	Expression
infensuc	|- ((A e. On /\ om (_ A) -> A ~~ suc A)

Proof of Theorem infensuc

Step	Hyp	Ref	Expression
1		omelon 3476	. 2 |- om e. On
2		id 9	. . . 4 |- (x = om -> x = om)
3		suceq 2288	. . . 4 |- (x = om -> suc x = suc om)
4	2, 3	breq12d 2073	. . 3 |- (x = om -> (x ~~ suc x <-> om ~~ suc om))
5		id 9	. . . 4 |- (x = y -> x = y)
6		suceq 2288	. . . 4 |- (x = y -> suc x = suc y)
7	5, 6	breq12d 2073	. . 3 |- (x = y -> (x ~~ suc x <-> y ~~ suc y))
8		id 9	. . . 4 |- (x = suc y -> x = suc y)
9		suceq 2288	. . . 4 |- (x = suc y -> suc x = suc suc y)
10	8, 9	breq12d 2073	. . 3 |- (x = suc y -> (x ~~ suc x <-> suc y ~~ suc suc y))
11		id 9	. . . 4 |- (x = A -> x = A)
12		suceq 2288	. . . 4 |- (x = A -> suc x = suc A)
13	11, 12	breq12d 2073	. . 3 |- (x = A -> (x ~~ suc x <-> A ~~ suc A))
14		omensuc 3483	. . . 4 |- om ~~ suc om
15	14	a1i 7	. . 3 |- (om e. On -> om ~~ suc om)
16		visset 1350	. . . . . . 7 |- y e. V
17	16	sucex 2303	. . . . . . 7 |- suc y e. V
18		en2sn 3336	. . . . . . 7 |- ((y e. V /\ suc y e. V) -> {y} ~~ {suc y})
19	16, 17, 18	mp2an 520	. . . . . 6 |- {y} ~~ {suc y}
20		unen 3338	. . . . . . . . 9 |- (((y ~~ suc y /\ {y} ~~ {suc y}) /\ ((y i^i {y}) = (/) /\ (suc y i^i {suc y}) = (/))) -> (y u. {y}) ~~ (suc y u. {suc y}))
21		df-suc 2205	. . . . . . . . 9 |- suc y = (y u. {y})
22		df-suc 2205	. . . . . . . . 9 |- suc suc y = (suc y u. {suc y})
23	20, 21, 22	3brtr4g 2088	. . . . . . . 8 |- (((y ~~ suc y /\ {y} ~~ {suc y}) /\ ((y i^i {y}) = (/) /\ (suc y i^i {suc y}) = (/))) -> suc y ~~ suc suc y)
24	23	exp 291	. . . . . . 7 |- ((y ~~ suc y /\ {y} ~~ {suc y}) -> (((y i^i {y}) = (/) /\ (suc y i^i {suc y}) = (/)) -> suc y ~~ suc suc y))
25		eloni 2209	. . . . . . . . . 10 |- (y e. On -> Ord y)
26		ordeirr 2217	. . . . . . . . . 10 |- (Ord y -> -. y e. y)
27	25, 26	syl 12	. . . . . . . . 9 |- (y e. On -> -. y e. y)
28		disjsn 1836	. . . . . . . . 9 |- ((y i^i {y}) = (/) <-> -. y e. y)
29	27, 28	sylibr 175	. . . . . . . 8 |- (y e. On -> (y i^i {y}) = (/))
30		eloni 2209	. . . . . . . . . 10 |- (suc y e. On -> Ord suc y)
31		ordeirr 2217	. . . . . . . . . 10 |- (Ord suc y -> -. suc y e. suc y)
32	30, 31	syl 12	. . . . . . . . 9 |- (suc y e. On -> -. suc y e. suc y)
33		sucelon 2319	. . . . . . . . 9 |- (y e. On <-> suc y e. On)
34		disjsn 1836	. . . . . . . . 9 |- ((suc y i^i {suc y}) = (/) <-> -. suc y e. suc y)
35	32, 33, 34	3imtr4 192	. . . . . . . 8 |- (y e. On -> (suc y i^i {suc y}) = (/))
36	29, 35	jca 236	. . . . . . 7 |- (y e. On -> ((y i^i {y}) = (/) /\ (suc y i^i {suc y}) = (/)))
37	24, 36	syl5 22	. . . . . 6 |- ((y ~~ suc y /\ {y} ~~ {suc y}) -> (y e. On -> suc y ~~ suc suc y))
38	19, 37	mpan2 519	. . . . 5 |- (y ~~ suc y -> (y e. On -> suc y ~~ suc suc y))
39	38	com12 13	. . . 4 |- (y e. On -> (y ~~ suc y -> suc y ~~ suc suc y))
40	39	ad2antll 320	. . 3 |- (((y e. On /\ om e. On) /\ om (_ y) -> (y ~~ suc y -> suc y ~~ suc suc y))
41		visset 1350	. . . . . 6 |- x e. V
42		limensuc 3402	. . . . . 6 |- ((x e. V /\ Lim x) -> x ~~ suc x)
43	41, 42	mpan 518	. . . . 5 |- (Lim x -> x ~~ suc x)
44	43	ad2antll 320	. . . 4 |- (((Lim x /\ om e. On) /\ om (_ x) -> x ~~ suc x)
45	44	a1d 14	. . 3 |- (((Lim x /\ om e. On) /\ om (_ x) -> (A.y e. x (om (_ y -> y ~~ suc y) -> x ~~ suc x))
46	4, 7, 10, 13, 15, 40, 45	tfindsg 2402	. 2 |- (((A e. On /\ om e. On) /\ om (_ A) -> A ~~ suc A)
47	1, 46	mpan12 530	1 |- ((A e. On /\ om (_ A) -> A ~~ suc A)

Syntax hints:  -. wn 1   -> wi 2   /\ wa 196   = weq 797   e. wel 803   = wceq 1091   e. wcel 1092  A.wral 1201  Vcvv 1348   u. cun 1485   i^i cin 1486   (_ wss 1487  (/)c0 1707  {csn 1808   class class class wbr 2054  Ord word 2198  Oncon0 2199  Lim wlim 2200  suc csuc 2201  omcom 2372   ~~ cen 3271

This theorem is referenced by:  cardlim 3657

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-un 1076  ax-pow 1077  ax-reg 1078  ax-inf 1079

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-3or 582  df-3an 583  df-ex 679  df-sb 853  df-eu 1009  df-mo 1010  df-clab 1093  df-cleq 1097  df-clel 1099  df-ne 1192  df-ral 1205  df-rex 1206  df-rab 1208  df-v 1349  df-sbc 1441  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-pss 1494  df-nul 1708  df-if 1777  df-pw 1799  df-sn 1811  df-pr 1812  df-tp 1814  df-op 1815  df-uni 1920  df-tr 2042  df-br 2063  df-opab 2098  df-eprel 2122  df-id 2125  df-po 2128  df-so 2138  df-fr 2169  df-we 2186  df-ord 2202  df-on 2203  df-lim 2204  df-suc 2205  df-om 2373  df-xp 2424  df-rel 2425  df-cnv 2426  df-co 2427  df-dm 2428  df-rn 2429  df-res 2430  df-ima 2431  df-fun 2432  df-fn 2433  df-f 2434  df-f1 2435  df-fo 2436  df-f1o 2437  df-fv 2438  df-rdg 2970  df-1o 3104  df-er 3200  df-en 3274  df-dom 3275

metamath.org