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 ∈ On Lim ⁡ 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 ∈ On A ∪ ω ∈ ω ⋅ 𝑜 a
5 3 4 syl ⊢ A ∈ On → ∃ a ∈ On A ∪ ω ∈ ω ⋅ 𝑜 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 ∈ On Lim ⁡ x ∧ A ∈ x
42 8 30 37 41 syl12anc ⊢ A ∈ On ∧ a ∈ On ∧ A ∪ ω ∈ ω ⋅ 𝑜 a → ∃ x ∈ On Lim ⁡ x ∧ A ∈ x
43 42 rexlimdv3a ⊢ A ∈ On → ∃ a ∈ On A ∪ ω ∈ ω ⋅ 𝑜 a → ∃ x ∈ On Lim ⁡ x ∧ A ∈ x
44 5 43 mpd ⊢ A ∈ On → ∃ x ∈ On Lim ⁡ x ∧ A ∈ x