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