Theorem suceloni 3069

Description: The successor of an ordinal number is an ordinal number. Proposition 7.24 of [TakeutiZaring] p. 41.

Assertion

Ref	Expression
suceloni	|- (A e. On -> suc A e. On)

Proof of Theorem suceloni

Step	Hyp	Ref	Expression
1		ordon 2994	. . . 4 |- Ord On
2		trssord 2972	. . . . 5 |- ((Tr suc A /\ suc A (_ On /\ Ord On) -> Ord suc A)
3	2	3exp 834	. . . 4 |- (Tr suc A -> (suc A (_ On -> (Ord On -> Ord suc A)))
4	1, 3	mpii 45	. . 3 |- (Tr suc A -> (suc A (_ On -> Ord suc A))
5		onelsst 3007	. . . . . . . 8 |- (A e. On -> (x e. A -> x (_ A))
6		elsn 2426	. . . . . . . . . 10 |- (x e. {A} <-> x = A)
7		eqimss 2113	. . . . . . . . . 10 |- (x = A -> x (_ A)
8	6, 7	sylbi 199	. . . . . . . . 9 |- (x e. {A} -> x (_ A)
9	8	a1i 8	. . . . . . . 8 |- (A e. On -> (x e. {A} -> x (_ A))
10	5, 9	orim12d 567	. . . . . . 7 |- (A e. On -> ((x e. A \/ x e. {A}) -> (x (_ A \/ x (_ A)))
11		df-suc 2961	. . . . . . . . 9 |- suc A = (A u. {A})
12	11	eleq2i 1541	. . . . . . . 8 |- (x e. suc A <-> x e. (A u. {A}))
13		elun 2177	. . . . . . . 8 |- (x e. (A u. {A}) <-> (x e. A \/ x e. {A}))
14	12, 13	bitr2 174	. . . . . . 7 |- ((x e. A \/ x e. {A}) <-> x e. suc A)
15		oridm 243	. . . . . . 7 |- ((x (_ A \/ x (_ A) <-> x (_ A)
16	10, 14, 15	3imtr3g 554	. . . . . 6 |- (A e. On -> (x e. suc A -> x (_ A))
17		sssucid 3054	. . . . . . 7 |- A (_ suc A
18		sstr2 2075	. . . . . . 7 |- (x (_ A -> (A (_ suc A -> x (_ suc A))
19	17, 18	mpi 44	. . . . . 6 |- (x (_ A -> x (_ suc A)
20	16, 19	syl6 22	. . . . 5 |- (A e. On -> (x e. suc A -> x (_ suc A))
21	20	r19.21aiv 1716	. . . 4 |- (A e. On -> A.x e. suc Ax (_ suc A)
22		dftr3 2690	. . . 4 |- (Tr suc A <-> A.x e. suc Ax (_ suc A)
23	21, 22	sylibr 200	. . 3 |- (A e. On -> Tr suc A)
24		onsst 2999	. . . . . 6 |- (A e. On -> A (_ On)
25		snssi 2471	. . . . . 6 |- (A e. On -> {A} (_ On)
26	24, 25	jca 288	. . . . 5 |- (A e. On -> (A (_ On /\ {A} (_ On))
27		unss 2208	. . . . 5 |- ((A (_ On /\ {A} (_ On) <-> (A u. {A}) (_ On)
28	26, 27	sylib 198	. . . 4 |- (A e. On -> (A u. {A}) (_ On)
29	28, 11	syl5ss 2109	. . 3 |- (A e. On -> suc A (_ On)
30	4, 23, 29	sylc 68	. 2 |- (A e. On -> Ord suc A)
31		sucexg 3056	. . 3 |- (A e. On -> suc A e. V)
32		elong 2963	. . 3 |- (suc A e. V -> (suc A e. On <-> Ord suc A))
33	31, 32	syl 10	. 2 |- (A e. On -> (suc A e. On <-> Ord suc A))
34	30, 33	mpbird 196	1 |- (A e. On -> suc A e. On)

Syntax hints:   -> wi 3   <-> wb 146   \/ wo 222   /\ wa 223   = wceq 958   e. wcel 960  A.wral 1648  Vcvv 1814   u. cun 2049   (_ wss 2051  {csn 2414  Tr wtr 2686  Ord word 2954  Oncon0 2955  suc csuc 2957

This theorem is referenced by:  ordsuc 3072  unon 3095  onsuc 3112  ordunisuc2 3122  ordzsl 3123  dfom2 3140  findsg 3164  tfindsg 3169  tfrlem12 3929  oasuc 4170  omsuc 4172  oesuc 4173  oacl 4177  oneo 4219  oelim2 4229  nnacom 4240  nneob 4262  r1ord 4672  rankwflem 4682  rankr1 4691  bndrank 4699  r1pw 4703

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-11 969  ax-12 970  ax-13 971  ax-14 972  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462  ax-sep 2709  ax-pow 2749  ax-pr 2786  ax-un 2873

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 778  df-3an 779  df-ex 983  df-sb 1174  df-eu 1384  df-mo 1385  df-clab 1467  df-cleq 1472  df-clel 1475  df-ne 1590  df-ral 1652  df-rex 1653  df-v 1815  df-dif 2053  df-un 2054  df-in 2055  df-ss 2057  df-nul 2285  df-pw 2407  df-sn 2417  df-pr 2418  df-tp 2420  df-op 2421  df-uni 2509  df-br 2626  df-opab 2673  df-tr 2687  df-eprel 2839  df-po 2847  df-so 2857  df-fr 2924  df-we 2941  df-ord 2958  df-on 2959  df-suc 2961

Copyright terms: Public domain