This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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