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

Proof

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