Theorem df2o3

Description: Expanded value of the ordinal number 2. (Contributed by Mario Carneiro, 14-Aug-2015)

	Ref	Expression
Assertion	df2o3	⊢ 2o = { ∅ , 1o }

Proof

Step	Hyp	Ref	Expression
1		df-2o	⊢ 2o = suc 1o
2		df-suc	⊢ suc 1o = ( 1o ∪ { 1o } )
3		df1o2	⊢ 1o = { ∅ }
4	3	uneq1i	⊢ ( 1o ∪ { 1o } ) = ( { ∅ } ∪ { 1o } )
5		df-pr	⊢ { ∅ , 1o } = ( { ∅ } ∪ { 1o } )
6	4 5	eqtr4i	⊢ ( 1o ∪ { 1o } ) = { ∅ , 1o }
7	1 2 6	3eqtri	⊢ 2o = { ∅ , 1o }