Metamath Proof Explorer

Theorem oenord1ex

Description: When ordinals two and three are both raised to the power of omega, ordering of the powers is not equivalent to the ordering of the bases. Remark 3.26 of Schloeder p. 11. (Contributed by RP, 30-Jan-2025)

Ref Expression
Assertion oenord1ex ⊢ ¬ 2 𝑜 ∈ 3 𝑜 ↔ 2 𝑜 ↑ 𝑜 ω ∈ 3 𝑜 ↑ 𝑜 ω

Proof

Step Hyp Ref Expression
1 2oex ⊢ 2 𝑜 ∈ V
2 1 tpid3 ⊢ 2 𝑜 ∈ ∅ 1 𝑜 2 𝑜
3 df3o2 ⊢ 3 𝑜 = ∅ 1 𝑜 2 𝑜
4 2 3 eleqtrri ⊢ 2 𝑜 ∈ 3 𝑜
5 ordom ⊢ Ord ⁡ ω
6 ordirr ⊢ Ord ⁡ ω → ¬ ω ∈ ω
7 2onn ⊢ 2 𝑜 ∈ ω
8 1oex ⊢ 1 𝑜 ∈ V
9 8 prid2 ⊢ 1 𝑜 ∈ ∅ 1 𝑜
10 df2o3 ⊢ 2 𝑜 = ∅ 1 𝑜
11 9 10 eleqtrri ⊢ 1 𝑜 ∈ 2 𝑜
12 nnoeomeqom ⊢ 2 𝑜 ∈ ω ∧ 1 𝑜 ∈ 2 𝑜 → 2 𝑜 ↑ 𝑜 ω = ω
13 7 11 12 mp2an ⊢ 2 𝑜 ↑ 𝑜 ω = ω
14 3onn ⊢ 3 𝑜 ∈ ω
15 8 tpid2 ⊢ 1 𝑜 ∈ ∅ 1 𝑜 2 𝑜
16 15 3 eleqtrri ⊢ 1 𝑜 ∈ 3 𝑜
17 nnoeomeqom ⊢ 3 𝑜 ∈ ω ∧ 1 𝑜 ∈ 3 𝑜 → 3 𝑜 ↑ 𝑜 ω = ω
18 14 16 17 mp2an ⊢ 3 𝑜 ↑ 𝑜 ω = ω
19 13 18 eleq12i ⊢ 2 𝑜 ↑ 𝑜 ω ∈ 3 𝑜 ↑ 𝑜 ω ↔ ω ∈ ω
20 6 19 sylnibr ⊢ Ord ⁡ ω → ¬ 2 𝑜 ↑ 𝑜 ω ∈ 3 𝑜 ↑ 𝑜 ω
21 5 20 ax-mp ⊢ ¬ 2 𝑜 ↑ 𝑜 ω ∈ 3 𝑜 ↑ 𝑜 ω
22 4 21 2th ⊢ 2 𝑜 ∈ 3 𝑜 ↔ ¬ 2 𝑜 ↑ 𝑜 ω ∈ 3 𝑜 ↑ 𝑜 ω
23 xor3 ⊢ ¬ 2 𝑜 ∈ 3 𝑜 ↔ 2 𝑜 ↑ 𝑜 ω ∈ 3 𝑜 ↑ 𝑜 ω ↔ 2 𝑜 ∈ 3 𝑜 ↔ ¬ 2 𝑜 ↑ 𝑜 ω ∈ 3 𝑜 ↑ 𝑜 ω
24 22 23 mpbir ⊢ ¬ 2 𝑜 ∈ 3 𝑜 ↔ 2 𝑜 ↑ 𝑜 ω ∈ 3 𝑜 ↑ 𝑜 ω