Metamath Proof Explorer

Theorem we0

Description: Any relation is a well-ordering of the empty set. (Contributed by NM, 16-Mar-1997)

Ref Expression
Assertion we0 
|- R We (/)

Proof

Step Hyp Ref Expression
1 fr0 
 |-  R Fr (/)
2 so0 
 |-  R Or (/)
3 df-we 
 |-  ( R We (/) <-> ( R Fr (/) /\ R Or (/) ) )
4 1 2 3 mpbir2an 
 |-  R We (/)