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	⊢ ∃ 𝑎 ∈ ( On ∖ 2o ) ∃ 𝑏 ∈ ( On ∖ 2o ) ∃ 𝑐 ∈ ( On ∖ 1o ) ¬ ( 𝑎 ∈ 𝑏 ↔ ( 𝑎 ↑o 𝑐 ) ∈ ( 𝑏 ↑o 𝑐 ) )

Proof

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