Theorem ordon 7776

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 6380	. 2 ⊢ Tr On
2		epweon 7774	. 2 ⊢ E We On
3		df-ord 6360	. 2 ⊢ (Ord On ↔ (Tr On ∧ E We On))
4	1, 2, 3	mpbir2an 711	1 ⊢ Ord On

Syntax hints:  Tr wtr 5234   E cep 5557   We wwe 5610  Ord word 6356  Oncon0 6357

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pr 5407

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-ne 2934  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-pss 3951  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-opab 5187  df-tr 5235  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-ord 6360  df-on 6361

This theorem is referenced by:  onprc  7777  ssorduni  7778  ordeleqon  7781  ordsson  7782  onint  7789  ordsuci  7807  sucexeloniOLD  7809  suceloniOLD  7811  limon  7835  tfi  7853  ordom  7876  ordtypelem2  9538  hartogs  9563  card2on  9573  tskwe  9969  alephsmo  10121  ondomon  10582  dford3lem2  43018  dford3  43019  tfsconcatlem  43327  iunord  49507