![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ordirr | Structured version Visualization version GIF version |
Description: Epsilon irreflexivity of ordinals: no ordinal class is a member of itself. Theorem 2.2(i) of [BellMachover] p. 469, generalized to classes. 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 6044 | . 2 ⊢ (Ord 𝐴 → E Fr 𝐴) | |
2 | efrirr 5388 | . 2 ⊢ ( E Fr 𝐴 → ¬ 𝐴 ∈ 𝐴) | |
3 | 1, 2 | syl 17 | 1 ⊢ (Ord 𝐴 → ¬ 𝐴 ∈ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∈ wcel 2050 E cep 5316 Fr wfr 5363 Ord word 6028 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-13 2301 ax-ext 2750 ax-sep 5060 ax-nul 5067 ax-pr 5186 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-mo 2547 df-eu 2584 df-clab 2759 df-cleq 2771 df-clel 2846 df-nfc 2918 df-ne 2968 df-ral 3093 df-rex 3094 df-rab 3097 df-v 3417 df-sbc 3682 df-dif 3832 df-un 3834 df-in 3836 df-ss 3843 df-nul 4179 df-if 4351 df-sn 4442 df-pr 4444 df-op 4448 df-br 4930 df-opab 4992 df-eprel 5317 df-fr 5366 df-we 5368 df-ord 6032 |
This theorem is referenced by: nordeq 6048 ordn2lp 6049 ordtri3or 6061 ordtri1 6062 ordtri3 6065 orddisj 6067 ordunidif 6077 ordnbtwn 6119 onirri 6135 onssneli 6138 onprc 7315 nlimsucg 7373 nnlim 7409 limom 7411 smo11 7805 smoord 7806 tfrlem13 7830 omopth2 8011 limensuci 8489 infensuc 8491 ordtypelem9 8785 cantnfp1lem3 8937 cantnfp1 8938 oemapvali 8941 tskwe 9173 dif1card 9230 dju1p1e2ALT 9398 pwsdompw 9424 cflim2 9483 fin23lem24 9542 fin23lem26 9545 axdc3lem4 9673 ttukeylem7 9735 canthp1lem2 9873 inar1 9995 gruina 10038 grur1 10040 addnidpi 10121 fzennn 13151 hashp1i 13577 soseq 32623 noseponlem 32698 noextend 32700 noextenddif 32702 noextendlt 32703 noextendgt 32704 fvnobday 32710 nosepssdm 32717 nosupbnd1lem3 32737 nosupbnd1lem5 32739 nosupbnd2lem1 32742 noetalem3 32746 sucneqond 34094 |
Copyright terms: Public domain | W3C validator |