Theorem ordsuc 6511

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 4811	. . . 4 |- ( A e. _V -> ( A e. On <-> Ord A ) )
2		suceloni 6510	. . . . 5 |- ( A e. On -> suc A e. On )
3		eloni 4813	. . . . 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 4881	. . . 4 |- ( A e. _V -> A e. suc A )
7		ordelord 4825	. . . . 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 4878	. . . 4 |- ( -. A e. _V -> suc A = A )
12	11	eqcomd 2457	. . 3 |- ( -. A e. _V -> A = suc A )
13		ordeq 4810	. . 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 1370   e. wcel 1757   _Vcvv 3054   Ord word 4802   Oncon0 4803   suc csuc 4805

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1709  ax-7 1729  ax-8 1759  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2429  ax-sep 4497  ax-nul 4505  ax-pr 4615  ax-un 6458

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1702  df-eu 2263  df-mo 2264  df-clab 2436  df-cleq 2442  df-clel 2445  df-nfc 2598  df-ne 2643  df-ral 2797  df-rex 2798  df-rab 2801  df-v 3056  df-sbc 3271  df-dif 3415  df-un 3417  df-in 3419  df-ss 3426  df-pss 3428  df-nul 3722  df-if 3876  df-sn 3962  df-pr 3964  df-tp 3966  df-op 3968  df-uni 4176  df-br 4377  df-opab 4435  df-tr 4470  df-eprel 4716  df-po 4725  df-so 4726  df-fr 4763  df-we 4765  df-ord 4806  df-on 4807  df-suc 4809

This theorem is referenced by:  ordpwsuc  6512  sucelon  6514  ordsucss  6515  onpsssuc  6516  ordsucelsuc  6519  ordsucsssuc  6520  ordsucuniel  6521  ordsucun  6522  onsucuni2  6531  0elsuc  6532  nlimsucg  6539  limsssuc  6547  php4  7584  cantnflt  7967  cantnfltOLD  7997  fin23lem26  8581  hsmexlem1  8682  onsuct0  28407