Theorem onprc 7786

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 7785), 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	⊢ ¬ On ∈ V

Proof of Theorem onprc

Step	Hyp	Ref	Expression
1		ordon 7785	. . 3 ⊢ Ord On
2		ordirr 6385	. . 3 ⊢ (Ord On → ¬ On ∈ On)
3	1, 2	ax-mp 5	. 2 ⊢ ¬ On ∈ On
4		elong 6375	. . 3 ⊢ (On ∈ V → (On ∈ On ↔ Ord On))
5	1, 4	mpbiri 261	. 2 ⊢ (On ∈ V → On ∈ On)
6	3, 5	mto 200	1 ⊢ ¬ On ∈ V

This proof depends on syntax axioms:  ¬ wn 3   ∈ wcel 2146  Vcvv 3458  Ord word 6366  Oncon0 6367

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738  ax-sep 5262  ax-pr 5409

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-ne 2962  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3928  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-tr 5224  df-eprel 5566  df-po 5574  df-so 5575  df-fr 5619  df-we 5621  df-ord 6370  df-on 6371

This theorem is used by:  ordeleqon  7790  ssonprc  7795  sucon  7811  orduninsuc  7848  omelon2  7884  tfr2b  8392  tz7.48-3  8440  infensuc  9153  ordfin  9210  zorn2lem4  10501  noprc  27986  xoromon  35504  fineqvomonb  35556  onvf1od  35615