Theorem onsucb 7829

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

Assertion

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

Proof of Theorem onsucb

Step	Hyp	Ref	Expression
1		ordsuc 7826	. . 3 ⊢ (Ord 𝐴 ↔ Ord suc 𝐴)
2		sucexb 7819	. . 3 ⊢ (𝐴 ∈ V ↔ suc 𝐴 ∈ V)
3	1, 2	anbi12i 640	. 2 ⊢ ((Ord 𝐴 ∧ 𝐴 ∈ V) ↔ (Ord suc 𝐴 ∧ suc 𝐴 ∈ V))
4		elon2 6374	. 2 ⊢ (𝐴 ∈ On ↔ (Ord 𝐴 ∧ 𝐴 ∈ V))
5		elon2 6374	. 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 2145  Vcvv 3451  Ord word 6362  Oncon0 6363  suc csuc 6365

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pr 5391  ax-un 7752

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3900  df-un 3902  df-in 3904  df-ss 3915  df-pss 4035  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-tr 5213  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-ord 6366  df-on 6367  df-suc 6369

This theorem is used by:  onsucmin  7833  tfindsg2  7874  oaordi  8555  oalimcl  8569  omlimcl  8587  omeulem1  8591  oeordsuc  8604  naddcllem  8686  infensuc  9175  cantnflem1b  9688  cantnflem1  9691  r1ordg  9786  alephnbtwn  10151  cfsuc  10336  alephsuc3  10666  alephreg  10668  bdayimaon  28051  nosupbnd1lem1  28066  nosupbnd1  28072  nosupbnd2lem1  28073  nosupbnd2  28074  noinfno  28076  noinfres  28080  noinfbnd1lem1  28081  noinfbnd1  28087  noinfbnd2lem1  28088  noinfbnd2  28089  noeta2  28148  etaslts2  28181