Metamath Proof Explorer

Theorem onexomgt

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

Ref Expression
Assertion onexomgt ⊢ A ∈ On → ∃ x ∈ On A ∈ ω ⋅ 𝑜 x

Proof

Step Hyp Ref Expression
1 omelon ⊢ ω ∈ On
2 peano1 ⊢ ∅ ∈ ω
3 2 ne0ii ⊢ ω ≠ ∅
4 omeu ⊢ ω ∈ On ∧ A ∈ On ∧ ω ≠ ∅ → ∃! c ∃ a ∈ On ∃ b ∈ ω c = a b ∧ ω ⋅ 𝑜 a + 𝑜 b = A
5 1 3 4 mp3an13 ⊢ A ∈ On → ∃! c ∃ a ∈ On ∃ b ∈ ω c = a b ∧ ω ⋅ 𝑜 a + 𝑜 b = A
6 euex ⊢ ∃! c ∃ a ∈ On ∃ b ∈ ω c = a b ∧ ω ⋅ 𝑜 a + 𝑜 b = A → ∃ c ∃ a ∈ On ∃ b ∈ ω c = a b ∧ ω ⋅ 𝑜 a + 𝑜 b = A
7 onsuc ⊢ a ∈ On → suc ⁡ a ∈ On
8 7 adantr ⊢ a ∈ On ∧ b ∈ ω → suc ⁡ a ∈ On
9 simpr ⊢ a ∈ On ∧ b ∈ ω ∧ ω ⋅ 𝑜 a + 𝑜 b = A → ω ⋅ 𝑜 a + 𝑜 b = A
10 simpr ⊢ a ∈ On ∧ b ∈ ω → b ∈ ω
11 simpl ⊢ a ∈ On ∧ b ∈ ω → a ∈ On
12 omcl ⊢ ω ∈ On ∧ a ∈ On → ω ⋅ 𝑜 a ∈ On
13 1 11 12 sylancr ⊢ a ∈ On ∧ b ∈ ω → ω ⋅ 𝑜 a ∈ On
14 oaordi ⊢ ω ∈ On ∧ ω ⋅ 𝑜 a ∈ On → b ∈ ω → ω ⋅ 𝑜 a + 𝑜 b ∈ ω ⋅ 𝑜 a + 𝑜 ω
15 1 13 14 sylancr ⊢ a ∈ On ∧ b ∈ ω → b ∈ ω → ω ⋅ 𝑜 a + 𝑜 b ∈ ω ⋅ 𝑜 a + 𝑜 ω
16 10 15 mpd ⊢ a ∈ On ∧ b ∈ ω → ω ⋅ 𝑜 a + 𝑜 b ∈ ω ⋅ 𝑜 a + 𝑜 ω
17 omsuc ⊢ ω ∈ On ∧ a ∈ On → ω ⋅ 𝑜 suc ⁡ a = ω ⋅ 𝑜 a + 𝑜 ω
18 1 11 17 sylancr ⊢ a ∈ On ∧ b ∈ ω → ω ⋅ 𝑜 suc ⁡ a = ω ⋅ 𝑜 a + 𝑜 ω
19 16 18 eleqtrrd ⊢ a ∈ On ∧ b ∈ ω → ω ⋅ 𝑜 a + 𝑜 b ∈ ω ⋅ 𝑜 suc ⁡ a
20 19 adantr ⊢ a ∈ On ∧ b ∈ ω ∧ ω ⋅ 𝑜 a + 𝑜 b = A → ω ⋅ 𝑜 a + 𝑜 b ∈ ω ⋅ 𝑜 suc ⁡ a
21 9 20 eqeltrrd ⊢ a ∈ On ∧ b ∈ ω ∧ ω ⋅ 𝑜 a + 𝑜 b = A → A ∈ ω ⋅ 𝑜 suc ⁡ a
22 oveq2 ⊢ x = suc ⁡ a → ω ⋅ 𝑜 x = ω ⋅ 𝑜 suc ⁡ a
23 22 eleq2d ⊢ x = suc ⁡ a → A ∈ ω ⋅ 𝑜 x ↔ A ∈ ω ⋅ 𝑜 suc ⁡ a
24 23 rspcev ⊢ suc ⁡ a ∈ On ∧ A ∈ ω ⋅ 𝑜 suc ⁡ a → ∃ x ∈ On A ∈ ω ⋅ 𝑜 x
25 8 21 24 syl2an2r ⊢ a ∈ On ∧ b ∈ ω ∧ ω ⋅ 𝑜 a + 𝑜 b = A → ∃ x ∈ On A ∈ ω ⋅ 𝑜 x
26 25 ex ⊢ a ∈ On ∧ b ∈ ω → ω ⋅ 𝑜 a + 𝑜 b = A → ∃ x ∈ On A ∈ ω ⋅ 𝑜 x
27 26 adantld ⊢ a ∈ On ∧ b ∈ ω → c = a b ∧ ω ⋅ 𝑜 a + 𝑜 b = A → ∃ x ∈ On A ∈ ω ⋅ 𝑜 x
28 27 a1i ⊢ A ∈ On → a ∈ On ∧ b ∈ ω → c = a b ∧ ω ⋅ 𝑜 a + 𝑜 b = A → ∃ x ∈ On A ∈ ω ⋅ 𝑜 x
29 28 rexlimdvv ⊢ A ∈ On → ∃ a ∈ On ∃ b ∈ ω c = a b ∧ ω ⋅ 𝑜 a + 𝑜 b = A → ∃ x ∈ On A ∈ ω ⋅ 𝑜 x
30 29 exlimdv ⊢ A ∈ On → ∃ c ∃ a ∈ On ∃ b ∈ ω c = a b ∧ ω ⋅ 𝑜 a + 𝑜 b = A → ∃ x ∈ On A ∈ ω ⋅ 𝑜 x
31 6 30 syl5 ⊢ A ∈ On → ∃! c ∃ a ∈ On ∃ b ∈ ω c = a b ∧ ω ⋅ 𝑜 a + 𝑜 b = A → ∃ x ∈ On A ∈ ω ⋅ 𝑜 x
32 5 31 mpd ⊢ A ∈ On → ∃ x ∈ On A ∈ ω ⋅ 𝑜 x