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

Theorem ordirr 5729
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 𝐴 → ¬ 𝐴𝐴)

Proof of Theorem ordirr
StepHypRef Expression
1 ordfr 5726 . 2 (Ord 𝐴 → E Fr 𝐴)
2 efrirr 5085 . 2 ( E Fr 𝐴 → ¬ 𝐴𝐴)
31, 2syl 17 1 (Ord 𝐴 → ¬ 𝐴𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wcel 1988   E cep 5018   Fr wfr 5060  Ord word 5710
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pr 4897
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-ral 2914  df-rex 2915  df-rab 2918  df-v 3197  df-sbc 3430  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-br 4645  df-opab 4704  df-eprel 5019  df-fr 5063  df-we 5065  df-ord 5714
This theorem is referenced by:  nordeq  5730  ordn2lp  5731  ordtri3or  5743  ordtri1  5744  ordtri3  5747  ordtri3OLD  5748  orddisj  5750  ordunidif  5761  ordnbtwn  5804  ordnbtwnOLD  5805  onirri  5822  onssneli  5825  onprc  6969  nlimsucg  7027  nnlim  7063  limom  7065  smo11  7446  smoord  7447  tfrlem13  7471  omopth2  7649  limensuci  8121  infensuc  8123  ordtypelem9  8416  cantnfp1lem3  8562  cantnfp1  8563  oemapvali  8566  tskwe  8761  dif1card  8818  pm110.643ALT  8985  pwsdompw  9011  cflim2  9070  fin23lem24  9129  fin23lem26  9132  axdc3lem4  9260  ttukeylem7  9322  canthp1lem2  9460  inar1  9582  gruina  9625  grur1  9627  addnidpi  9708  fzennn  12750  hashp1i  13174  soseq  31725  noseponlem  31791  noextend  31793  noextenddif  31795  noextendlt  31796  noextendgt  31797  fvnobday  31803  nosepssdm  31810  nosupbnd1lem3  31830  nosupbnd1lem5  31832  nosupbnd2lem1  31835  noetalem3  31839  sucneqond  33184
  Copyright terms: Public domain W3C validator