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	⊢ { ∅ , { ∅ } , { ∅ , { ∅ } } } ∈ V

Proof

Step	Hyp	Ref	Expression
1		df-tp	⊢ { ∅ , { ∅ } , { ∅ , { ∅ } } } = ( { ∅ , { ∅ } } ∪ { { ∅ , { ∅ } } } )
2		pwpr	⊢ 𝒫 { ∅ , { ∅ } } = ( { ∅ , { ∅ } } ∪ { { { ∅ } } , { ∅ , { ∅ } } } )
3		pp0ex	⊢ { ∅ , { ∅ } } ∈ V
4	3	pwex	⊢ 𝒫 { ∅ , { ∅ } } ∈ V
5	2 4	eqeltrri	⊢ ( { ∅ , { ∅ } } ∪ { { { ∅ } } , { ∅ , { ∅ } } } ) ∈ V
6		snsspr2	⊢ { { ∅ , { ∅ } } } ⊆ { { { ∅ } } , { ∅ , { ∅ } } }
7		unss2	⊢ ( { { ∅ , { ∅ } } } ⊆ { { { ∅ } } , { ∅ , { ∅ } } } → ( { ∅ , { ∅ } } ∪ { { ∅ , { ∅ } } } ) ⊆ ( { ∅ , { ∅ } } ∪ { { { ∅ } } , { ∅ , { ∅ } } } ) )
8	6 7	ax-mp	⊢ ( { ∅ , { ∅ } } ∪ { { ∅ , { ∅ } } } ) ⊆ ( { ∅ , { ∅ } } ∪ { { { ∅ } } , { ∅ , { ∅ } } } )
9	5 8	ssexi	⊢ ( { ∅ , { ∅ } } ∪ { { ∅ , { ∅ } } } ) ∈ V
10	1 9	eqeltri	⊢ { ∅ , { ∅ } , { ∅ , { ∅ } } } ∈ V