Theorem ordon 7727

Description: The class of all ordinal numbers is ordinal. Proposition 7.12 of [TakeutiZaring] p. 38, but without using the Axiom of Regularity. (Contributed by NM, 17-May-1994.)

Assertion

Ref	Expression
ordon	⊢ Ord On

Proof of Theorem ordon

Step	Hyp	Ref	Expression
1		tron 6340	. 2 ⊢ Tr On
2		epweon 7725	. 2 ⊢ E We On
3		df-ord 6320	. 2 ⊢ (Ord On ↔ (Tr On ∧ E We On))
4	1, 2, 3	mpbir2an 717	1 ⊢ Ord On

Syntax hints:  Tr wtr 5186   E cep 5524   We wwe 5577  Ord word 6316  Oncon0 6317

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-sep 5225  ax-pr 5369

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ne 2936  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-tr 5187  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-ord 6320  df-on 6321

This theorem is referenced by:  onprc  7728  ssorduni  7729  ordeleqon  7732  ordsson  7733  onint  7740  ordsuci  7758  limon  7783  tfi  7800  ordom  7823  ordtypelem2  9431  hartogs  9456  card2on  9466  tskwe  9872  alephsmo  10022  ondomon  10483  dford3lem2  43479  dford3  43480  tfsconcatlem  43788  iunord  50173