omnord1

Description: When the same nonzero 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 ∖ 1_o ) ¬ ( 𝑎 ∈ 𝑏 ↔ ( 𝑎 ·_o 𝑐 ) ∈ ( 𝑏 ·_o 𝑐 ) )

Proof

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

Metamath Proof Explorer

Theorem omnord1

Proof