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