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

Theorem ordirr 4412
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 4409 . 2  |-  ( Ord 
A  ->  _E  Fr  A )
2 efrirr 4376 . 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 1686    _E cep 4305    Fr wfr 4351   Ord word 4393
This theorem is referenced by:  nordeq  4413  ordn2lp  4414  ordtri3or  4426  ordtri1  4427  ordtri3  4430  orddisj  4432  ordunidif  4442  ordnbtwn  4485  onirri  4501  onssneli  4504  onprc  4578  nlimsucg  4635  nnlim  4671  limom  4673  smo11  6383  smoord  6384  tfrlem13  6408  omopth2  6584  limensuci  7039  infensuc  7041  ordtypelem9  7243  cantnfp1lem3  7384  cantnfp1  7385  oemapvali  7388  wfelirr  7499  tskwe  7585  dif1card  7640  pm110.643ALT  7806  pwsdompw  7832  cflim2  7891  fin23lem24  7950  fin23lem26  7953  axdc3lem4  8081  ttukeylem7  8144  canthp1lem2  8277  inar1  8399  gruina  8442  grur1  8444  addnidpi  8527  fzennn  11032  hashp1i  11371  soseq  24256  hfninf  24818
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-14 1690  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266  ax-sep 4143  ax-nul 4151  ax-pr 4216
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-eu 2149  df-mo 2150  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-ral 2550  df-rex 2551  df-rab 2554  df-v 2792  df-sbc 2994  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-if 3568  df-sn 3648  df-pr 3649  df-op 3651  df-br 4026  df-opab 4080  df-eprel 4307  df-fr 4354  df-we 4356  df-ord 4397
  Copyright terms: Public domain W3C validator