Metamath Proof Explorer

Theorem 1oequni2o

Description: The ordinal number 1o is the predecessor of the ordinal number 2o . (Contributed by ML, 19-Oct-2020)

Ref Expression
Assertion 1oequni2o 
|- 1o = U. 2o

Proof

Step Hyp Ref Expression
1 df-2o 
 |-  2o = suc 1o
2 2on 
 |-  2o e. On
3 2on0 
 |-  2o =/= (/)
4 2onn 
 |-  2o e. _om
5 nnlim 
 |-  ( 2o e. _om -> -. Lim 2o )
6 4 5 ax-mp 
 |-  -. Lim 2o
7 onsucuni3 
 |-  ( ( 2o e. On /\ 2o =/= (/) /\ -. Lim 2o ) -> 2o = suc U. 2o )
8 2 3 6 7 mp3an 
 |-  2o = suc U. 2o
9 1 8 eqtr3i 
 |-  suc 1o = suc U. 2o
10 1on 
 |-  1o e. On
11 onuni 
 |-  ( 2o e. On -> U. 2o e. On )
12 2 11 ax-mp 
 |-  U. 2o e. On
13 suc11 
 |-  ( ( 1o e. On /\ U. 2o e. On ) -> ( suc 1o = suc U. 2o <-> 1o = U. 2o ) )
14 10 12 13 mp2an 
 |-  ( suc 1o = suc U. 2o <-> 1o = U. 2o )
15 9 14 mpbi 
 |-  1o = U. 2o