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