Theorem omnord1

Description: When the same non-zero ordinal is multiplied on the right, 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, 4-Feb-2025)

	Ref	Expression
Assertion	omnord1	⊢ ∃ 𝑎 ∈ On ∃ 𝑏 ∈ On ∃ 𝑐 ∈ ( On ∖ 1o ) ¬ ( 𝑎 ∈ 𝑏 ↔ ( 𝑎 ·o 𝑐 ) ∈ ( 𝑏 ·o 𝑐 ) )

Proof

Step	Hyp	Ref	Expression
1		omnord1ex	⊢ ¬ ( 1o ∈ 2o ↔ ( 1o ·o ω ) ∈ ( 2o ·o ω ) )
2		1on	⊢ 1o ∈ On
3		2on	⊢ 2o ∈ On
4		omelon	⊢ ω ∈ On
5		peano1	⊢ ∅ ∈ ω
6		ondif1	⊢ ( ω ∈ ( On ∖ 1o ) ↔ ( ω ∈ On ∧ ∅ ∈ ω ) )
7	4 5 6	mpbir2an	⊢ ω ∈ ( On ∖ 1o )
8		oveq2	⊢ ( 𝑐 = ω → ( 1o ·o 𝑐 ) = ( 1o ·o ω ) )
9		oveq2	⊢ ( 𝑐 = ω → ( 2o ·o 𝑐 ) = ( 2o ·o ω ) )
10	8 9	eleq12d	⊢ ( 𝑐 = ω → ( ( 1o ·o 𝑐 ) ∈ ( 2o ·o 𝑐 ) ↔ ( 1o ·o ω ) ∈ ( 2o ·o ω ) ) )
11	10	bibi2d	⊢ ( 𝑐 = ω → ( ( 1o ∈ 2o ↔ ( 1o ·o 𝑐 ) ∈ ( 2o ·o 𝑐 ) ) ↔ ( 1o ∈ 2o ↔ ( 1o ·o ω ) ∈ ( 2o ·o ω ) ) ) )
12	11	notbid	⊢ ( 𝑐 = ω → ( ¬ ( 1o ∈ 2o ↔ ( 1o ·o 𝑐 ) ∈ ( 2o ·o 𝑐 ) ) ↔ ¬ ( 1o ∈ 2o ↔ ( 1o ·o ω ) ∈ ( 2o ·o ω ) ) ) )
13	12	rspcev	⊢ ( ( ω ∈ ( On ∖ 1o ) ∧ ¬ ( 1o ∈ 2o ↔ ( 1o ·o ω ) ∈ ( 2o ·o ω ) ) ) → ∃ 𝑐 ∈ ( On ∖ 1o ) ¬ ( 1o ∈ 2o ↔ ( 1o ·o 𝑐 ) ∈ ( 2o ·o 𝑐 ) ) )
14	7 13	mpan	⊢ ( ¬ ( 1o ∈ 2o ↔ ( 1o ·o ω ) ∈ ( 2o ·o ω ) ) → ∃ 𝑐 ∈ ( On ∖ 1o ) ¬ ( 1o ∈ 2o ↔ ( 1o ·o 𝑐 ) ∈ ( 2o ·o 𝑐 ) ) )
15		eleq2	⊢ ( 𝑏 = 2o → ( 1o ∈ 𝑏 ↔ 1o ∈ 2o ) )
16		oveq1	⊢ ( 𝑏 = 2o → ( 𝑏 ·o 𝑐 ) = ( 2o ·o 𝑐 ) )
17	16	eleq2d	⊢ ( 𝑏 = 2o → ( ( 1o ·o 𝑐 ) ∈ ( 𝑏 ·o 𝑐 ) ↔ ( 1o ·o 𝑐 ) ∈ ( 2o ·o 𝑐 ) ) )
18	15 17	bibi12d	⊢ ( 𝑏 = 2o → ( ( 1o ∈ 𝑏 ↔ ( 1o ·o 𝑐 ) ∈ ( 𝑏 ·o 𝑐 ) ) ↔ ( 1o ∈ 2o ↔ ( 1o ·o 𝑐 ) ∈ ( 2o ·o 𝑐 ) ) ) )
19	18	notbid	⊢ ( 𝑏 = 2o → ( ¬ ( 1o ∈ 𝑏 ↔ ( 1o ·o 𝑐 ) ∈ ( 𝑏 ·o 𝑐 ) ) ↔ ¬ ( 1o ∈ 2o ↔ ( 1o ·o 𝑐 ) ∈ ( 2o ·o 𝑐 ) ) ) )
20	19	rexbidv	⊢ ( 𝑏 = 2o → ( ∃ 𝑐 ∈ ( On ∖ 1o ) ¬ ( 1o ∈ 𝑏 ↔ ( 1o ·o 𝑐 ) ∈ ( 𝑏 ·o 𝑐 ) ) ↔ ∃ 𝑐 ∈ ( On ∖ 1o ) ¬ ( 1o ∈ 2o ↔ ( 1o ·o 𝑐 ) ∈ ( 2o ·o 𝑐 ) ) ) )
21	20	rspcev	⊢ ( ( 2o ∈ On ∧ ∃ 𝑐 ∈ ( On ∖ 1o ) ¬ ( 1o ∈ 2o ↔ ( 1o ·o 𝑐 ) ∈ ( 2o ·o 𝑐 ) ) ) → ∃ 𝑏 ∈ On ∃ 𝑐 ∈ ( On ∖ 1o ) ¬ ( 1o ∈ 𝑏 ↔ ( 1o ·o 𝑐 ) ∈ ( 𝑏 ·o 𝑐 ) ) )
22	3 14 21	sylancr	⊢ ( ¬ ( 1o ∈ 2o ↔ ( 1o ·o ω ) ∈ ( 2o ·o ω ) ) → ∃ 𝑏 ∈ On ∃ 𝑐 ∈ ( On ∖ 1o ) ¬ ( 1o ∈ 𝑏 ↔ ( 1o ·o 𝑐 ) ∈ ( 𝑏 ·o 𝑐 ) ) )
23		eleq1	⊢ ( 𝑎 = 1o → ( 𝑎 ∈ 𝑏 ↔ 1o ∈ 𝑏 ) )
24		oveq1	⊢ ( 𝑎 = 1o → ( 𝑎 ·o 𝑐 ) = ( 1o ·o 𝑐 ) )
25	24	eleq1d	⊢ ( 𝑎 = 1o → ( ( 𝑎 ·o 𝑐 ) ∈ ( 𝑏 ·o 𝑐 ) ↔ ( 1o ·o 𝑐 ) ∈ ( 𝑏 ·o 𝑐 ) ) )
26	23 25	bibi12d	⊢ ( 𝑎 = 1o → ( ( 𝑎 ∈ 𝑏 ↔ ( 𝑎 ·o 𝑐 ) ∈ ( 𝑏 ·o 𝑐 ) ) ↔ ( 1o ∈ 𝑏 ↔ ( 1o ·o 𝑐 ) ∈ ( 𝑏 ·o 𝑐 ) ) ) )
27	26	notbid	⊢ ( 𝑎 = 1o → ( ¬ ( 𝑎 ∈ 𝑏 ↔ ( 𝑎 ·o 𝑐 ) ∈ ( 𝑏 ·o 𝑐 ) ) ↔ ¬ ( 1o ∈ 𝑏 ↔ ( 1o ·o 𝑐 ) ∈ ( 𝑏 ·o 𝑐 ) ) ) )
28	27	rexbidv	⊢ ( 𝑎 = 1o → ( ∃ 𝑐 ∈ ( On ∖ 1o ) ¬ ( 𝑎 ∈ 𝑏 ↔ ( 𝑎 ·o 𝑐 ) ∈ ( 𝑏 ·o 𝑐 ) ) ↔ ∃ 𝑐 ∈ ( On ∖ 1o ) ¬ ( 1o ∈ 𝑏 ↔ ( 1o ·o 𝑐 ) ∈ ( 𝑏 ·o 𝑐 ) ) ) )
29	28	rexbidv	⊢ ( 𝑎 = 1o → ( ∃ 𝑏 ∈ On ∃ 𝑐 ∈ ( On ∖ 1o ) ¬ ( 𝑎 ∈ 𝑏 ↔ ( 𝑎 ·o 𝑐 ) ∈ ( 𝑏 ·o 𝑐 ) ) ↔ ∃ 𝑏 ∈ On ∃ 𝑐 ∈ ( On ∖ 1o ) ¬ ( 1o ∈ 𝑏 ↔ ( 1o ·o 𝑐 ) ∈ ( 𝑏 ·o 𝑐 ) ) ) )
30	29	rspcev	⊢ ( ( 1o ∈ On ∧ ∃ 𝑏 ∈ On ∃ 𝑐 ∈ ( On ∖ 1o ) ¬ ( 1o ∈ 𝑏 ↔ ( 1o ·o 𝑐 ) ∈ ( 𝑏 ·o 𝑐 ) ) ) → ∃ 𝑎 ∈ On ∃ 𝑏 ∈ On ∃ 𝑐 ∈ ( On ∖ 1o ) ¬ ( 𝑎 ∈ 𝑏 ↔ ( 𝑎 ·o 𝑐 ) ∈ ( 𝑏 ·o 𝑐 ) ) )
31	2 22 30	sylancr	⊢ ( ¬ ( 1o ∈ 2o ↔ ( 1o ·o ω ) ∈ ( 2o ·o ω ) ) → ∃ 𝑎 ∈ On ∃ 𝑏 ∈ On ∃ 𝑐 ∈ ( On ∖ 1o ) ¬ ( 𝑎 ∈ 𝑏 ↔ ( 𝑎 ·o 𝑐 ) ∈ ( 𝑏 ·o 𝑐 ) ) )
32	1 31	ax-mp	⊢ ∃ 𝑎 ∈ On ∃ 𝑏 ∈ On ∃ 𝑐 ∈ ( On ∖ 1o ) ¬ ( 𝑎 ∈ 𝑏 ↔ ( 𝑎 ·o 𝑐 ) ∈ ( 𝑏 ·o 𝑐 ) )