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

Theorem ordirr 4735
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 4732 . 2  |-  ( Ord 
A  ->  _E  Fr  A )
2 efrirr 4699 . 2  |-  (  _E  Fr  A  ->  -.  A  e.  A )
31, 2syl 16 1  |-  ( Ord 
A  ->  -.  A  e.  A )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    e. wcel 1756    _E cep 4628    Fr wfr 4674   Ord word 4716
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2422  ax-sep 4411  ax-nul 4419  ax-pr 4529
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-ral 2718  df-rex 2719  df-rab 2722  df-v 2972  df-sbc 3185  df-dif 3329  df-un 3331  df-in 3333  df-ss 3340  df-nul 3636  df-if 3790  df-sn 3876  df-pr 3878  df-op 3882  df-br 4291  df-opab 4349  df-eprel 4630  df-fr 4677  df-we 4679  df-ord 4720
This theorem is referenced by:  nordeq  4736  ordn2lp  4737  ordtri3or  4749  ordtri1  4750  ordtri3  4753  orddisj  4755  ordunidif  4765  ordnbtwn  4807  onirri  4823  onssneli  4826  onprc  6394  nlimsucg  6451  nnlim  6487  limom  6489  smo11  6823  smoord  6824  tfrlem13  6847  omopth2  7021  limensuci  7485  infensuc  7487  ordtypelem9  7738  cantnfp1lem3  7886  cantnfp1  7887  oemapvali  7890  cantnfp1lem3OLD  7912  cantnfp1OLD  7913  tskwe  8118  dif1card  8175  pm110.643ALT  8345  pwsdompw  8371  cflim2  8430  fin23lem24  8489  fin23lem26  8492  axdc3lem4  8620  ttukeylem7  8682  canthp1lem2  8818  inar1  8940  gruina  8983  grur1  8985  addnidpi  9068  fzennn  11788  hashp1i  12159  soseq  27713
  Copyright terms: Public domain W3C validator