Metamath Proof Explorer

Theorem onprc

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 ), 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
Assertion onprc ¬ On V


Step Hyp Ref Expression
1 ordon Ord On
2 ordirr Ord On ¬ On On
3 1 2 ax-mp ¬ On On
4 elong On V On On Ord On
5 1 4 mpbiri On V On On
6 3 5 mto ¬ On V