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 ω ) ≠ ( ω +o 1o )

Proof

Step	Hyp	Ref	Expression
1		omex	⊢ ω ∈ V
2	1	sucid	⊢ ω ∈ suc ω
3		omelon	⊢ ω ∈ On
4		1onn	⊢ 1o ∈ ω
5		oaabslem	⊢ ( ( ω ∈ On ∧ 1o ∈ ω ) → ( 1o +o ω ) = ω )
6	3 4 5	mp2an	⊢ ( 1o +o ω ) = ω
7		oa1suc	⊢ ( ω ∈ On → ( ω +o 1o ) = suc ω )
8	3 7	ax-mp	⊢ ( ω +o 1o ) = suc ω
9	2 6 8	3eltr4i	⊢ ( 1o +o ω ) ∈ ( ω +o 1o )
10		1on	⊢ 1o ∈ On
11		oacl	⊢ ( ( 1o ∈ On ∧ ω ∈ On ) → ( 1o +o ω ) ∈ On )
12	10 3 11	mp2an	⊢ ( 1o +o ω ) ∈ On
13		oacl	⊢ ( ( ω ∈ On ∧ 1o ∈ On ) → ( ω +o 1o ) ∈ On )
14	3 10 13	mp2an	⊢ ( ω +o 1o ) ∈ On
15		onelpss	⊢ ( ( ( 1o +o ω ) ∈ On ∧ ( ω +o 1o ) ∈ On ) → ( ( 1o +o ω ) ∈ ( ω +o 1o ) ↔ ( ( 1o +o ω ) ⊆ ( ω +o 1o ) ∧ ( 1o +o ω ) ≠ ( ω +o 1o ) ) ) )
16	12 14 15	mp2an	⊢ ( ( 1o +o ω ) ∈ ( ω +o 1o ) ↔ ( ( 1o +o ω ) ⊆ ( ω +o 1o ) ∧ ( 1o +o ω ) ≠ ( ω +o 1o ) ) )
17	16	simprbi	⊢ ( ( 1o +o ω ) ∈ ( ω +o 1o ) → ( 1o +o ω ) ≠ ( ω +o 1o ) )
18	9 17	ax-mp	⊢ ( 1o +o ω ) ≠ ( ω +o 1o )