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

Theorem ordirr 4409
Description: Epsilon irreflexivity of ordinals: no ordinal class is a member of itself. Theorem 2.2(i) of [BellMachover] p. 469, generalized to classes. We prove this without invoking the Axiom of Regularity. (Contributed by NM, 2-Jan-1994.)
Assertion
Ref Expression
ordirr  |-  ( Ord 
A  ->  -.  A  e.  A )

Proof of Theorem ordirr
StepHypRef Expression
1 ordfr 4406 . 2  |-  ( Ord 
A  ->  _E  Fr  A )
2 efrirr 4373 . 2  |-  (  _E  Fr  A  ->  -.  A  e.  A )
31, 2syl 15 1  |-  ( Ord 
A  ->  -.  A  e.  A )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    e. wcel 1685    _E cep 4302    Fr wfr 4348   Ord word 4390
This theorem is referenced by:  nordeq  4410  ordn2lp  4411  ordtri3or  4423  ordtri1  4424  ordtri3  4427  orddisj  4429  ordunidif  4439  ordnbtwn  4482  onirri  4498  onssneli  4501  onprc  4575  nlimsucg  4632  nnlim  4668  limom  4670  smo11  6377  smoord  6378  tfrlem13  6402  omopth2  6578  limensuci  7033  infensuc  7035  ordtypelem9  7237  cantnfp1lem3  7378  cantnfp1  7379  oemapvali  7382  wfelirr  7493  tskwe  7579  dif1card  7634  pm110.643ALT  7800  pwsdompw  7826  cflim2  7885  fin23lem24  7944  fin23lem26  7947  axdc3lem4  8075  ttukeylem7  8138  canthp1lem2  8271  inar1  8393  gruina  8436  grur1  8438  addnidpi  8521  fzennn  11026  hashp1i  11365  soseq  23658  hfninf  24226
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-14 1689  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265  ax-sep 4142  ax-nul 4150  ax-pr 4213
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1631  df-eu 2148  df-mo 2149  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-ne 2449  df-ral 2549  df-rex 2550  df-rab 2553  df-v 2791  df-sbc 2993  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-nul 3457  df-if 3567  df-sn 3647  df-pr 3648  df-op 3650  df-br 4025  df-opab 4079  df-eprel 4304  df-fr 4351  df-we 4353  df-ord 4394
  Copyright terms: Public domain W3C validator