Theorem ordirr 6370

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2108   E cep 5552   Fr wfr 5603  Ord word 6351

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-br 5120  df-opab 5182  df-eprel 5553  df-fr 5606  df-we 5608  df-ord 6355

This theorem is referenced by:  nordeq  6371  ordn2lp  6372  ordtri3or  6384  ordtri1  6385  ordtri3  6388  orddisj  6390  ordunidif  6402  ordnbtwn  6447  onirri  6467  onssneli  6470  epweon  7769  onprc  7772  nlimsucg  7837  nnlim  7875  limom  7877  soseq  8158  smo11  8378  smoord  8379  tfrlem13  8404  omopth2  8596  cofonr  8686  naddcllem  8688  limensuci  9167  infensuc  9169  ordtypelem9  9540  cantnfp1lem3  9694  cantnfp1  9695  oemapvali  9698  tskwe  9964  dif1card  10024  dju1p1e2ALT  10189  nnadju  10212  pwsdompw  10217  cflim2  10277  fin23lem24  10336  fin23lem26  10339  axdc3lem4  10467  ttukeylem7  10529  canthp1lem2  10667  inar1  10789  gruina  10832  grur1  10834  addnidpi  10915  fzennn  13986  hashp1i  14421  noseponlem  27628  noextend  27630  noextenddif  27632  noextendlt  27633  noextendgt  27634  fvnobday  27642  nosepssdm  27650  nosupbnd1lem3  27674  nosupbnd1lem5  27676  nosupbnd2lem1  27679  noinfbnd1lem3  27689  noinfbnd1lem5  27691  noinfbnd2lem1  27694  noetasuplem4  27700  noetainflem4  27704  sucneqond  37383  oaordnrex  43319  omnord1ex  43328  oenord1ex  43339  cantnfresb  43348  tfsconcatb0  43368  nlimsuc  43465