Theorem onsucb 7830

Description: A class is an ordinal number if and only if its successor is an ordinal number. Biconditional form of onsuc 7826. (Contributed by NM, 9-Sep-2003.)

Assertion

Ref	Expression
onsucb	⊢ (𝐴 ∈ On ↔ suc 𝐴 ∈ On)

Proof of Theorem onsucb

Step	Hyp	Ref	Expression
1		ordsuc 7827	. . 3 ⊢ (Ord 𝐴 ↔ Ord suc 𝐴)
2		sucexb 7820	. . 3 ⊢ (𝐴 ∈ V ↔ suc 𝐴 ∈ V)
3	1, 2	anbi12i 640	. 2 ⊢ ((Ord 𝐴 ∧ 𝐴 ∈ V) ↔ (Ord suc 𝐴 ∧ suc 𝐴 ∈ V))
4		elon2 6375	. 2 ⊢ (𝐴 ∈ On ↔ (Ord 𝐴 ∧ 𝐴 ∈ V))
5		elon2 6375	. 2 ⊢ (suc 𝐴 ∈ On ↔ (Ord suc 𝐴 ∧ suc 𝐴 ∈ V))
6	3, 4, 5	3bitr4i 306	1 ⊢ (𝐴 ∈ On ↔ suc 𝐴 ∈ On)

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∈ wcel 2144  Vcvv 3450  Ord word 6363  Oncon0 6364  suc csuc 6366

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390  ax-un 7753

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3897  df-pss 4013  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-tr 5212  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-ord 6367  df-on 6368  df-suc 6370

This theorem is used by:  onsucmin  7834  tfindsg2  7875  oaordi  8559  oalimcl  8573  omlimcl  8591  omeulem1  8595  oeordsuc  8608  naddcllem  8690  infensuc  9179  cantnflem1b  9692  cantnflem1  9695  r1ordg  9790  alephnbtwn  10155  cfsuc  10340  alephsuc3  10670  alephreg  10672  bdayimaon  28057  nosupbnd1lem1  28072  nosupbnd1  28078  nosupbnd2lem1  28079  nosupbnd2  28080  noinfno  28082  noinfres  28086  noinfbnd1lem1  28087  noinfbnd1  28093  noinfbnd2lem1  28094  noinfbnd2  28095  noeta2  28154  etaslts2  28187