Theorem suceloni 7013

Description: The successor of an ordinal number is an ordinal number. Proposition 7.24 of [TakeutiZaring] p. 41. (Contributed by NM, 6-Jun-1994.)

Assertion

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

Proof of Theorem suceloni

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		onelss 5766	. . . . . . . 8 |- ( A e. On -> ( x e. A -> x C_ A ) )
2		velsn 4193	. . . . . . . . . 10 |- ( x e. { A } <-> x = A )
3		eqimss 3657	. . . . . . . . . 10 |- ( x = A -> x C_ A )
4	2, 3	sylbi 207	. . . . . . . . 9 |- ( x e. { A } -> x C_ A )
5	4	a1i 11	. . . . . . . 8 |- ( A e. On -> ( x e. { A } -> x C_ A ) )
6	1, 5	orim12d 883	. . . . . . 7 |- ( A e. On -> ( ( x e. A \/ x e. { A } ) -> ( x C_ A \/ x C_ A ) ) )
7		df-suc 5729	. . . . . . . . 9 |- suc A = ( A u. { A } )
8	7	eleq2i 2693	. . . . . . . 8 |- ( x e. suc A <-> x e. ( A u. { A } ) )
9		elun 3753	. . . . . . . 8 |- ( x e. ( A u. { A } ) <-> ( x e. A \/ x e. { A } ) )
10	8, 9	bitr2i 265	. . . . . . 7 |- ( ( x e. A \/ x e. { A } ) <-> x e. suc A )
11		oridm 536	. . . . . . 7 |- ( ( x C_ A \/ x C_ A ) <-> x C_ A )
12	6, 10, 11	3imtr3g 284	. . . . . 6 |- ( A e. On -> ( x e. suc A -> x C_ A ) )
13		sssucid 5802	. . . . . 6 |- A C_ suc A
14		sstr2 3610	. . . . . 6 |- ( x C_ A -> ( A C_ suc A -> x C_ suc A ) )
15	12, 13, 14	syl6mpi 67	. . . . 5 |- ( A e. On -> ( x e. suc A -> x C_ suc A ) )
16	15	ralrimiv 2965	. . . 4 |- ( A e. On -> A. x e. suc A x C_ suc A )
17		dftr3 4756	. . . 4 |- ( Tr suc A <-> A. x e. suc A x C_ suc A )
18	16, 17	sylibr 224	. . 3 |- ( A e. On -> Tr suc A )
19		onss 6990	. . . . 5 |- ( A e. On -> A C_ On )
20		snssi 4339	. . . . 5 |- ( A e. On -> { A } C_ On )
21	19, 20	unssd 3789	. . . 4 |- ( A e. On -> ( A u. { A } ) C_ On )
22	7, 21	syl5eqss 3649	. . 3 |- ( A e. On -> suc A C_ On )
23		ordon 6982	. . . 4 |- Ord On
24		trssord 5740	. . . . 5 |- ( ( Tr suc A /\ suc A C_ On /\ Ord On ) -> Ord suc A )
25	24	3exp 1264	. . . 4 |- ( Tr suc A -> ( suc A C_ On -> ( Ord On -> Ord suc A ) ) )
26	23, 25	mpii 46	. . 3 |- ( Tr suc A -> ( suc A C_ On -> Ord suc A ) )
27	18, 22, 26	sylc 65	. 2 |- ( A e. On -> Ord suc A )
28		sucexg 7010	. . 3 |- ( A e. On -> suc A e. _V )
29		elong 5731	. . 3 |- ( suc A e. _V -> ( suc A e. On <-> Ord suc A ) )
30	28, 29	syl 17	. 2 |- ( A e. On -> ( suc A e. On <-> Ord suc A ) )
31	27, 30	mpbird 247	1 |- ( A e. On -> suc A e. On )

Syntax hints:   -> wi 4   <-> wb 196   \/ wo 383   = wceq 1483   e. wcel 1990   A.wral 2912   _Vcvv 3200   u. cun 3572   C_ wss 3574   {csn 4177   Tr wtr 4752   Ord word 5722   Oncon0 5723   suc csuc 5725

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-tr 4753  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-ord 5726  df-on 5727  df-suc 5729

This theorem is referenced by:  ordsuc  7014  unon  7031  onsuci  7038  ordunisuc2  7044  ordzsl  7045  onzsl  7046  tfindsg  7060  dfom2  7067  findsg  7093  tfrlem12  7485  oasuc  7604  omsuc  7606  onasuc  7608  oacl  7615  oneo  7661  omeulem1  7662  omeulem2  7663  oeordi  7667  oeworde  7673  oelim2  7675  oelimcl  7680  oeeulem  7681  oeeui  7682  oaabs2  7725  omxpenlem  8061  card2inf  8460  cantnflt  8569  cantnflem1d  8585  cnfcom  8597  r1ordg  8641  bndrank  8704  r1pw  8708  r1pwALT  8709  tcrank  8747  onssnum  8863  dfac12lem2  8966  cfsuc  9079  cfsmolem  9092  fin1a2lem1  9222  fin1a2lem2  9223  ttukeylem7  9337  alephreg  9404  gch2  9497  winainflem  9515  winalim2  9518  r1wunlim  9559  nqereu  9751  noextend  31819  noresle  31846  nosupno  31849  ontgval  32430  ontgsucval  32431  onsuctop  32432  sucneqond  33213  onsetreclem2  42449