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 
|- { (/) , { (/) } , { (/) , { (/) } } } 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