Metamath Proof Explorer


Theorem onnev

Description: The class of ordinal numbers is not equal to the universe. (Contributed by NM, 16-Jun-2007) (Proof shortened by Mario Carneiro, 10-Jan-2013) (Proof shortened by Wolf Lammen, 27-May-2024)

Ref Expression
Assertion onnev On ≠ V

Proof

Step Hyp Ref Expression
1 snsn0non ¬ { { ∅ } } ∈ On
2 snex { { ∅ } } ∈ V
3 id ( On = V → On = V )
4 2 3 eleqtrrid ( On = V → { { ∅ } } ∈ On )
5 1 4 mto ¬ On = V
6 5 neir On ≠ V