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 e. On -> E. x e. On ( Lim x /\ A e. x ) )

Proof

Step Hyp Ref Expression
1 omelon 
 |-  _om e. On
2 onun2 
 |-  ( ( A e. On /\ _om e. On ) -> ( A u. _om ) e. On )
3 1 2 mpan2 
 |-  ( A e. On -> ( A u. _om ) e. On )
4 onexomgt 
 |-  ( ( A u. _om ) e. On -> E. a e. On ( A u. _om ) e. ( _om .o a ) )
5 3 4 syl 
 |-  ( A e. On -> E. a e. On ( A u. _om ) e. ( _om .o a ) )
6 simp2 
 |-  ( ( A e. On /\ a e. On /\ ( A u. _om ) e. ( _om .o a ) ) -> a e. On )
7 omcl 
 |-  ( ( _om e. On /\ a e. On ) -> ( _om .o a ) e. On )
8 1 6 7 sylancr 
 |-  ( ( A e. On /\ a e. On /\ ( A u. _om ) e. ( _om .o a ) ) -> ( _om .o a ) e. On )
9 noel 
 |-  -. ( A u. _om ) e. (/)
10 oveq2 
 |-  ( a = (/) -> ( _om .o a ) = ( _om .o (/) ) )
11 om0 
 |-  ( _om e. On -> ( _om .o (/) ) = (/) )
12 1 11 ax-mp 
 |-  ( _om .o (/) ) = (/)
13 10 12 eqtrdi 
 |-  ( a = (/) -> ( _om .o a ) = (/) )
14 13 eleq2d 
 |-  ( a = (/) -> ( ( A u. _om ) e. ( _om .o a ) <-> ( A u. _om ) e. (/) ) )
15 14 notbid 
 |-  ( a = (/) -> ( -. ( A u. _om ) e. ( _om .o a ) <-> -. ( A u. _om ) e. (/) ) )
16 15 adantl 
 |-  ( ( ( A e. On /\ a e. On ) /\ a = (/) ) -> ( -. ( A u. _om ) e. ( _om .o a ) <-> -. ( A u. _om ) e. (/) ) )
17 9 16 mpbiri 
 |-  ( ( ( A e. On /\ a e. On ) /\ a = (/) ) -> -. ( A u. _om ) e. ( _om .o a ) )
18 17 pm2.21d 
 |-  ( ( ( A e. On /\ a e. On ) /\ a = (/) ) -> ( ( A u. _om ) e. ( _om .o a ) -> Lim ( _om .o a ) ) )
19 18 ex 
 |-  ( ( A e. On /\ a e. On ) -> ( a = (/) -> ( ( A u. _om ) e. ( _om .o a ) -> Lim ( _om .o a ) ) ) )
20 19 com23 
 |-  ( ( A e. On /\ a e. On ) -> ( ( A u. _om ) e. ( _om .o a ) -> ( a = (/) -> Lim ( _om .o a ) ) ) )
21 20 3impia 
 |-  ( ( A e. On /\ a e. On /\ ( A u. _om ) e. ( _om .o a ) ) -> ( a = (/) -> Lim ( _om .o a ) ) )
22 limom 
 |-  Lim _om
23 1 22 pm3.2i 
 |-  ( _om e. On /\ Lim _om )
24 6 23 jctir 
 |-  ( ( A e. On /\ a e. On /\ ( A u. _om ) e. ( _om .o a ) ) -> ( a e. On /\ ( _om e. On /\ Lim _om ) ) )
25 omlimcl2 
 |-  ( ( ( a e. On /\ ( _om e. On /\ Lim _om ) ) /\ (/) e. a ) -> Lim ( _om .o a ) )
26 24 25 sylan 
 |-  ( ( ( A e. On /\ a e. On /\ ( A u. _om ) e. ( _om .o a ) ) /\ (/) e. a ) -> Lim ( _om .o a ) )
27 26 ex 
 |-  ( ( A e. On /\ a e. On /\ ( A u. _om ) e. ( _om .o a ) ) -> ( (/) e. a -> Lim ( _om .o a ) ) )
28 on0eqel 
 |-  ( a e. On -> ( a = (/) \/ (/) e. a ) )
29 6 28 syl 
 |-  ( ( A e. On /\ a e. On /\ ( A u. _om ) e. ( _om .o a ) ) -> ( a = (/) \/ (/) e. a ) )
30 21 27 29 mpjaod 
 |-  ( ( A e. On /\ a e. On /\ ( A u. _om ) e. ( _om .o a ) ) -> Lim ( _om .o a ) )
31 simp1 
 |-  ( ( A e. On /\ a e. On /\ ( A u. _om ) e. ( _om .o a ) ) -> A e. On )
32 31 8 jca 
 |-  ( ( A e. On /\ a e. On /\ ( A u. _om ) e. ( _om .o a ) ) -> ( A e. On /\ ( _om .o a ) e. On ) )
33 simp3 
 |-  ( ( A e. On /\ a e. On /\ ( A u. _om ) e. ( _om .o a ) ) -> ( A u. _om ) e. ( _om .o a ) )
34 ssun1 
 |-  A C_ ( A u. _om )
35 33 34 jctil 
 |-  ( ( A e. On /\ a e. On /\ ( A u. _om ) e. ( _om .o a ) ) -> ( A C_ ( A u. _om ) /\ ( A u. _om ) e. ( _om .o a ) ) )
36 ontr2 
 |-  ( ( A e. On /\ ( _om .o a ) e. On ) -> ( ( A C_ ( A u. _om ) /\ ( A u. _om ) e. ( _om .o a ) ) -> A e. ( _om .o a ) ) )
37 32 35 36 sylc 
 |-  ( ( A e. On /\ a e. On /\ ( A u. _om ) e. ( _om .o a ) ) -> A e. ( _om .o a ) )
38 limeq 
 |-  ( x = ( _om .o a ) -> ( Lim x <-> Lim ( _om .o a ) ) )
39 eleq2 
 |-  ( x = ( _om .o a ) -> ( A e. x <-> A e. ( _om .o a ) ) )
40 38 39 anbi12d 
 |-  ( x = ( _om .o a ) -> ( ( Lim x /\ A e. x ) <-> ( Lim ( _om .o a ) /\ A e. ( _om .o a ) ) ) )
41 40 rspcev 
 |-  ( ( ( _om .o a ) e. On /\ ( Lim ( _om .o a ) /\ A e. ( _om .o a ) ) ) -> E. x e. On ( Lim x /\ A e. x ) )
42 8 30 37 41 syl12anc 
 |-  ( ( A e. On /\ a e. On /\ ( A u. _om ) e. ( _om .o a ) ) -> E. x e. On ( Lim x /\ A e. x ) )
43 42 rexlimdv3a 
 |-  ( A e. On -> ( E. a e. On ( A u. _om ) e. ( _om .o a ) -> E. x e. On ( Lim x /\ A e. x ) ) )
44 5 43 mpd 
 |-  ( A e. On -> E. x e. On ( Lim x /\ A e. x ) )