![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ordirr | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
ordirr | ⊢ (Ord 𝐴 → ¬ 𝐴 ∈ 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ordfr 6401 | . 2 ⊢ (Ord 𝐴 → E Fr 𝐴) | |
2 | efrirr 5669 | . 2 ⊢ ( E Fr 𝐴 → ¬ 𝐴 ∈ 𝐴) | |
3 | 1, 2 | syl 17 | 1 ⊢ (Ord 𝐴 → ¬ 𝐴 ∈ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∈ wcel 2106 E cep 5588 Fr wfr 5638 Ord word 6385 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-ext 2706 ax-sep 5302 ax-nul 5312 ax-pr 5438 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1540 df-fal 1550 df-ex 1777 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 df-ne 2939 df-ral 3060 df-rex 3069 df-rab 3434 df-v 3480 df-dif 3966 df-un 3968 df-ss 3980 df-nul 4340 df-if 4532 df-pw 4607 df-sn 4632 df-pr 4634 df-op 4638 df-br 5149 df-opab 5211 df-eprel 5589 df-fr 5641 df-we 5643 df-ord 6389 |
This theorem is referenced by: nordeq 6405 ordn2lp 6406 ordtri3or 6418 ordtri1 6419 ordtri3 6422 orddisj 6424 ordunidif 6435 ordnbtwn 6479 onirri 6499 onssneli 6502 epweon 7794 onprc 7797 nlimsucg 7863 nnlim 7901 limom 7903 soseq 8183 smo11 8403 smoord 8404 tfrlem13 8429 omopth2 8621 cofonr 8711 naddcllem 8713 limensuci 9192 infensuc 9194 ordtypelem9 9564 cantnfp1lem3 9718 cantnfp1 9719 oemapvali 9722 tskwe 9988 dif1card 10048 dju1p1e2ALT 10213 nnadju 10236 pwsdompw 10241 cflim2 10301 fin23lem24 10360 fin23lem26 10363 axdc3lem4 10491 ttukeylem7 10553 canthp1lem2 10691 inar1 10813 gruina 10856 grur1 10858 addnidpi 10939 fzennn 14006 hashp1i 14439 noseponlem 27724 noextend 27726 noextenddif 27728 noextendlt 27729 noextendgt 27730 fvnobday 27738 nosepssdm 27746 nosupbnd1lem3 27770 nosupbnd1lem5 27772 nosupbnd2lem1 27775 noinfbnd1lem3 27785 noinfbnd1lem5 27787 noinfbnd2lem1 27790 noetasuplem4 27796 noetainflem4 27800 sucneqond 37348 oaordnrex 43285 omnord1ex 43294 oenord1ex 43305 cantnfresb 43314 tfsconcatb0 43334 nlimsuc 43431 |
Copyright terms: Public domain | W3C validator |