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

Metamath Proof Explorer

Theorem oancom

Description: Ordinal addition is not commutative. This theorem shows a counterexample. Remark in TakeutiZaring p. 60. (Contributed by NM, 10-Dec-2004)

Ref Expression
Assertion oancom 
|- ( 1o +o _om ) =/= ( _om +o 1o )

Proof

Step Hyp Ref Expression
1 omex 
 |-  _om e. _V
2 1 sucid 
 |-  _om e. suc _om
3 omelon 
 |-  _om e. On
4 1onn 
 |-  1o e. _om
5 oaabslem 
 |-  ( ( _om e. On /\ 1o e. _om ) -> ( 1o +o _om ) = _om )
6 3 4 5 mp2an 
 |-  ( 1o +o _om ) = _om
7 oa1suc 
 |-  ( _om e. On -> ( _om +o 1o ) = suc _om )
8 3 7 ax-mp 
 |-  ( _om +o 1o ) = suc _om
9 2 6 8 3eltr4i 
 |-  ( 1o +o _om ) e. ( _om +o 1o )
10 1on 
 |-  1o e. On
11 oacl 
 |-  ( ( 1o e. On /\ _om e. On ) -> ( 1o +o _om ) e. On )
12 10 3 11 mp2an 
 |-  ( 1o +o _om ) e. On
13 oacl 
 |-  ( ( _om e. On /\ 1o e. On ) -> ( _om +o 1o ) e. On )
14 3 10 13 mp2an 
 |-  ( _om +o 1o ) e. On
15 onelpss 
 |-  ( ( ( 1o +o _om ) e. On /\ ( _om +o 1o ) e. On ) -> ( ( 1o +o _om ) e. ( _om +o 1o ) <-> ( ( 1o +o _om ) C_ ( _om +o 1o ) /\ ( 1o +o _om ) =/= ( _om +o 1o ) ) ) )
16 12 14 15 mp2an 
 |-  ( ( 1o +o _om ) e. ( _om +o 1o ) <-> ( ( 1o +o _om ) C_ ( _om +o 1o ) /\ ( 1o +o _om ) =/= ( _om +o 1o ) ) )
17 16 simprbi 
 |-  ( ( 1o +o _om ) e. ( _om +o 1o ) -> ( 1o +o _om ) =/= ( _om +o 1o ) )
18 9 17 ax-mp 
 |-  ( 1o +o _om ) =/= ( _om +o 1o )