Theorem ordsuc 6652

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 5447	. . . 4 |- ( A e. _V -> ( A e. On <-> Ord A ) )
2		suceloni 6651	. . . . 5 |- ( A e. On -> suc A e. On )
3		eloni 5449	. . . . 5 |- ( suc A e. On -> Ord suc A )
4	2, 3	syl 17	. . . 4 |- ( A e. On -> Ord suc A )
5	1, 4	syl6bir 232	. . 3 |- ( A e. _V -> ( Ord A -> Ord suc A ) )
6		sucidg 5517	. . . 4 |- ( A e. _V -> A e. suc A )
7		ordelord 5461	. . . . 5 |- ( ( Ord suc A /\ A e. suc A ) -> Ord A )
8	7	ex 435	. . . 4 |- ( Ord suc A -> ( A e. suc A -> Ord A ) )
9	6, 8	syl5com 31	. . 3 |- ( A e. _V -> ( Ord suc A -> Ord A ) )
10	5, 9	impbid 193	. 2 |- ( A e. _V -> ( Ord A <-> Ord suc A ) )
11		sucprc 5514	. . . 4 |- ( -. A e. _V -> suc A = A )
12	11	eqcomd 2430	. . 3 |- ( -. A e. _V -> A = suc A )
13		ordeq 5446	. . 3 |- ( A = suc A -> ( Ord A <-> Ord suc A ) )
14	12, 13	syl 17	. 2 |- ( -. A e. _V -> ( Ord A <-> Ord suc A ) )
15	10, 14	pm2.61i 167	1 |- ( Ord A <-> Ord suc A )

Syntax hints:   -. wn 3   <-> wb 187   = wceq 1437   e. wcel 1868   _Vcvv 3081   Ord word 5438   Oncon0 5439   suc csuc 5441

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4552  ax-pr 4657  ax-un 6594

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-rab 2784  df-v 3083  df-sbc 3300  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3910  df-sn 3997  df-pr 3999  df-tp 4001  df-op 4003  df-uni 4217  df-br 4421  df-opab 4480  df-tr 4516  df-eprel 4761  df-po 4771  df-so 4772  df-fr 4809  df-we 4811  df-ord 5442  df-on 5443  df-suc 5445

This theorem is referenced by:  ordpwsuc  6653  sucelon  6655  ordsucss  6656  onpsssuc  6657  ordsucelsuc  6660  ordsucsssuc  6661  ordsucuniel  6662  ordsucun  6663  onsucuni2  6672  0elsuc  6673  nlimsucg  6680  limsssuc  6688  php4  7762  cantnflt  8179  fin23lem26  8756  hsmexlem1  8857  onsuct0  31094