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 ( 𝐴 ∈ On → ∃ 𝑥 ∈ On ( Lim 𝑥 ∧ 𝐴 ∈ 𝑥 ) )

Proof

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