![]() |
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 5881 | . 2 ⊢ (Ord 𝐴 → E Fr 𝐴) | |
2 | efrirr 5230 | . 2 ⊢ ( E Fr 𝐴 → ¬ 𝐴 ∈ 𝐴) | |
3 | 1, 2 | syl 17 | 1 ⊢ (Ord 𝐴 → ¬ 𝐴 ∈ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∈ wcel 2145 E cep 5161 Fr wfr 5205 Ord word 5865 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 ax-sep 4915 ax-nul 4923 ax-pr 5034 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 837 df-3an 1073 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-eu 2622 df-mo 2623 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-ne 2944 df-ral 3066 df-rex 3067 df-rab 3070 df-v 3353 df-sbc 3588 df-dif 3726 df-un 3728 df-in 3730 df-ss 3737 df-nul 4064 df-if 4226 df-sn 4317 df-pr 4319 df-op 4323 df-br 4787 df-opab 4847 df-eprel 5162 df-fr 5208 df-we 5210 df-ord 5869 |
This theorem is referenced by: nordeq 5885 ordn2lp 5886 ordtri3or 5898 ordtri1 5899 ordtri3 5902 ordtri3OLD 5903 orddisj 5905 ordunidif 5916 ordnbtwn 5959 ordnbtwnOLD 5960 onirri 5977 onssneli 5980 onprc 7131 nlimsucg 7189 nnlim 7225 limom 7227 smo11 7614 smoord 7615 tfrlem13 7639 omopth2 7818 limensuci 8292 infensuc 8294 ordtypelem9 8587 cantnfp1lem3 8741 cantnfp1 8742 oemapvali 8745 tskwe 8976 dif1card 9033 pm110.643ALT 9202 pwsdompw 9228 cflim2 9287 fin23lem24 9346 fin23lem26 9349 axdc3lem4 9477 ttukeylem7 9539 canthp1lem2 9677 inar1 9799 gruina 9842 grur1 9844 addnidpi 9925 fzennn 12975 hashp1i 13393 soseq 32091 noseponlem 32154 noextend 32156 noextenddif 32158 noextendlt 32159 noextendgt 32160 fvnobday 32166 nosepssdm 32173 nosupbnd1lem3 32193 nosupbnd1lem5 32195 nosupbnd2lem1 32198 noetalem3 32202 sucneqond 33550 |
Copyright terms: Public domain | W3C validator |