![]() |
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 6368 | . 2 ⊢ (Ord 𝐴 → E Fr 𝐴) | |
2 | efrirr 5650 | . 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 5572 Fr wfr 5621 Ord word 6352 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2702 ax-sep 5292 ax-nul 5299 ax-pr 5420 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-sb 2068 df-clab 2709 df-cleq 2723 df-clel 2809 df-ne 2940 df-ral 3061 df-rex 3070 df-rab 3432 df-v 3475 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-nul 4319 df-if 4523 df-pw 4598 df-sn 4623 df-pr 4625 df-op 4629 df-br 5142 df-opab 5204 df-eprel 5573 df-fr 5624 df-we 5626 df-ord 6356 |
This theorem is referenced by: nordeq 6372 ordn2lp 6373 ordtri3or 6385 ordtri1 6386 ordtri3 6389 orddisj 6391 ordunidif 6402 ordnbtwn 6446 onirri 6466 onssneli 6469 epweon 7745 onprc 7748 nlimsucg 7814 nnlim 7852 limom 7854 soseq 8127 smo11 8346 smoord 8347 tfrlem13 8372 omopth2 8567 cofonr 8656 naddcllem 8658 limensuci 9136 infensuc 9138 ordtypelem9 9503 cantnfp1lem3 9657 cantnfp1 9658 oemapvali 9661 tskwe 9927 dif1card 9987 dju1p1e2ALT 10151 nnadju 10174 pwsdompw 10181 cflim2 10240 fin23lem24 10299 fin23lem26 10302 axdc3lem4 10430 ttukeylem7 10492 canthp1lem2 10630 inar1 10752 gruina 10795 grur1 10797 addnidpi 10878 fzennn 13915 hashp1i 14345 noseponlem 27094 noextend 27096 noextenddif 27098 noextendlt 27099 noextendgt 27100 fvnobday 27108 nosepssdm 27116 nosupbnd1lem3 27140 nosupbnd1lem5 27142 nosupbnd2lem1 27145 noinfbnd1lem3 27155 noinfbnd1lem5 27157 noinfbnd2lem1 27160 noetasuplem4 27166 noetainflem4 27170 sucneqond 36048 oaordnrex 41814 omnord1ex 41823 oenord1ex 41834 cantnfresb 41843 tfsconcatb0 41863 nlimsuc 41961 |
Copyright terms: Public domain | W3C validator |