Theorem ordirr 6380

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 6377	. 2 ⊢ (Ord 𝐴 → E Fr 𝐴)
2		efrirr 5630	. 2 ⊢ ( E Fr 𝐴 → ¬ 𝐴 ∈ 𝐴)
3	1, 2	syl 18	1 ⊢ (Ord 𝐴 → ¬ 𝐴 ∈ 𝐴)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∈ wcel 2144   E cep 5549   Fr wfr 5600  Ord word 6361

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-eprel 5550  df-fr 5603  df-we 5605  df-ord 6365

This theorem is used by:  nordeq  6381  ordn2lp  6382  ordtri3or  6395  ordtri1  6396  ordtri3  6399  orddisj  6401  ordunidif  6413  ordnbtwn  6458  onirri  6477  onssneli  6480  epweon  7790  onprc  7793  nlimsucg  7854  nnlim  7892  limom  7894  soseq  8179  smo11  8376  smoord  8377  tfrlem13  8402  omopth2  8596  cofonr  8687  naddcllem  8689  limensuci  9176  infensuc  9178  ordtypelem9  9524  cantnfp1lem3  9685  cantnfp1  9686  oemapvali  9689  tskwe  10035  dif1card  10093  dju1p1e2ALT  10257  nnadju  10280  pwsdompw  10285  cflim2  10345  fin23lem24  10404  fin23lem26  10407  axdc3lem4  10535  ttukeylem7  10597  canthp1lem2  10742  inar1  10864  gruina  10907  grur1  10909  addnidpi  10990  fzennn  14115  hashp1i  14551  noseponlem  28027  noextend  28029  noextenddif  28031  noextendlt  28032  noextendgt  28033  fvnobday  28041  nosepssdm  28049  nosupbnd1lem3  28073  nosupbnd1lem5  28075  nosupbnd2lem1  28078  noinfbnd1lem3  28088  noinfbnd1lem5  28090  noinfbnd2lem1  28093  noetasuplem4  28099  noetainflem4  28103  maxssj0  35946  onprcr  36549  nmulprop  37032  bj-iomnnom  38274  sucneqond  38382  oaordnrex  44391  omnord1ex  44400  oenord1ex  44411  cantnfresb  44420  omabs2  44428  tfsconcatb0  44440  nlimsuc  44536