Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  onprc Unicode version

Theorem onprc 4719
 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 4717), 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.)
Assertion
Ref Expression
onprc

Proof of Theorem onprc
StepHypRef Expression
1 ordon 4717 . . 3
2 ordirr 4554 . . 3
31, 2ax-mp 8 . 2
4 elong 4544 . . 3
51, 4mpbiri 225 . 2
63, 5mto 169 1
 Colors of variables: wff set class Syntax hints:   wn 3   wcel 1721  cvv 2913   word 4535  con0 4536 This theorem is referenced by:  ordeleqon  4723  ssonprc  4726  sucon  4742  orduninsuc  4777  omelon2  4811  tfr2b  6607  tz7.48-3  6651  abianfp  6666  infensuc  7235  zorn2lem4  8326  noprc  25373 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2382  ax-sep 4285  ax-nul 4293  ax-pr 4358  ax-un 4655 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2256  df-mo 2257  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2526  df-ne 2566  df-ral 2668  df-rex 2669  df-rab 2672  df-v 2915  df-sbc 3119  df-dif 3280  df-un 3282  df-in 3284  df-ss 3291  df-pss 3293  df-nul 3586  df-if 3697  df-sn 3777  df-pr 3778  df-tp 3779  df-op 3780  df-uni 3972  df-br 4168  df-opab 4222  df-tr 4258  df-eprel 4449  df-po 4458  df-so 4459  df-fr 4496  df-we 4498  df-ord 4539  df-on 4540
 Copyright terms: Public domain W3C validator