Metamath Proof Explorer

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 ⊢ ∃ a ∈ On ∃ b ∈ On ∃ c ∈ On ∖ 1 𝑜 ¬ a ∈ b ↔ a ⋅ 𝑜 c ∈ b ⋅ 𝑜 c

Proof

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