Theorem ordirr 6382

Description: No ordinal class is a member of itself. In other words, the membership relation is irreflexive on ordinal classes. Theorem 2.2(i) of [BellMachover] p. 469, generalized to classes. Theorem 1.9(i) of [Schloeder] p. 1. We prove this without invoking the Axiom of Regularity. (Contributed by NM, 2-Jan-1994.)

Assertion

Ref	Expression
ordirr	⊢ (Ord 𝐴 → ¬ 𝐴 ∈ 𝐴)

Proof of Theorem ordirr

Step	Hyp	Ref	Expression
1		ordfr 6379	. 2 ⊢ (Ord 𝐴 → E Fr 𝐴)
2		efrirr 5643	. 2 ⊢ ( E Fr 𝐴 → ¬ 𝐴 ∈ 𝐴)
3	1, 2	syl 18	1 ⊢ (Ord 𝐴 → ¬ 𝐴 ∈ 𝐴)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∈ wcel 2146   E cep 5562   Fr wfr 5613  Ord word 6363

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-pr 5406

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-br 5112  df-opab 5176  df-eprel 5563  df-fr 5616  df-we 5618  df-ord 6367

This theorem is used by:  nordeq  6383  ordn2lp  6384  ordtri3or  6397  ordtri1  6398  ordtri3  6401  orddisj  6403  ordunidif  6415  ordnbtwn  6460  onirri  6479  onssneli  6482  epweon  7776  onprc  7779  nlimsucg  7840  nnlim  7878  limom  7880  soseq  8157  smo11  8353  smoord  8354  tfrlem13  8379  omopth2  8571  cofonr  8662  naddcllem  8664  limensuci  9144  infensuc  9146  ordtypelem9  9491  cantnfp1lem3  9652  cantnfp1  9653  oemapvali  9656  tskwe  9948  dif1card  10006  dju1p1e2ALT  10170  nnadju  10193  pwsdompw  10198  cflim2  10258  fin23lem24  10317  fin23lem26  10320  axdc3lem4  10448  ttukeylem7  10510  canthp1lem2  10649  inar1  10771  gruina  10814  grur1  10816  addnidpi  10897  fzennn  14017  hashp1i  14452  noseponlem  27857  noextend  27859  noextenddif  27861  noextendlt  27862  noextendgt  27863  fvnobday  27871  nosepssdm  27879  nosupbnd1lem3  27903  nosupbnd1lem5  27905  nosupbnd2lem1  27908  noinfbnd1lem3  27918  noinfbnd1lem5  27920  noinfbnd2lem1  27923  noetasuplem4  27929  noetainflem4  27933  nmulprop  36695  bj-iomnnom  37936  sucneqond  38044  oaordnrex  44055  omnord1ex  44064  oenord1ex  44075  cantnfresb  44084  omabs2  44092  tfsconcatb0  44104  nlimsuc  44200