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