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∈OnA∈ω⋅𝑜x

Proof

Step Hyp Ref Expression
1 omelon ⊢ω∈On
2 peano1 ⊢∅∈ω
3 2 ne0ii ⊢ω≠∅
4 omeu ⊢ω∈On∧A∈On∧ω≠∅→∃!c∃a∈On∃b∈ωc=ab∧ω⋅𝑜a+𝑜b=A
5 1 3 4 mp3an13 ⊢A∈On→∃!c∃a∈On∃b∈ωc=ab∧ω⋅𝑜a+𝑜b=A
6 euex ⊢∃!c∃a∈On∃b∈ωc=ab∧ω⋅𝑜a+𝑜b=A→∃c∃a∈On∃b∈ωc=ab∧ω⋅𝑜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∈OnA∈ω⋅𝑜x
25 8 21 24 syl2an2r ⊢a∈On∧b∈ω∧ω⋅𝑜a+𝑜b=A→∃x∈OnA∈ω⋅𝑜x
26 25 ex ⊢a∈On∧b∈ω→ω⋅𝑜a+𝑜b=A→∃x∈OnA∈ω⋅𝑜x
27 26 adantld ⊢a∈On∧b∈ω→c=ab∧ω⋅𝑜a+𝑜b=A→∃x∈OnA∈ω⋅𝑜x
28 27 a1i ⊢A∈On→a∈On∧b∈ω→c=ab∧ω⋅𝑜a+𝑜b=A→∃x∈OnA∈ω⋅𝑜x
29 28 rexlimdvv ⊢A∈On→∃a∈On∃b∈ωc=ab∧ω⋅𝑜a+𝑜b=A→∃x∈OnA∈ω⋅𝑜x
30 29 exlimdv ⊢A∈On→∃c∃a∈On∃b∈ωc=ab∧ω⋅𝑜a+𝑜b=A→∃x∈OnA∈ω⋅𝑜x
31 6 30 syl5 ⊢A∈On→∃!c∃a∈On∃b∈ωc=ab∧ω⋅𝑜a+𝑜b=A→∃x∈OnA∈ω⋅𝑜x
32 5 31 mpd ⊢A∈On→∃x∈OnA∈ω⋅𝑜x