Metamath Proof Explorer

Theorem oaordnr

Description: When the same ordinal is added on the right, ordering of the sums is not equivalent to the ordering of the ordinals on the left. Remark 3.9 of Schloeder p. 8. (Contributed by RP, 29-Jan-2025)

Ref Expression
Assertion oaordnr ⊢ ∃ a ∈ On ∃ b ∈ On ∃ c ∈ On ¬ a ∈ b ↔ a + 𝑜 c ∈ b + 𝑜 c

Proof

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