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