Theorem ordirr 6406

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∈ wcel 2147   E cep 5557   Fr wfr 5608  Ord word 6387

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5255  ax-pr 5398

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-br 5109  df-opab 5174  df-eprel 5558  df-fr 5611  df-we 5613  df-ord 6391

This theorem is used by:  nordeq  6407  ordn2lp  6408  ordtri3or  6421  ordtri1  6422  ordtri3  6425  orddisj  6427  ordunidif  6439  ordnbtwn  6484  onirri  6503  onssneli  6506  epweon  7821  onprc  7824  onprcr  7825  nlimsucg  7887  nnlim  7925  limom  7927  soseq  8213  smo11  8410  smoord  8411  tfrlem13  8436  omopth2  8630  cofonr  8721  naddcllem  8723  limensuci  9210  infensuc  9212  ordtypelem9  9557  cantnfp1lem3  9718  cantnfp1  9719  oemapvali  9722  tskwe  10068  dif1card  10128  dju1p1e2ALT  10292  nnadju  10315  pwsdompw  10320  cflim2  10380  fin23lem24  10439  fin23lem26  10442  axdc3lem4  10570  ttukeylem7  10632  canthp1lem2  10777  inar1  10899  gruina  10942  grur1  10944  addnidpi  11025  fzennn  14151  hashp1i  14588  noseponlem  28078  noextend  28080  noextenddif  28082  noextendlt  28083  noextendgt  28084  fvnobday  28092  nosepssdm  28100  nosupbnd1lem3  28124  nosupbnd1lem5  28126  nosupbnd2lem1  28129  noinfbnd1lem3  28139  noinfbnd1lem5  28141  noinfbnd2lem1  28144  noetasuplem4  28150  noetainflem4  28154  maxssj0  36047  nmulprop  37154  bj-iomnnom  38448  sucneqond  38556  oaordnrex  44558  omnord1ex  44567  oenord1ex  44578  cantnfresb  44587  omabs2  44595  tfsconcatb0  44607  nlimsuc  44703