Theorem suceloni 3058

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 2983	. . . 4 |- Ord On
2		trssord 2961	. . . . 5 |- ((Tr suc A /\ suc A (_ On /\ Ord On) -> Ord suc A)
3	2	3exp 831	. . . 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 2996	. . . . . . . 8 |- (A e. On -> (x e. A -> x (_ A))
6		elsn 2418	. . . . . . . . . 10 |- (x e. {A} <-> x = A)
7		eqimss 2106	. . . . . . . . . 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 564	. . . . . . 7 |- (A e. On -> ((x e. A \/ x e. {A}) -> (x (_ A \/ x (_ A)))
11		df-suc 2950	. . . . . . . . 9 |- suc A = (A u. {A})
12	11	eleq2i 1536	. . . . . . . 8 |- (x e. suc A <-> x e. (A u. {A}))
13		elun 2170	. . . . . . . 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 551	. . . . . 6 |- (A e. On -> (x e. suc A -> x (_ A))
17		sssucid 3043	. . . . . . 7 |- A (_ suc A
18		sstr2 2068	. . . . . . 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 1711	. . . 4 |- (A e. On -> A.x e. suc Ax (_ suc A)
22		dftr3 2680	. . . 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 2988	. . . . . 6 |- (A e. On -> A (_ On)
25		snssi 2463	. . . . . 6 |- (A e. On -> {A} (_ On)
26	24, 25	jca 288	. . . . 5 |- (A e. On -> (A (_ On /\ {A} (_ On))
27		unss 2201	. . . . 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 2102	. . 3 |- (A e. On -> suc A (_ On)
30	4, 23, 29	sylc 68	. 2 |- (A e. On -> Ord suc A)
31		sucexg 3045	. . 3 |- (A e. On -> suc A e. V)
32		elong 2952	. . 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 955   e. wcel 957  A.wral 1643  Vcvv 1808   u. cun 2042   (_ wss 2044  {csn 2406  Tr wtr 2676  Ord word 2943  Oncon0 2944  suc csuc 2946

This theorem is referenced by:  ordsuc 3061  unon 3084  onsuc 3101  ordunisuc2 3111  ordzsl 3112  dfom2 3129  findsg 3153  tfindsg 3158  tfrlem12 3917  oasuc 4156  omsuc 4158  oesuc 4159  oacl 4163  oneo 4205  oelim2 4215  nnacom 4226  nneob 4248  r1ord 4638  rankwflem 4648  rankr1 4657  bndrank 4665  r1pw 4669

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-11 966  ax-12 967  ax-13 968  ax-14 969  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1209  ax-11o 1217  ax-ext 1458  ax-sep 2699  ax-pow 2738  ax-pr 2775  ax-un 2862

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 775  df-3an 776  df-ex 980  df-sb 1171  df-eu 1381  df-mo 1382  df-clab 1463  df-cleq 1468  df-clel 1471  df-ne 1585  df-ral 1647  df-rex 1648  df-v 1809  df-dif 2046  df-un 2047  df-in 2048  df-ss 2050  df-nul 2278  df-pw 2399  df-sn 2409  df-pr 2410  df-tp 2412  df-op 2413  df-uni 2500  df-br 2616  df-opab 2663  df-tr 2677  df-eprel 2828  df-po 2836  df-so 2846  df-fr 2913  df-we 2930  df-ord 2947  df-on 2948  df-suc 2950

Copyright terms: Public domain