Metamath Proof Explorer

Theorem 0we1

Description: The empty set is a well-ordering of ordinal one. (Contributed by Mario Carneiro, 9-Feb-2015)

Ref Expression
Assertion 0we1 
|- (/) We 1o

Proof

Step Hyp Ref Expression
1 br0 
 |-  -. (/) (/) (/)
2 rel0 
 |-  Rel (/)
3 wesn 
 |-  ( Rel (/) -> ( (/) We { (/) } <-> -. (/) (/) (/) ) )
4 2 3 ax-mp 
 |-  ( (/) We { (/) } <-> -. (/) (/) (/) )
5 1 4 mpbir 
 |-  (/) We { (/) }
6 df1o2 
 |-  1o = { (/) }
7 weeq2 
 |-  ( 1o = { (/) } -> ( (/) We 1o <-> (/) We { (/) } ) )
8 6 7 ax-mp 
 |-  ( (/) We 1o <-> (/) We { (/) } )
9 5 8 mpbir 
 |-  (/) We 1o