Theorem ordon 7756

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 6365	. 2 ⊢ Tr On
2		epweon 7754	. 2 ⊢ E We On
3		df-ord 6345	. 2 ⊢ (Ord On ↔ (Tr On ∧ E We On))
4	1, 2, 3	mpbir2an 721	1 ⊢ Ord On

Syntax hints:  Tr wtr 5206   E cep 5544   We wwe 5597  Ord word 6341  Oncon0 6342

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5245  ax-pr 5389

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-tr 5207  df-eprel 5545  df-po 5553  df-so 5554  df-fr 5598  df-we 5600  df-ord 6345  df-on 6346

This theorem is referenced by:  onprc  7757  ssorduni  7758  ordeleqon  7761  ordsson  7762  onint  7769  ordsuci  7787  limon  7812  tfi  7829  ordom  7852  ordtypelem2  9464  hartogs  9489  card2on  9499  tskwe  9905  alephsmo  10055  ondomon  10517  dford3lem2  43568  dford3  43569  tfsconcatlem  43877  iunord  50261