Metamath Proof Explorer

Theorem oenord1

Description: When two ordinals (both at least as large as two) are raised to the same power, ordering of the powers is not equivalent to the ordering of the bases. Remark 3.26 of Schloeder p. 11. (Contributed by RP, 4-Feb-2025)

Ref Expression
Assertion oenord1 ⊢ ∃ a ∈ On ∖ 2 𝑜 ∃ b ∈ On ∖ 2 𝑜 ∃ c ∈ On ∖ 1 𝑜 ¬ a ∈ b ↔ a ↑ 𝑜 c ∈ b ↑ 𝑜 c

Proof

Step Hyp Ref Expression
1 oenord1ex ⊢ ¬ 2 𝑜 ∈ 3 𝑜 ↔ 2 𝑜 ↑ 𝑜 ω ∈ 3 𝑜 ↑ 𝑜 ω
2 2on ⊢ 2 𝑜 ∈ On
3 1oex ⊢ 1 𝑜 ∈ V
4 3 prid2 ⊢ 1 𝑜 ∈ ∅ 1 𝑜
5 df2o3 ⊢ 2 𝑜 = ∅ 1 𝑜
6 4 5 eleqtrri ⊢ 1 𝑜 ∈ 2 𝑜
7 ondif2 ⊢ 2 𝑜 ∈ On ∖ 2 𝑜 ↔ 2 𝑜 ∈ On ∧ 1 𝑜 ∈ 2 𝑜
8 2 6 7 mpbir2an ⊢ 2 𝑜 ∈ On ∖ 2 𝑜
9 3on ⊢ 3 𝑜 ∈ On
10 3 tpid2 ⊢ 1 𝑜 ∈ ∅ 1 𝑜 2 𝑜
11 df3o2 ⊢ 3 𝑜 = ∅ 1 𝑜 2 𝑜
12 10 11 eleqtrri ⊢ 1 𝑜 ∈ 3 𝑜
13 ondif2 ⊢ 3 𝑜 ∈ On ∖ 2 𝑜 ↔ 3 𝑜 ∈ On ∧ 1 𝑜 ∈ 3 𝑜
14 9 12 13 mpbir2an ⊢ 3 𝑜 ∈ On ∖ 2 𝑜
15 omelon ⊢ ω ∈ On
16 peano1 ⊢ ∅ ∈ ω
17 ondif1 ⊢ ω ∈ On ∖ 1 𝑜 ↔ ω ∈ On ∧ ∅ ∈ ω
18 15 16 17 mpbir2an ⊢ ω ∈ On ∖ 1 𝑜
19 oveq2 ⊢ c = ω → 2 𝑜 ↑ 𝑜 c = 2 𝑜 ↑ 𝑜 ω
20 oveq2 ⊢ c = ω → 3 𝑜 ↑ 𝑜 c = 3 𝑜 ↑ 𝑜 ω
21 19 20 eleq12d ⊢ c = ω → 2 𝑜 ↑ 𝑜 c ∈ 3 𝑜 ↑ 𝑜 c ↔ 2 𝑜 ↑ 𝑜 ω ∈ 3 𝑜 ↑ 𝑜 ω
22 21 bibi2d ⊢ c = ω → 2 𝑜 ∈ 3 𝑜 ↔ 2 𝑜 ↑ 𝑜 c ∈ 3 𝑜 ↑ 𝑜 c ↔ 2 𝑜 ∈ 3 𝑜 ↔ 2 𝑜 ↑ 𝑜 ω ∈ 3 𝑜 ↑ 𝑜 ω
23 22 notbid ⊢ c = ω → ¬ 2 𝑜 ∈ 3 𝑜 ↔ 2 𝑜 ↑ 𝑜 c ∈ 3 𝑜 ↑ 𝑜 c ↔ ¬ 2 𝑜 ∈ 3 𝑜 ↔ 2 𝑜 ↑ 𝑜 ω ∈ 3 𝑜 ↑ 𝑜 ω
24 23 rspcev ⊢ ω ∈ On ∖ 1 𝑜 ∧ ¬ 2 𝑜 ∈ 3 𝑜 ↔ 2 𝑜 ↑ 𝑜 ω ∈ 3 𝑜 ↑ 𝑜 ω → ∃ c ∈ On ∖ 1 𝑜 ¬ 2 𝑜 ∈ 3 𝑜 ↔ 2 𝑜 ↑ 𝑜 c ∈ 3 𝑜 ↑ 𝑜 c
25 18 24 mpan ⊢ ¬ 2 𝑜 ∈ 3 𝑜 ↔ 2 𝑜 ↑ 𝑜 ω ∈ 3 𝑜 ↑ 𝑜 ω → ∃ c ∈ On ∖ 1 𝑜 ¬ 2 𝑜 ∈ 3 𝑜 ↔ 2 𝑜 ↑ 𝑜 c ∈ 3 𝑜 ↑ 𝑜 c
26 eleq2 ⊢ b = 3 𝑜 → 2 𝑜 ∈ b ↔ 2 𝑜 ∈ 3 𝑜
27 oveq1 ⊢ b = 3 𝑜 → b ↑ 𝑜 c = 3 𝑜 ↑ 𝑜 c
28 27 eleq2d ⊢ b = 3 𝑜 → 2 𝑜 ↑ 𝑜 c ∈ b ↑ 𝑜 c ↔ 2 𝑜 ↑ 𝑜 c ∈ 3 𝑜 ↑ 𝑜 c
29 26 28 bibi12d ⊢ b = 3 𝑜 → 2 𝑜 ∈ b ↔ 2 𝑜 ↑ 𝑜 c ∈ b ↑ 𝑜 c ↔ 2 𝑜 ∈ 3 𝑜 ↔ 2 𝑜 ↑ 𝑜 c ∈ 3 𝑜 ↑ 𝑜 c
30 29 notbid ⊢ b = 3 𝑜 → ¬ 2 𝑜 ∈ b ↔ 2 𝑜 ↑ 𝑜 c ∈ b ↑ 𝑜 c ↔ ¬ 2 𝑜 ∈ 3 𝑜 ↔ 2 𝑜 ↑ 𝑜 c ∈ 3 𝑜 ↑ 𝑜 c
31 30 rexbidv ⊢ b = 3 𝑜 → ∃ c ∈ On ∖ 1 𝑜 ¬ 2 𝑜 ∈ b ↔ 2 𝑜 ↑ 𝑜 c ∈ b ↑ 𝑜 c ↔ ∃ c ∈ On ∖ 1 𝑜 ¬ 2 𝑜 ∈ 3 𝑜 ↔ 2 𝑜 ↑ 𝑜 c ∈ 3 𝑜 ↑ 𝑜 c
32 31 rspcev ⊢ 3 𝑜 ∈ On ∖ 2 𝑜 ∧ ∃ c ∈ On ∖ 1 𝑜 ¬ 2 𝑜 ∈ 3 𝑜 ↔ 2 𝑜 ↑ 𝑜 c ∈ 3 𝑜 ↑ 𝑜 c → ∃ b ∈ On ∖ 2 𝑜 ∃ c ∈ On ∖ 1 𝑜 ¬ 2 𝑜 ∈ b ↔ 2 𝑜 ↑ 𝑜 c ∈ b ↑ 𝑜 c
33 14 25 32 sylancr ⊢ ¬ 2 𝑜 ∈ 3 𝑜 ↔ 2 𝑜 ↑ 𝑜 ω ∈ 3 𝑜 ↑ 𝑜 ω → ∃ b ∈ On ∖ 2 𝑜 ∃ c ∈ On ∖ 1 𝑜 ¬ 2 𝑜 ∈ b ↔ 2 𝑜 ↑ 𝑜 c ∈ b ↑ 𝑜 c
34 eleq1 ⊢ a = 2 𝑜 → a ∈ b ↔ 2 𝑜 ∈ b
35 oveq1 ⊢ a = 2 𝑜 → a ↑ 𝑜 c = 2 𝑜 ↑ 𝑜 c
36 35 eleq1d ⊢ a = 2 𝑜 → a ↑ 𝑜 c ∈ b ↑ 𝑜 c ↔ 2 𝑜 ↑ 𝑜 c ∈ b ↑ 𝑜 c
37 34 36 bibi12d ⊢ a = 2 𝑜 → a ∈ b ↔ a ↑ 𝑜 c ∈ b ↑ 𝑜 c ↔ 2 𝑜 ∈ b ↔ 2 𝑜 ↑ 𝑜 c ∈ b ↑ 𝑜 c
38 37 notbid ⊢ a = 2 𝑜 → ¬ a ∈ b ↔ a ↑ 𝑜 c ∈ b ↑ 𝑜 c ↔ ¬ 2 𝑜 ∈ b ↔ 2 𝑜 ↑ 𝑜 c ∈ b ↑ 𝑜 c
39 38 2rexbidv ⊢ a = 2 𝑜 → ∃ b ∈ On ∖ 2 𝑜 ∃ c ∈ On ∖ 1 𝑜 ¬ a ∈ b ↔ a ↑ 𝑜 c ∈ b ↑ 𝑜 c ↔ ∃ b ∈ On ∖ 2 𝑜 ∃ c ∈ On ∖ 1 𝑜 ¬ 2 𝑜 ∈ b ↔ 2 𝑜 ↑ 𝑜 c ∈ b ↑ 𝑜 c
40 39 rspcev ⊢ 2 𝑜 ∈ On ∖ 2 𝑜 ∧ ∃ b ∈ On ∖ 2 𝑜 ∃ c ∈ On ∖ 1 𝑜 ¬ 2 𝑜 ∈ b ↔ 2 𝑜 ↑ 𝑜 c ∈ b ↑ 𝑜 c → ∃ a ∈ On ∖ 2 𝑜 ∃ b ∈ On ∖ 2 𝑜 ∃ c ∈ On ∖ 1 𝑜 ¬ a ∈ b ↔ a ↑ 𝑜 c ∈ b ↑ 𝑜 c
41 8 33 40 sylancr ⊢ ¬ 2 𝑜 ∈ 3 𝑜 ↔ 2 𝑜 ↑ 𝑜 ω ∈ 3 𝑜 ↑ 𝑜 ω → ∃ a ∈ On ∖ 2 𝑜 ∃ b ∈ On ∖ 2 𝑜 ∃ c ∈ On ∖ 1 𝑜 ¬ a ∈ b ↔ a ↑ 𝑜 c ∈ b ↑ 𝑜 c
42 1 41 ax-mp ⊢ ∃ a ∈ On ∖ 2 𝑜 ∃ b ∈ On ∖ 2 𝑜 ∃ c ∈ On ∖ 1 𝑜 ¬ a ∈ b ↔ a ↑ 𝑜 c ∈ b ↑ 𝑜 c