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

Theorem ordirr 4591
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 4588 . 2  |-  ( Ord 
A  ->  _E  Fr  A )
2 efrirr 4555 . 2  |-  (  _E  Fr  A  ->  -.  A  e.  A )
31, 2syl 16 1  |-  ( Ord 
A  ->  -.  A  e.  A )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    e. wcel 1725    _E cep 4484    Fr wfr 4530   Ord word 4572
This theorem is referenced by:  nordeq  4592  ordn2lp  4593  ordtri3or  4605  ordtri1  4606  ordtri3  4609  orddisj  4611  ordunidif  4621  ordnbtwn  4664  onirri  4680  onssneli  4683  onprc  4757  nlimsucg  4814  nnlim  4850  limom  4852  smo11  6618  smoord  6619  tfrlem13  6643  omopth2  6819  limensuci  7275  infensuc  7277  ordtypelem9  7487  cantnfp1lem3  7628  cantnfp1  7629  oemapvali  7632  tskwe  7829  dif1card  7884  pm110.643ALT  8050  pwsdompw  8076  cflim2  8135  fin23lem24  8194  fin23lem26  8197  axdc3lem4  8325  ttukeylem7  8387  canthp1lem2  8520  inar1  8642  gruina  8685  grur1  8687  addnidpi  8770  fzennn  11299  hashp1i  11664  soseq  25521
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322  ax-nul 4330  ax-pr 4395
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rex 2703  df-rab 2706  df-v 2950  df-sbc 3154  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-br 4205  df-opab 4259  df-eprel 4486  df-fr 4533  df-we 4535  df-ord 4576
  Copyright terms: Public domain W3C validator