Theorem omnord1ex

Description: When omega is multiplied on the right to ordinals one and two, ordering of the products is not equivalent to the ordering of the ordinals on the left. Remark 3.18 of Schloeder p. 10. (Contributed by RP, 29-Jan-2025)

	Ref	Expression
Assertion	omnord1ex	|- -. ( 1o e. 2o <-> ( 1o .o _om ) e. ( 2o .o _om ) )

Proof

Step	Hyp	Ref	Expression
1		1oelpr	|- 1o e. { (/) , 1o }
2		df2o3	|- 2o = { (/) , 1o }
3	1 2	eleqtrri	|- 1o e. 2o
4		ordom	|- Ord _om
5		ordirr	|- ( Ord _om -> -. _om e. _om )
6		omelon	|- _om e. On
7		1onn	|- 1o e. _om
8		0lt1o	|- (/) e. 1o
9		omabslem	|- ( ( _om e. On /\ 1o e. _om /\ (/) e. 1o ) -> ( 1o .o _om ) = _om )
10	6 7 8 9	mp3an	|- ( 1o .o _om ) = _om
11		2omomeqom	|- ( 2o .o _om ) = _om
12	10 11	eleq12i	|- ( ( 1o .o _om ) e. ( 2o .o _om ) <-> _om e. _om )
13	5 12	sylnibr	|- ( Ord _om -> -. ( 1o .o _om ) e. ( 2o .o _om ) )
14	4 13	ax-mp	|- -. ( 1o .o _om ) e. ( 2o .o _om )
15	3 14	2th	|- ( 1o e. 2o <-> -. ( 1o .o _om ) e. ( 2o .o _om ) )
16		xor3	|- ( -. ( 1o e. 2o <-> ( 1o .o _om ) e. ( 2o .o _om ) ) <-> ( 1o e. 2o <-> -. ( 1o .o _om ) e. ( 2o .o _om ) ) )
17	15 16	mpbir	|- -. ( 1o e. 2o <-> ( 1o .o _om ) e. ( 2o .o _om ) )