![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > onprc | Structured version Visualization version GIF version |
Description: No set contains all ordinal numbers. Proposition 7.13 of [TakeutiZaring] p. 38, but without using the Axiom of Regularity. This is also known as the Burali-Forti paradox (remark in [Enderton] p. 194). In 1897, Cesare Burali-Forti noticed that since the "set" of all ordinal numbers is an ordinal class (ordon 7139), it must be both an element of the set of all ordinal numbers yet greater than every such element. ZF set theory resolves this paradox by not allowing the class of all ordinal numbers to be a set (so instead it is a proper class). Here we prove the denial of its existence. (Contributed by NM, 18-May-1994.) |
Ref | Expression |
---|---|
onprc | ⊢ ¬ On ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ordon 7139 | . . 3 ⊢ Ord On | |
2 | ordirr 5894 | . . 3 ⊢ (Ord On → ¬ On ∈ On) | |
3 | 1, 2 | ax-mp 5 | . 2 ⊢ ¬ On ∈ On |
4 | elong 5884 | . . 3 ⊢ (On ∈ V → (On ∈ On ↔ Ord On)) | |
5 | 1, 4 | mpbiri 248 | . 2 ⊢ (On ∈ V → On ∈ On) |
6 | 3, 5 | mto 188 | 1 ⊢ ¬ On ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∈ wcel 2131 Vcvv 3332 Ord word 5875 Oncon0 5876 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1863 ax-4 1878 ax-5 1980 ax-6 2046 ax-7 2082 ax-8 2133 ax-9 2140 ax-10 2160 ax-11 2175 ax-12 2188 ax-13 2383 ax-ext 2732 ax-sep 4925 ax-nul 4933 ax-pr 5047 ax-un 7106 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1073 df-3an 1074 df-tru 1627 df-ex 1846 df-nf 1851 df-sb 2039 df-eu 2603 df-mo 2604 df-clab 2739 df-cleq 2745 df-clel 2748 df-nfc 2883 df-ne 2925 df-ral 3047 df-rex 3048 df-rab 3051 df-v 3334 df-sbc 3569 df-dif 3710 df-un 3712 df-in 3714 df-ss 3721 df-pss 3723 df-nul 4051 df-if 4223 df-sn 4314 df-pr 4316 df-tp 4318 df-op 4320 df-uni 4581 df-br 4797 df-opab 4857 df-tr 4897 df-eprel 5171 df-po 5179 df-so 5180 df-fr 5217 df-we 5219 df-ord 5879 df-on 5880 |
This theorem is referenced by: ordeleqon 7145 ssonprc 7149 sucon 7165 orduninsuc 7200 omelon2 7234 tfr2b 7653 tz7.48-3 7700 infensuc 8295 zorn2lem4 9505 noprc 32193 |
Copyright terms: Public domain | W3C validator |