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 )