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 ∃ 𝑎 ∈ On ∃ 𝑏 ∈ On ∃ 𝑐 ∈ On ¬ ( 𝑎 ∈ 𝑏 ↔ ( 𝑎 +o 𝑐 ) ∈ ( 𝑏 +o 𝑐 ) )

Proof

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