Theorem oenord1 43732

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.)

Assertion

Ref	Expression
oenord1	⊢ ∃𝑎 ∈ (On ∖ 2o)∃𝑏 ∈ (On ∖ 2o)∃𝑐 ∈ (On ∖ 1o) ¬ (𝑎 ∈ 𝑏 ↔ (𝑎 ↑o 𝑐) ∈ (𝑏 ↑o 𝑐))

Distinct variable group:   𝑎,𝑏,𝑐

Proof of Theorem oenord1

Step	Hyp	Ref	Expression
1		oenord1ex 43731	. 2 ⊢ ¬ (2o ∈ 3o ↔ (2o ↑o ω) ∈ (3o ↑o ω))
2		2on 8407	. . . 4 ⊢ 2o ∈ On
3		1oex 8404	. . . . . 6 ⊢ 1o ∈ V
4	3	prid2 4697	. . . . 5 ⊢ 1o ∈ {∅, 1o}
5		df2o3 8402	. . . . 5 ⊢ 2o = {∅, 1o}
6	4, 5	eleqtrri 2834	. . . 4 ⊢ 1o ∈ 2o
7		ondif2 8426	. . . 4 ⊢ (2o ∈ (On ∖ 2o) ↔ (2o ∈ On ∧ 1o ∈ 2o))
8	2, 6, 7	mpbir2an 712	. . 3 ⊢ 2o ∈ (On ∖ 2o)
9		3on 8410	. . . . 5 ⊢ 3o ∈ On
10	3	tpid2 4704	. . . . . 6 ⊢ 1o ∈ {∅, 1o, 2o}
11		df3o2 43729	. . . . . 6 ⊢ 3o = {∅, 1o, 2o}
12	10, 11	eleqtrri 2834	. . . . 5 ⊢ 1o ∈ 3o
13		ondif2 8426	. . . . 5 ⊢ (3o ∈ (On ∖ 2o) ↔ (3o ∈ On ∧ 1o ∈ 3o))
14	9, 12, 13	mpbir2an 712	. . . 4 ⊢ 3o ∈ (On ∖ 2o)
15		omelon 9556	. . . . . 6 ⊢ ω ∈ On
16		peano1 7829	. . . . . 6 ⊢ ∅ ∈ ω
17		ondif1 8425	. . . . . 6 ⊢ (ω ∈ (On ∖ 1o) ↔ (ω ∈ On ∧ ∅ ∈ ω))
18	15, 16, 17	mpbir2an 712	. . . . 5 ⊢ ω ∈ (On ∖ 1o)
19		oveq2 7364	. . . . . . . . 9 ⊢ (𝑐 = ω → (2o ↑o 𝑐) = (2o ↑o ω))
20		oveq2 7364	. . . . . . . . 9 ⊢ (𝑐 = ω → (3o ↑o 𝑐) = (3o ↑o ω))
21	19, 20	eleq12d 2829	. . . . . . . 8 ⊢ (𝑐 = ω → ((2o ↑o 𝑐) ∈ (3o ↑o 𝑐) ↔ (2o ↑o ω) ∈ (3o ↑o ω)))
22	21	bibi2d 342	. . . . . . 7 ⊢ (𝑐 = ω → ((2o ∈ 3o ↔ (2o ↑o 𝑐) ∈ (3o ↑o 𝑐)) ↔ (2o ∈ 3o ↔ (2o ↑o ω) ∈ (3o ↑o ω))))
23	22	notbid 318	. . . . . 6 ⊢ (𝑐 = ω → (¬ (2o ∈ 3o ↔ (2o ↑o 𝑐) ∈ (3o ↑o 𝑐)) ↔ ¬ (2o ∈ 3o ↔ (2o ↑o ω) ∈ (3o ↑o ω))))
24	23	rspcev 3562	. . . . 5 ⊢ ((ω ∈ (On ∖ 1o) ∧ ¬ (2o ∈ 3o ↔ (2o ↑o ω) ∈ (3o ↑o ω))) → ∃𝑐 ∈ (On ∖ 1o) ¬ (2o ∈ 3o ↔ (2o ↑o 𝑐) ∈ (3o ↑o 𝑐)))
25	18, 24	mpan 691	. . . 4 ⊢ (¬ (2o ∈ 3o ↔ (2o ↑o ω) ∈ (3o ↑o ω)) → ∃𝑐 ∈ (On ∖ 1o) ¬ (2o ∈ 3o ↔ (2o ↑o 𝑐) ∈ (3o ↑o 𝑐)))
26		eleq2 2824	. . . . . . . 8 ⊢ (𝑏 = 3o → (2o ∈ 𝑏 ↔ 2o ∈ 3o))
27		oveq1 7363	. . . . . . . . 9 ⊢ (𝑏 = 3o → (𝑏 ↑o 𝑐) = (3o ↑o 𝑐))
28	27	eleq2d 2821	. . . . . . . 8 ⊢ (𝑏 = 3o → ((2o ↑o 𝑐) ∈ (𝑏 ↑o 𝑐) ↔ (2o ↑o 𝑐) ∈ (3o ↑o 𝑐)))
29	26, 28	bibi12d 345	. . . . . . 7 ⊢ (𝑏 = 3o → ((2o ∈ 𝑏 ↔ (2o ↑o 𝑐) ∈ (𝑏 ↑o 𝑐)) ↔ (2o ∈ 3o ↔ (2o ↑o 𝑐) ∈ (3o ↑o 𝑐))))
30	29	notbid 318	. . . . . 6 ⊢ (𝑏 = 3o → (¬ (2o ∈ 𝑏 ↔ (2o ↑o 𝑐) ∈ (𝑏 ↑o 𝑐)) ↔ ¬ (2o ∈ 3o ↔ (2o ↑o 𝑐) ∈ (3o ↑o 𝑐))))
31	30	rexbidv 3159	. . . . 5 ⊢ (𝑏 = 3o → (∃𝑐 ∈ (On ∖ 1o) ¬ (2o ∈ 𝑏 ↔ (2o ↑o 𝑐) ∈ (𝑏 ↑o 𝑐)) ↔ ∃𝑐 ∈ (On ∖ 1o) ¬ (2o ∈ 3o ↔ (2o ↑o 𝑐) ∈ (3o ↑o 𝑐))))
32	31	rspcev 3562	. . . 4 ⊢ ((3o ∈ (On ∖ 2o) ∧ ∃𝑐 ∈ (On ∖ 1o) ¬ (2o ∈ 3o ↔ (2o ↑o 𝑐) ∈ (3o ↑o 𝑐))) → ∃𝑏 ∈ (On ∖ 2o)∃𝑐 ∈ (On ∖ 1o) ¬ (2o ∈ 𝑏 ↔ (2o ↑o 𝑐) ∈ (𝑏 ↑o 𝑐)))
33	14, 25, 32	sylancr 588	. . 3 ⊢ (¬ (2o ∈ 3o ↔ (2o ↑o ω) ∈ (3o ↑o ω)) → ∃𝑏 ∈ (On ∖ 2o)∃𝑐 ∈ (On ∖ 1o) ¬ (2o ∈ 𝑏 ↔ (2o ↑o 𝑐) ∈ (𝑏 ↑o 𝑐)))
34		eleq1 2823	. . . . . . 7 ⊢ (𝑎 = 2o → (𝑎 ∈ 𝑏 ↔ 2o ∈ 𝑏))
35		oveq1 7363	. . . . . . . 8 ⊢ (𝑎 = 2o → (𝑎 ↑o 𝑐) = (2o ↑o 𝑐))
36	35	eleq1d 2820	. . . . . . 7 ⊢ (𝑎 = 2o → ((𝑎 ↑o 𝑐) ∈ (𝑏 ↑o 𝑐) ↔ (2o ↑o 𝑐) ∈ (𝑏 ↑o 𝑐)))
37	34, 36	bibi12d 345	. . . . . 6 ⊢ (𝑎 = 2o → ((𝑎 ∈ 𝑏 ↔ (𝑎 ↑o 𝑐) ∈ (𝑏 ↑o 𝑐)) ↔ (2o ∈ 𝑏 ↔ (2o ↑o 𝑐) ∈ (𝑏 ↑o 𝑐))))
38	37	notbid 318	. . . . 5 ⊢ (𝑎 = 2o → (¬ (𝑎 ∈ 𝑏 ↔ (𝑎 ↑o 𝑐) ∈ (𝑏 ↑o 𝑐)) ↔ ¬ (2o ∈ 𝑏 ↔ (2o ↑o 𝑐) ∈ (𝑏 ↑o 𝑐))))
39	38	2rexbidv 3200	. . . 4 ⊢ (𝑎 = 2o → (∃𝑏 ∈ (On ∖ 2o)∃𝑐 ∈ (On ∖ 1o) ¬ (𝑎 ∈ 𝑏 ↔ (𝑎 ↑o 𝑐) ∈ (𝑏 ↑o 𝑐)) ↔ ∃𝑏 ∈ (On ∖ 2o)∃𝑐 ∈ (On ∖ 1o) ¬ (2o ∈ 𝑏 ↔ (2o ↑o 𝑐) ∈ (𝑏 ↑o 𝑐))))
40	39	rspcev 3562	. . 3 ⊢ ((2o ∈ (On ∖ 2o) ∧ ∃𝑏 ∈ (On ∖ 2o)∃𝑐 ∈ (On ∖ 1o) ¬ (2o ∈ 𝑏 ↔ (2o ↑o 𝑐) ∈ (𝑏 ↑o 𝑐))) → ∃𝑎 ∈ (On ∖ 2o)∃𝑏 ∈ (On ∖ 2o)∃𝑐 ∈ (On ∖ 1o) ¬ (𝑎 ∈ 𝑏 ↔ (𝑎 ↑o 𝑐) ∈ (𝑏 ↑o 𝑐)))
41	8, 33, 40	sylancr 588	. 2 ⊢ (¬ (2o ∈ 3o ↔ (2o ↑o ω) ∈ (3o ↑o ω)) → ∃𝑎 ∈ (On ∖ 2o)∃𝑏 ∈ (On ∖ 2o)∃𝑐 ∈ (On ∖ 1o) ¬ (𝑎 ∈ 𝑏 ↔ (𝑎 ↑o 𝑐) ∈ (𝑏 ↑o 𝑐)))
42	1, 41	ax-mp 5	1 ⊢ ∃𝑎 ∈ (On ∖ 2o)∃𝑏 ∈ (On ∖ 2o)∃𝑐 ∈ (On ∖ 1o) ¬ (𝑎 ∈ 𝑏 ↔ (𝑎 ↑o 𝑐) ∈ (𝑏 ↑o 𝑐))

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1542   ∈ wcel 2114  ∃wrex 3059   ∖ cdif 3882  ∅c0 4263  {cpr 4559  {ctp 4561  Oncon0 6312  (class class class)co 7356  ωcom 7806  1_oc1o 8387  2_oc2o 8388  3_oc3o 8389   ↑_o coe 8393

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2184  ax-ext 2707  ax-rep 5201  ax-sep 5220  ax-nul 5230  ax-pr 5364  ax-un 7678  ax-inf2 9551

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2538  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2810  df-nfc 2884  df-ne 2931  df-ral 3050  df-rex 3060  df-reu 3341  df-rab 3388  df-v 3429  df-sbc 3726  df-csb 3834  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-pss 3905  df-nul 4264  df-if 4457  df-pw 4533  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4841  df-iun 4925  df-br 5075  df-opab 5137  df-mpt 5156  df-tr 5182  df-id 5515  df-eprel 5520  df-po 5528  df-so 5529  df-fr 5573  df-we 5575  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633  df-pred 6254  df-ord 6315  df-on 6316  df-lim 6317  df-suc 6318  df-iota 6443  df-fun 6489  df-fn 6490  df-f 6491  df-f1 6492  df-fo 6493  df-f1o 6494  df-fv 6495  df-ov 7359  df-oprab 7360  df-mpo 7361  df-om 7807  df-2nd 7932  df-frecs 8220  df-wrecs 8251  df-recs 8300  df-rdg 8338  df-1o 8394  df-2o 8395  df-3o 8396  df-oadd 8398  df-omul 8399  df-oexp 8400

This theorem is referenced by: (None)