Theorem onprc 4652

Description: No set contains all ordinal numbers. Proposition 7.13 of [TakeutiZaring] p. 38. 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 4586), 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 4586	. . 3 ⊢ Ord On
2		ordirr 4642	. . 3 ⊢ (Ord On → ¬ On ∈ On)
3	1, 2	ax-mp 5	. 2 ⊢ ¬ On ∈ On
4		elong 4472	. . 3 ⊢ (On ∈ V → (On ∈ On ↔ Ord On))
5	1, 4	mpbiri 168	. 2 ⊢ (On ∈ V → On ∈ On)
6	3, 5	mto 668	1 ⊢ ¬ On ∈ V

Syntax hints:  ¬ wn 3   ∈ wcel 2201  Vcvv 2801  Ord word 4461  Oncon0 4462

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2212  ax-setind 4637

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-clel 2226  df-nfc 2362  df-ne 2402  df-ral 2514  df-rex 2515  df-v 2803  df-dif 3201  df-in 3205  df-ss 3212  df-sn 3676  df-uni 3895  df-tr 4189  df-iord 4465  df-on 4467

This theorem is referenced by:  sucon  4653