Metamath Proof Explorer

Theorem onexoegt

Description: For any ordinal, there is always a larger power of omega. (Contributed by RP, 1-Feb-2025)

Ref Expression
Assertion onexoegt ⊢ A ∈ On → ∃ x ∈ On A ∈ ω ↑ 𝑜 x

Proof

Step Hyp Ref Expression
1 0elon ⊢ ∅ ∈ On
2 0lt1o ⊢ ∅ ∈ 1 𝑜
3 omelon ⊢ ω ∈ On
4 oe0 ⊢ ω ∈ On → ω ↑ 𝑜 ∅ = 1 𝑜
5 3 4 ax-mp ⊢ ω ↑ 𝑜 ∅ = 1 𝑜
6 2 5 eleqtrri ⊢ ∅ ∈ ω ↑ 𝑜 ∅
7 6 a1i ⊢ A = ∅ → ∅ ∈ ω ↑ 𝑜 ∅
8 oveq2 ⊢ x = ∅ → ω ↑ 𝑜 x = ω ↑ 𝑜 ∅
9 8 eleq2d ⊢ x = ∅ → ∅ ∈ ω ↑ 𝑜 x ↔ ∅ ∈ ω ↑ 𝑜 ∅
10 9 rspcev ⊢ ∅ ∈ On ∧ ∅ ∈ ω ↑ 𝑜 ∅ → ∃ x ∈ On ∅ ∈ ω ↑ 𝑜 x
11 1 7 10 sylancr ⊢ A = ∅ → ∃ x ∈ On ∅ ∈ ω ↑ 𝑜 x
12 eleq1 ⊢ A = ∅ → A ∈ ω ↑ 𝑜 x ↔ ∅ ∈ ω ↑ 𝑜 x
13 12 rexbidv ⊢ A = ∅ → ∃ x ∈ On A ∈ ω ↑ 𝑜 x ↔ ∃ x ∈ On ∅ ∈ ω ↑ 𝑜 x
14 11 13 mpbird ⊢ A = ∅ → ∃ x ∈ On A ∈ ω ↑ 𝑜 x
15 14 a1i ⊢ A ∈ On → A = ∅ → ∃ x ∈ On A ∈ ω ↑ 𝑜 x
16 1onn ⊢ 1 𝑜 ∈ ω
17 ondif2 ⊢ ω ∈ On ∖ 2 𝑜 ↔ ω ∈ On ∧ 1 𝑜 ∈ ω
18 3 16 17 mpbir2an ⊢ ω ∈ On ∖ 2 𝑜
19 ondif1 ⊢ A ∈ On ∖ 1 𝑜 ↔ A ∈ On ∧ ∅ ∈ A
20 19 biimpri ⊢ A ∈ On ∧ ∅ ∈ A → A ∈ On ∖ 1 𝑜
21 oeeu ⊢ ω ∈ On ∖ 2 𝑜 ∧ A ∈ On ∖ 1 𝑜 → ∃! d ∃ a ∈ On ∃ b ∈ ω ∖ 1 𝑜 ∃ c ∈ ω ↑ 𝑜 a d = a b c ∧ ω ↑ 𝑜 a ⋅ 𝑜 b + 𝑜 c = A
22 18 20 21 sylancr ⊢ A ∈ On ∧ ∅ ∈ A → ∃! d ∃ a ∈ On ∃ b ∈ ω ∖ 1 𝑜 ∃ c ∈ ω ↑ 𝑜 a d = a b c ∧ ω ↑ 𝑜 a ⋅ 𝑜 b + 𝑜 c = A
23 euex ⊢ ∃! d ∃ a ∈ On ∃ b ∈ ω ∖ 1 𝑜 ∃ c ∈ ω ↑ 𝑜 a d = a b c ∧ ω ↑ 𝑜 a ⋅ 𝑜 b + 𝑜 c = A → ∃ d ∃ a ∈ On ∃ b ∈ ω ∖ 1 𝑜 ∃ c ∈ ω ↑ 𝑜 a d = a b c ∧ ω ↑ 𝑜 a ⋅ 𝑜 b + 𝑜 c = A
24 simpr ⊢ d = a b c ∧ ω ↑ 𝑜 a ⋅ 𝑜 b + 𝑜 c = A → ω ↑ 𝑜 a ⋅ 𝑜 b + 𝑜 c = A
25 simp1 ⊢ a ∈ On ∧ b ∈ ω ∖ 1 𝑜 ∧ c ∈ ω ↑ 𝑜 a → a ∈ On
26 onsuc ⊢ a ∈ On → suc ⁡ a ∈ On
27 25 26 syl ⊢ a ∈ On ∧ b ∈ ω ∖ 1 𝑜 ∧ c ∈ ω ↑ 𝑜 a → suc ⁡ a ∈ On
28 27 adantl ⊢ A ∈ On ∧ ∅ ∈ A ∧ a ∈ On ∧ b ∈ ω ∖ 1 𝑜 ∧ c ∈ ω ↑ 𝑜 a → suc ⁡ a ∈ On
29 simpr ⊢ a ∈ On ∧ b ∈ ω ∖ 1 𝑜 ∧ c ∈ ω ↑ 𝑜 a ∧ ω ↑ 𝑜 a ⋅ 𝑜 b + 𝑜 c = A → ω ↑ 𝑜 a ⋅ 𝑜 b + 𝑜 c = A
30 oecl ⊢ ω ∈ On ∧ a ∈ On → ω ↑ 𝑜 a ∈ On
31 3 25 30 sylancr ⊢ a ∈ On ∧ b ∈ ω ∖ 1 𝑜 ∧ c ∈ ω ↑ 𝑜 a → ω ↑ 𝑜 a ∈ On
32 3 a1i ⊢ a ∈ On ∧ b ∈ ω ∖ 1 𝑜 ∧ c ∈ ω ↑ 𝑜 a → ω ∈ On
33 omcl ⊢ ω ↑ 𝑜 a ∈ On ∧ ω ∈ On → ω ↑ 𝑜 a ⋅ 𝑜 ω ∈ On
34 31 32 33 syl2anc ⊢ a ∈ On ∧ b ∈ ω ∖ 1 𝑜 ∧ c ∈ ω ↑ 𝑜 a → ω ↑ 𝑜 a ⋅ 𝑜 ω ∈ On
35 simp3 ⊢ a ∈ On ∧ b ∈ ω ∖ 1 𝑜 ∧ c ∈ ω ↑ 𝑜 a → c ∈ ω ↑ 𝑜 a
36 eldifi ⊢ b ∈ ω ∖ 1 𝑜 → b ∈ ω
37 nnon ⊢ b ∈ ω → b ∈ On
38 36 37 syl ⊢ b ∈ ω ∖ 1 𝑜 → b ∈ On
39 38 3ad2ant2 ⊢ a ∈ On ∧ b ∈ ω ∖ 1 𝑜 ∧ c ∈ ω ↑ 𝑜 a → b ∈ On
40 omcl ⊢ ω ↑ 𝑜 a ∈ On ∧ b ∈ On → ω ↑ 𝑜 a ⋅ 𝑜 b ∈ On
41 31 39 40 syl2anc ⊢ a ∈ On ∧ b ∈ ω ∖ 1 𝑜 ∧ c ∈ ω ↑ 𝑜 a → ω ↑ 𝑜 a ⋅ 𝑜 b ∈ On
42 oaordi ⊢ ω ↑ 𝑜 a ∈ On ∧ ω ↑ 𝑜 a ⋅ 𝑜 b ∈ On → c ∈ ω ↑ 𝑜 a → ω ↑ 𝑜 a ⋅ 𝑜 b + 𝑜 c ∈ ω ↑ 𝑜 a ⋅ 𝑜 b + 𝑜 ω ↑ 𝑜 a
43 31 41 42 syl2anc ⊢ a ∈ On ∧ b ∈ ω ∖ 1 𝑜 ∧ c ∈ ω ↑ 𝑜 a → c ∈ ω ↑ 𝑜 a → ω ↑ 𝑜 a ⋅ 𝑜 b + 𝑜 c ∈ ω ↑ 𝑜 a ⋅ 𝑜 b + 𝑜 ω ↑ 𝑜 a
44 35 43 mpd ⊢ a ∈ On ∧ b ∈ ω ∖ 1 𝑜 ∧ c ∈ ω ↑ 𝑜 a → ω ↑ 𝑜 a ⋅ 𝑜 b + 𝑜 c ∈ ω ↑ 𝑜 a ⋅ 𝑜 b + 𝑜 ω ↑ 𝑜 a
45 omsuc ⊢ ω ↑ 𝑜 a ∈ On ∧ b ∈ On → ω ↑ 𝑜 a ⋅ 𝑜 suc ⁡ b = ω ↑ 𝑜 a ⋅ 𝑜 b + 𝑜 ω ↑ 𝑜 a
46 31 39 45 syl2anc ⊢ a ∈ On ∧ b ∈ ω ∖ 1 𝑜 ∧ c ∈ ω ↑ 𝑜 a → ω ↑ 𝑜 a ⋅ 𝑜 suc ⁡ b = ω ↑ 𝑜 a ⋅ 𝑜 b + 𝑜 ω ↑ 𝑜 a
47 44 46 eleqtrrd ⊢ a ∈ On ∧ b ∈ ω ∖ 1 𝑜 ∧ c ∈ ω ↑ 𝑜 a → ω ↑ 𝑜 a ⋅ 𝑜 b + 𝑜 c ∈ ω ↑ 𝑜 a ⋅ 𝑜 suc ⁡ b
48 36 3ad2ant2 ⊢ a ∈ On ∧ b ∈ ω ∖ 1 𝑜 ∧ c ∈ ω ↑ 𝑜 a → b ∈ ω
49 peano2 ⊢ b ∈ ω → suc ⁡ b ∈ ω
50 48 49 syl ⊢ a ∈ On ∧ b ∈ ω ∖ 1 𝑜 ∧ c ∈ ω ↑ 𝑜 a → suc ⁡ b ∈ ω
51 peano1 ⊢ ∅ ∈ ω
52 51 a1i ⊢ a ∈ On ∧ b ∈ ω ∖ 1 𝑜 ∧ c ∈ ω ↑ 𝑜 a → ∅ ∈ ω
53 oen0 ⊢ ω ∈ On ∧ a ∈ On ∧ ∅ ∈ ω → ∅ ∈ ω ↑ 𝑜 a
54 32 25 52 53 syl21anc ⊢ a ∈ On ∧ b ∈ ω ∖ 1 𝑜 ∧ c ∈ ω ↑ 𝑜 a → ∅ ∈ ω ↑ 𝑜 a
55 omordi ⊢ ω ∈ On ∧ ω ↑ 𝑜 a ∈ On ∧ ∅ ∈ ω ↑ 𝑜 a → suc ⁡ b ∈ ω → ω ↑ 𝑜 a ⋅ 𝑜 suc ⁡ b ∈ ω ↑ 𝑜 a ⋅ 𝑜 ω
56 32 31 54 55 syl21anc ⊢ a ∈ On ∧ b ∈ ω ∖ 1 𝑜 ∧ c ∈ ω ↑ 𝑜 a → suc ⁡ b ∈ ω → ω ↑ 𝑜 a ⋅ 𝑜 suc ⁡ b ∈ ω ↑ 𝑜 a ⋅ 𝑜 ω
57 50 56 mpd ⊢ a ∈ On ∧ b ∈ ω ∖ 1 𝑜 ∧ c ∈ ω ↑ 𝑜 a → ω ↑ 𝑜 a ⋅ 𝑜 suc ⁡ b ∈ ω ↑ 𝑜 a ⋅ 𝑜 ω
58 ontr1 ⊢ ω ↑ 𝑜 a ⋅ 𝑜 ω ∈ On → ω ↑ 𝑜 a ⋅ 𝑜 b + 𝑜 c ∈ ω ↑ 𝑜 a ⋅ 𝑜 suc ⁡ b ∧ ω ↑ 𝑜 a ⋅ 𝑜 suc ⁡ b ∈ ω ↑ 𝑜 a ⋅ 𝑜 ω → ω ↑ 𝑜 a ⋅ 𝑜 b + 𝑜 c ∈ ω ↑ 𝑜 a ⋅ 𝑜 ω
59 58 imp ⊢ ω ↑ 𝑜 a ⋅ 𝑜 ω ∈ On ∧ ω ↑ 𝑜 a ⋅ 𝑜 b + 𝑜 c ∈ ω ↑ 𝑜 a ⋅ 𝑜 suc ⁡ b ∧ ω ↑ 𝑜 a ⋅ 𝑜 suc ⁡ b ∈ ω ↑ 𝑜 a ⋅ 𝑜 ω → ω ↑ 𝑜 a ⋅ 𝑜 b + 𝑜 c ∈ ω ↑ 𝑜 a ⋅ 𝑜 ω
60 34 47 57 59 syl12anc ⊢ a ∈ On ∧ b ∈ ω ∖ 1 𝑜 ∧ c ∈ ω ↑ 𝑜 a → ω ↑ 𝑜 a ⋅ 𝑜 b + 𝑜 c ∈ ω ↑ 𝑜 a ⋅ 𝑜 ω
61 oesuc ⊢ ω ∈ On ∧ a ∈ On → ω ↑ 𝑜 suc ⁡ a = ω ↑ 𝑜 a ⋅ 𝑜 ω
62 3 25 61 sylancr ⊢ a ∈ On ∧ b ∈ ω ∖ 1 𝑜 ∧ c ∈ ω ↑ 𝑜 a → ω ↑ 𝑜 suc ⁡ a = ω ↑ 𝑜 a ⋅ 𝑜 ω
63 60 62 eleqtrrd ⊢ a ∈ On ∧ b ∈ ω ∖ 1 𝑜 ∧ c ∈ ω ↑ 𝑜 a → ω ↑ 𝑜 a ⋅ 𝑜 b + 𝑜 c ∈ ω ↑ 𝑜 suc ⁡ a
64 63 adantr ⊢ a ∈ On ∧ b ∈ ω ∖ 1 𝑜 ∧ c ∈ ω ↑ 𝑜 a ∧ ω ↑ 𝑜 a ⋅ 𝑜 b + 𝑜 c = A → ω ↑ 𝑜 a ⋅ 𝑜 b + 𝑜 c ∈ ω ↑ 𝑜 suc ⁡ a
65 29 64 eqeltrrd ⊢ a ∈ On ∧ b ∈ ω ∖ 1 𝑜 ∧ c ∈ ω ↑ 𝑜 a ∧ ω ↑ 𝑜 a ⋅ 𝑜 b + 𝑜 c = A → A ∈ ω ↑ 𝑜 suc ⁡ a
66 65 adantll ⊢ A ∈ On ∧ ∅ ∈ A ∧ a ∈ On ∧ b ∈ ω ∖ 1 𝑜 ∧ c ∈ ω ↑ 𝑜 a ∧ ω ↑ 𝑜 a ⋅ 𝑜 b + 𝑜 c = A → A ∈ ω ↑ 𝑜 suc ⁡ a
67 oveq2 ⊢ x = suc ⁡ a → ω ↑ 𝑜 x = ω ↑ 𝑜 suc ⁡ a
68 67 eleq2d ⊢ x = suc ⁡ a → A ∈ ω ↑ 𝑜 x ↔ A ∈ ω ↑ 𝑜 suc ⁡ a
69 68 rspcev ⊢ suc ⁡ a ∈ On ∧ A ∈ ω ↑ 𝑜 suc ⁡ a → ∃ x ∈ On A ∈ ω ↑ 𝑜 x
70 28 66 69 syl2an2r ⊢ A ∈ On ∧ ∅ ∈ A ∧ a ∈ On ∧ b ∈ ω ∖ 1 𝑜 ∧ c ∈ ω ↑ 𝑜 a ∧ ω ↑ 𝑜 a ⋅ 𝑜 b + 𝑜 c = A → ∃ x ∈ On A ∈ ω ↑ 𝑜 x
71 70 ex ⊢ A ∈ On ∧ ∅ ∈ A ∧ a ∈ On ∧ b ∈ ω ∖ 1 𝑜 ∧ c ∈ ω ↑ 𝑜 a → ω ↑ 𝑜 a ⋅ 𝑜 b + 𝑜 c = A → ∃ x ∈ On A ∈ ω ↑ 𝑜 x
72 24 71 syl5 ⊢ A ∈ On ∧ ∅ ∈ A ∧ a ∈ On ∧ b ∈ ω ∖ 1 𝑜 ∧ c ∈ ω ↑ 𝑜 a → d = a b c ∧ ω ↑ 𝑜 a ⋅ 𝑜 b + 𝑜 c = A → ∃ x ∈ On A ∈ ω ↑ 𝑜 x
73 72 3exp2 ⊢ A ∈ On ∧ ∅ ∈ A → a ∈ On → b ∈ ω ∖ 1 𝑜 → c ∈ ω ↑ 𝑜 a → d = a b c ∧ ω ↑ 𝑜 a ⋅ 𝑜 b + 𝑜 c = A → ∃ x ∈ On A ∈ ω ↑ 𝑜 x
74 73 imp4b ⊢ A ∈ On ∧ ∅ ∈ A ∧ a ∈ On → b ∈ ω ∖ 1 𝑜 ∧ c ∈ ω ↑ 𝑜 a → d = a b c ∧ ω ↑ 𝑜 a ⋅ 𝑜 b + 𝑜 c = A → ∃ x ∈ On A ∈ ω ↑ 𝑜 x
75 74 rexlimdvv ⊢ A ∈ On ∧ ∅ ∈ A ∧ a ∈ On → ∃ b ∈ ω ∖ 1 𝑜 ∃ c ∈ ω ↑ 𝑜 a d = a b c ∧ ω ↑ 𝑜 a ⋅ 𝑜 b + 𝑜 c = A → ∃ x ∈ On A ∈ ω ↑ 𝑜 x
76 75 rexlimdva ⊢ A ∈ On ∧ ∅ ∈ A → ∃ a ∈ On ∃ b ∈ ω ∖ 1 𝑜 ∃ c ∈ ω ↑ 𝑜 a d = a b c ∧ ω ↑ 𝑜 a ⋅ 𝑜 b + 𝑜 c = A → ∃ x ∈ On A ∈ ω ↑ 𝑜 x
77 76 exlimdv ⊢ A ∈ On ∧ ∅ ∈ A → ∃ d ∃ a ∈ On ∃ b ∈ ω ∖ 1 𝑜 ∃ c ∈ ω ↑ 𝑜 a d = a b c ∧ ω ↑ 𝑜 a ⋅ 𝑜 b + 𝑜 c = A → ∃ x ∈ On A ∈ ω ↑ 𝑜 x
78 23 77 syl5 ⊢ A ∈ On ∧ ∅ ∈ A → ∃! d ∃ a ∈ On ∃ b ∈ ω ∖ 1 𝑜 ∃ c ∈ ω ↑ 𝑜 a d = a b c ∧ ω ↑ 𝑜 a ⋅ 𝑜 b + 𝑜 c = A → ∃ x ∈ On A ∈ ω ↑ 𝑜 x
79 22 78 mpd ⊢ A ∈ On ∧ ∅ ∈ A → ∃ x ∈ On A ∈ ω ↑ 𝑜 x
80 79 ex ⊢ A ∈ On → ∅ ∈ A → ∃ x ∈ On A ∈ ω ↑ 𝑜 x
81 on0eqel ⊢ A ∈ On → A = ∅ ∨ ∅ ∈ A
82 15 80 81 mpjaod ⊢ A ∈ On → ∃ x ∈ On A ∈ ω ↑ 𝑜 x