MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ordon Structured version   Unicode version

Theorem ordon 6505
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
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 tron 4851 . 2  |-  Tr  On
2 onfr 4867 . . 3  |-  _E  Fr  On
3 eloni 4838 . . . . 5  |-  ( x  e.  On  ->  Ord  x )
4 eloni 4838 . . . . 5  |-  ( y  e.  On  ->  Ord  y )
5 ordtri3or 4860 . . . . . 6  |-  ( ( Ord  x  /\  Ord  y )  ->  (
x  e.  y  \/  x  =  y  \/  y  e.  x ) )
6 epel 4744 . . . . . . 7  |-  ( x  _E  y  <->  x  e.  y )
7 biid 236 . . . . . . 7  |-  ( x  =  y  <->  x  =  y )
8 epel 4744 . . . . . . 7  |-  ( y  _E  x  <->  y  e.  x )
96, 7, 83orbi123i 1178 . . . . . 6  |-  ( ( x  _E  y  \/  x  =  y  \/  y  _E  x )  <-> 
( x  e.  y  \/  x  =  y  \/  y  e.  x
) )
105, 9sylibr 212 . . . . 5  |-  ( ( Ord  x  /\  Ord  y )  ->  (
x  _E  y  \/  x  =  y  \/  y  _E  x ) )
113, 4, 10syl2an 477 . . . 4  |-  ( ( x  e.  On  /\  y  e.  On )  ->  ( x  _E  y  \/  x  =  y  \/  y  _E  x
) )
1211rgen2a 2900 . . 3  |-  A. x  e.  On  A. y  e.  On  ( x  _E  y  \/  x  =  y  \/  y  _E  x )
13 dfwe2 6504 . . 3  |-  (  _E  We  On  <->  (  _E  Fr  On  /\  A. x  e.  On  A. y  e.  On  ( x  _E  y  \/  x  =  y  \/  y  _E  x ) ) )
142, 12, 13mpbir2an 911 . 2  |-  _E  We  On
15 df-ord 4831 . 2  |-  ( Ord 
On 
<->  ( Tr  On  /\  _E  We  On ) )
161, 14, 15mpbir2an 911 1  |-  Ord  On
Colors of variables: wff setvar class
Syntax hints:    /\ wa 369    \/ w3o 964    e. wcel 1758   A.wral 2799   class class class wbr 4401   Tr wtr 4494    _E cep 4739    Fr wfr 4785    We wwe 4787   Ord word 4827   Oncon0 4828
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4522  ax-nul 4530  ax-pr 4640  ax-un 6483
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-ral 2804  df-rex 2805  df-rab 2808  df-v 3080  df-sbc 3295  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-pss 3453  df-nul 3747  df-if 3901  df-sn 3987  df-pr 3989  df-tp 3991  df-op 3993  df-uni 4201  df-br 4402  df-opab 4460  df-tr 4495  df-eprel 4741  df-po 4750  df-so 4751  df-fr 4788  df-we 4790  df-ord 4831  df-on 4832
This theorem is referenced by:  epweon  6506  onprc  6507  ssorduni  6508  ordeleqon  6511  ordsson  6512  onint  6517  suceloni  6535  limon  6558  tfi  6575  ordom  6596  ordtypelem2  7845  hartogs  7870  card2on  7881  tskwe  8232  alephsmo  8384  ondomon  8839  dford3lem2  29525  dford3  29526
  Copyright terms: Public domain W3C validator