Theorem ordsuc 6630

Description: The successor of an ordinal class is ordinal. (Contributed by NM, 3-Apr-1995.)

Assertion

Ref	Expression
ordsuc	|- ( Ord A <-> Ord suc A )

Proof of Theorem ordsuc

Step	Hyp	Ref	Expression
1		elong 4872	. . . 4 |- ( A e. _V -> ( A e. On <-> Ord A ) )
2		suceloni 6629	. . . . 5 |- ( A e. On -> suc A e. On )
3		eloni 4874	. . . . 5 |- ( suc A e. On -> Ord suc A )
4	2, 3	syl 16	. . . 4 |- ( A e. On -> Ord suc A )
5	1, 4	syl6bir 229	. . 3 |- ( A e. _V -> ( Ord A -> Ord suc A ) )
6		sucidg 4942	. . . 4 |- ( A e. _V -> A e. suc A )
7		ordelord 4886	. . . . 5 |- ( ( Ord suc A /\ A e. suc A ) -> Ord A )
8	7	ex 434	. . . 4 |- ( Ord suc A -> ( A e. suc A -> Ord A ) )
9	6, 8	syl5com 30	. . 3 |- ( A e. _V -> ( Ord suc A -> Ord A ) )
10	5, 9	impbid 191	. 2 |- ( A e. _V -> ( Ord A <-> Ord suc A ) )
11		sucprc 4939	. . . 4 |- ( -. A e. _V -> suc A = A )
12	11	eqcomd 2449	. . 3 |- ( -. A e. _V -> A = suc A )
13		ordeq 4871	. . 3 |- ( A = suc A -> ( Ord A <-> Ord suc A ) )
14	12, 13	syl 16	. 2 |- ( -. A e. _V -> ( Ord A <-> Ord suc A ) )
15	10, 14	pm2.61i 164	1 |- ( Ord A <-> Ord suc A )

Syntax hints:   -. wn 3   <-> wb 184   = wceq 1381   e. wcel 1802   _Vcvv 3093   Ord word 4863   Oncon0 4864   suc csuc 4866

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-8 1804  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-sep 4554  ax-nul 4562  ax-pr 4672  ax-un 6573

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 973  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-ral 2796  df-rex 2797  df-rab 2800  df-v 3095  df-sbc 3312  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-pss 3474  df-nul 3768  df-if 3923  df-sn 4011  df-pr 4013  df-tp 4015  df-op 4017  df-uni 4231  df-br 4434  df-opab 4492  df-tr 4527  df-eprel 4777  df-po 4786  df-so 4787  df-fr 4824  df-we 4826  df-ord 4867  df-on 4868  df-suc 4870

This theorem is referenced by:  ordpwsuc  6631  sucelon  6633  ordsucss  6634  onpsssuc  6635  ordsucelsuc  6638  ordsucsssuc  6639  ordsucuniel  6640  ordsucun  6641  onsucuni2  6650  0elsuc  6651  nlimsucg  6658  limsssuc  6666  php4  7702  cantnflt  8089  cantnfltOLD  8119  fin23lem26  8703  hsmexlem1  8804  onsuct0  29874