Theorem ord3ex

Description: The ordinal number 3 is a set, proved without the Axiom of Union ax-un . (Contributed by NM, 2-May-2009)

	Ref	Expression
Assertion	ord3ex	|- { (/) , { (/) } , { (/) , { (/) } } } e. _V

Proof

Step	Hyp	Ref	Expression
1		df-tp	|- { (/) , { (/) } , { (/) , { (/) } } } = ( { (/) , { (/) } } u. { { (/) , { (/) } } } )
2		pwpr	|- ~P { (/) , { (/) } } = ( { (/) , { (/) } } u. { { { (/) } } , { (/) , { (/) } } } )
3		pp0ex	|- { (/) , { (/) } } e. _V
4	3	pwex	|- ~P { (/) , { (/) } } e. _V
5	2 4	eqeltrri	|- ( { (/) , { (/) } } u. { { { (/) } } , { (/) , { (/) } } } ) e. _V
6		snsspr2	|- { { (/) , { (/) } } } C_ { { { (/) } } , { (/) , { (/) } } }
7		unss2	|- ( { { (/) , { (/) } } } C_ { { { (/) } } , { (/) , { (/) } } } -> ( { (/) , { (/) } } u. { { (/) , { (/) } } } ) C_ ( { (/) , { (/) } } u. { { { (/) } } , { (/) , { (/) } } } ) )
8	6 7	ax-mp	|- ( { (/) , { (/) } } u. { { (/) , { (/) } } } ) C_ ( { (/) , { (/) } } u. { { { (/) } } , { (/) , { (/) } } } )
9	5 8	ssexi	|- ( { (/) , { (/) } } u. { { (/) , { (/) } } } ) e. _V
10	1 9	eqeltri	|- { (/) , { (/) } , { (/) , { (/) } } } e. _V