Metamath Proof Explorer

Theorem onexlimgt

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

Ref Expression
Assertion onexlimgt ⊢A∈On→∃x∈OnLim⁡x∧A∈x

Proof

Step Hyp Ref Expression
1 omelon ⊢ω∈On
2 onun2 ⊢A∈On∧ω∈On→A∪ω∈On
3 1 2 mpan2 ⊢A∈On→A∪ω∈On
4 onexomgt ⊢A∪ω∈On→∃a∈OnA∪ω∈ω⋅𝑜a
5 3 4 syl ⊢A∈On→∃a∈OnA∪ω∈ω⋅𝑜a
6 simp2 ⊢A∈On∧a∈On∧A∪ω∈ω⋅𝑜a→a∈On
7 omcl ⊢ω∈On∧a∈On→ω⋅𝑜a∈On
8 1 6 7 sylancr ⊢A∈On∧a∈On∧A∪ω∈ω⋅𝑜a→ω⋅𝑜a∈On
9 noel ⊢¬A∪ω∈∅
10 oveq2 ⊢a=∅→ω⋅𝑜a=ω⋅𝑜∅
11 om0 ⊢ω∈On→ω⋅𝑜∅=∅
12 1 11 ax-mp ⊢ω⋅𝑜∅=∅
13 10 12 eqtrdi ⊢a=∅→ω⋅𝑜a=∅
14 13 eleq2d ⊢a=∅→A∪ω∈ω⋅𝑜a↔A∪ω∈∅
15 14 notbid ⊢a=∅→¬A∪ω∈ω⋅𝑜a↔¬A∪ω∈∅
16 15 adantl ⊢A∈On∧a∈On∧a=∅→¬A∪ω∈ω⋅𝑜a↔¬A∪ω∈∅
17 9 16 mpbiri ⊢A∈On∧a∈On∧a=∅→¬A∪ω∈ω⋅𝑜a
18 17 pm2.21d ⊢A∈On∧a∈On∧a=∅→A∪ω∈ω⋅𝑜a→Lim⁡ω⋅𝑜a
19 18 ex ⊢A∈On∧a∈On→a=∅→A∪ω∈ω⋅𝑜a→Lim⁡ω⋅𝑜a
20 19 com23 ⊢A∈On∧a∈On→A∪ω∈ω⋅𝑜a→a=∅→Lim⁡ω⋅𝑜a
21 20 3impia ⊢A∈On∧a∈On∧A∪ω∈ω⋅𝑜a→a=∅→Lim⁡ω⋅𝑜a
22 limom ⊢Lim⁡ω
23 1 22 pm3.2i ⊢ω∈On∧Lim⁡ω
24 6 23 jctir ⊢A∈On∧a∈On∧A∪ω∈ω⋅𝑜a→a∈On∧ω∈On∧Lim⁡ω
25 omlimcl2 ⊢a∈On∧ω∈On∧Lim⁡ω∧∅∈a→Lim⁡ω⋅𝑜a
26 24 25 sylan ⊢A∈On∧a∈On∧A∪ω∈ω⋅𝑜a∧∅∈a→Lim⁡ω⋅𝑜a
27 26 ex ⊢A∈On∧a∈On∧A∪ω∈ω⋅𝑜a→∅∈a→Lim⁡ω⋅𝑜a
28 on0eqel ⊢a∈On→a=∅∨∅∈a
29 6 28 syl ⊢A∈On∧a∈On∧A∪ω∈ω⋅𝑜a→a=∅∨∅∈a
30 21 27 29 mpjaod ⊢A∈On∧a∈On∧A∪ω∈ω⋅𝑜a→Lim⁡ω⋅𝑜a
31 simp1 ⊢A∈On∧a∈On∧A∪ω∈ω⋅𝑜a→A∈On
32 31 8 jca ⊢A∈On∧a∈On∧A∪ω∈ω⋅𝑜a→A∈On∧ω⋅𝑜a∈On
33 simp3 ⊢A∈On∧a∈On∧A∪ω∈ω⋅𝑜a→A∪ω∈ω⋅𝑜a
34 ssun1 ⊢A⊆A∪ω
35 33 34 jctil ⊢A∈On∧a∈On∧A∪ω∈ω⋅𝑜a→A⊆A∪ω∧A∪ω∈ω⋅𝑜a
36 ontr2 ⊢A∈On∧ω⋅𝑜a∈On→A⊆A∪ω∧A∪ω∈ω⋅𝑜a→A∈ω⋅𝑜a
37 32 35 36 sylc ⊢A∈On∧a∈On∧A∪ω∈ω⋅𝑜a→A∈ω⋅𝑜a
38 limeq ⊢x=ω⋅𝑜a→Lim⁡x↔Lim⁡ω⋅𝑜a
39 eleq2 ⊢x=ω⋅𝑜a→A∈x↔A∈ω⋅𝑜a
40 38 39 anbi12d ⊢x=ω⋅𝑜a→Lim⁡x∧A∈x↔Lim⁡ω⋅𝑜a∧A∈ω⋅𝑜a
41 40 rspcev ⊢ω⋅𝑜a∈On∧Lim⁡ω⋅𝑜a∧A∈ω⋅𝑜a→∃x∈OnLim⁡x∧A∈x
42 8 30 37 41 syl12anc ⊢A∈On∧a∈On∧A∪ω∈ω⋅𝑜a→∃x∈OnLim⁡x∧A∈x
43 42 rexlimdv3a ⊢A∈On→∃a∈OnA∪ω∈ω⋅𝑜a→∃x∈OnLim⁡x∧A∈x
44 5 43 mpd ⊢A∈On→∃x∈OnLim⁡x∧A∈x