![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > onirri | Structured version Visualization version GIF version |
Description: An ordinal number is not a member of itself. Theorem 7M(c) of [Enderton] p. 192. (Contributed by NM, 11-Jun-1994.) |
Ref | Expression |
---|---|
on.1 | ⊢ 𝐴 ∈ On |
Ref | Expression |
---|---|
onirri | ⊢ ¬ 𝐴 ∈ 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | on.1 | . . 3 ⊢ 𝐴 ∈ On | |
2 | 1 | onordi 6177 | . 2 ⊢ Ord 𝐴 |
3 | ordirr 6091 | . 2 ⊢ (Ord 𝐴 → ¬ 𝐴 ∈ 𝐴) | |
4 | 2, 3 | ax-mp 5 | 1 ⊢ ¬ 𝐴 ∈ 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∈ wcel 2083 Ord word 6072 Oncon0 6073 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1781 ax-4 1795 ax-5 1892 ax-6 1951 ax-7 1996 ax-8 2085 ax-9 2093 ax-10 2114 ax-11 2128 ax-12 2143 ax-13 2346 ax-ext 2771 ax-sep 5101 ax-nul 5108 ax-pr 5228 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1082 df-tru 1528 df-ex 1766 df-nf 1770 df-sb 2045 df-mo 2578 df-eu 2614 df-clab 2778 df-cleq 2790 df-clel 2865 df-nfc 2937 df-ne 2987 df-ral 3112 df-rex 3113 df-rab 3116 df-v 3442 df-sbc 3712 df-dif 3868 df-un 3870 df-in 3872 df-ss 3880 df-nul 4218 df-if 4388 df-sn 4479 df-pr 4481 df-op 4485 df-uni 4752 df-br 4969 df-opab 5031 df-tr 5071 df-eprel 5360 df-po 5369 df-so 5370 df-fr 5409 df-we 5411 df-ord 6076 df-on 6077 |
This theorem is referenced by: onssnel2i 6183 onuninsuci 7418 oelim2 8078 omopthlem2 8140 harndom 8881 wfelirr 9107 carduni 9263 pm54.43 9282 alephle 9367 alephfp 9387 pwxpndom2 9940 onsucsuccmpi 33402 onint1 33408 finxpreclem5 34228 wepwsolem 39148 enpr2d 40072 |
Copyright terms: Public domain | W3C validator |