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	$⊢ 1_{𝑜} +_{𝑜} ω \neq ω +_{𝑜} 1_{𝑜}$

Proof

Step	Hyp	Ref	Expression
1		omex	$⊢ ω \in V$
2	1	sucid	$⊢ ω \in suc ω$
3		omelon	$⊢ ω \in On$
4		1onn	$⊢ 1_{𝑜} \in ω$
5		oaabslem	$⊢ (ω \in On \land 1_{𝑜} \in ω) \to 1_{𝑜} +_{𝑜} ω = ω$
6	3 4 5	mp2an	$⊢ 1_{𝑜} +_{𝑜} ω = ω$
7		oa1suc	$⊢ ω \in On \to ω +_{𝑜} 1_{𝑜} = suc ω$
8	3 7	ax-mp	$⊢ ω +_{𝑜} 1_{𝑜} = suc ω$
9	2 6 8	3eltr4i	$⊢ 1_{𝑜} +_{𝑜} ω \in (ω +_{𝑜} 1_{𝑜})$
10		1on	$⊢ 1_{𝑜} \in On$
11		oacl	$⊢ (1_{𝑜} \in On \land ω \in On) \to 1_{𝑜} +_{𝑜} ω \in On$
12	10 3 11	mp2an	$⊢ 1_{𝑜} +_{𝑜} ω \in On$
13		oacl	$⊢ (ω \in On \land 1_{𝑜} \in On) \to ω +_{𝑜} 1_{𝑜} \in On$
14	3 10 13	mp2an	$⊢ ω +_{𝑜} 1_{𝑜} \in On$
15		onelpss	$⊢ (1_{𝑜} +_{𝑜} ω \in On \land ω +_{𝑜} 1_{𝑜} \in On) \to (1_{𝑜} +_{𝑜} ω \in (ω +_{𝑜} 1_{𝑜}) \leftrightarrow (1_{𝑜} +_{𝑜} ω \subseteq ω +_{𝑜} 1_{𝑜} \land 1_{𝑜} +_{𝑜} ω \neq ω +_{𝑜} 1_{𝑜}))$
16	12 14 15	mp2an	$⊢ 1_{𝑜} +_{𝑜} ω \in (ω +_{𝑜} 1_{𝑜}) \leftrightarrow (1_{𝑜} +_{𝑜} ω \subseteq ω +_{𝑜} 1_{𝑜} \land 1_{𝑜} +_{𝑜} ω \neq ω +_{𝑜} 1_{𝑜})$
17	16	simprbi	$⊢ 1_{𝑜} +_{𝑜} ω \in (ω +_{𝑜} 1_{𝑜}) \to 1_{𝑜} +_{𝑜} ω \neq ω +_{𝑜} 1_{𝑜}$
18	9 17	ax-mp	$⊢ 1_{𝑜} +_{𝑜} ω \neq ω +_{𝑜} 1_{𝑜}$