Metamath Proof Explorer

Theorem ord0

Description: The empty set is an ordinal class. Remark 1.5 of Schloeder p. 1. (Contributed by NM, 11-May-1994)

Ref Expression
Assertion ord0 
|- Ord (/)

Proof

Step Hyp Ref Expression
1 tr0 
 |-  Tr (/)
2 we0 
 |-  _E We (/)
3 df-ord 
 |-  ( Ord (/) <-> ( Tr (/) /\ _E We (/) ) )
4 1 2 3 mpbir2an 
 |-  Ord (/)