Theorem onprc 2985

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 2983), 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.

Assertion

Ref	Expression
onprc	|- -. On e. V

Proof of Theorem onprc

Step	Hyp	Ref	Expression
1		ordon 2983	. . 3 |- Ord On
2		ordirr 2962	. . 3 |- (Ord On -> -. On e. On)
3	1, 2	ax-mp 7	. 2 |- -. On e. On
4		elong 2952	. . 3 |- (On e. V -> (On e. On <-> Ord On))
5	1, 4	mpbiri 194	. 2 |- (On e. V -> On e. On)
6	3, 5	mto 106	1 |- -. On e. V

Syntax hints:  -. wn 2   e. wcel 957  Vcvv 1808  Ord word 2943  Oncon0 2944

This theorem is referenced by:  ordeleqon 2986  sucon 3041  ordunisuc 3085  orduninsuc 3110  tz7.48-3 3953  abianfp 3957  omelon 4612  zorn2lem4 4774

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-11 966  ax-12 967  ax-13 968  ax-14 969  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1209  ax-11o 1217  ax-ext 1458  ax-sep 2699  ax-pow 2738  ax-pr 2775  ax-un 2862

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 775  df-3an 776  df-ex 980  df-sb 1171  df-eu 1381  df-mo 1382  df-clab 1463  df-cleq 1468  df-clel 1471  df-ne 1585  df-ral 1647  df-rex 1648  df-v 1809  df-dif 2046  df-un 2047  df-in 2048  df-ss 2050  df-nul 2278  df-pw 2399  df-sn 2409  df-pr 2410  df-tp 2412  df-op 2413  df-uni 2500  df-br 2616  df-opab 2663  df-tr 2677  df-eprel 2828  df-po 2836  df-so 2846  df-fr 2913  df-we 2930  df-ord 2947  df-on 2948

Copyright terms: Public domain