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 e. On -> E. x e. On A e. ( _om .o x ) )

Proof

Step Hyp Ref Expression
1 omelon 
 |-  _om e. On
2 peano1 
 |-  (/) e. _om
3 2 ne0ii 
 |-  _om =/= (/)
4 omeu 
 |-  ( ( _om e. On /\ A e. On /\ _om =/= (/) ) -> E! c E. a e. On E. b e. _om ( c = <. a , b >. /\ ( ( _om .o a ) +o b ) = A ) )
5 1 3 4 mp3an13 
 |-  ( A e. On -> E! c E. a e. On E. b e. _om ( c = <. a , b >. /\ ( ( _om .o a ) +o b ) = A ) )
6 euex 
 |-  ( E! c E. a e. On E. b e. _om ( c = <. a , b >. /\ ( ( _om .o a ) +o b ) = A ) -> E. c E. a e. On E. b e. _om ( c = <. a , b >. /\ ( ( _om .o a ) +o b ) = A ) )
7 onsuc 
 |-  ( a e. On -> suc a e. On )
8 7 adantr 
 |-  ( ( a e. On /\ b e. _om ) -> suc a e. On )
9 simpr 
 |-  ( ( ( a e. On /\ b e. _om ) /\ ( ( _om .o a ) +o b ) = A ) -> ( ( _om .o a ) +o b ) = A )
10 simpr 
 |-  ( ( a e. On /\ b e. _om ) -> b e. _om )
11 simpl 
 |-  ( ( a e. On /\ b e. _om ) -> a e. On )
12 omcl 
 |-  ( ( _om e. On /\ a e. On ) -> ( _om .o a ) e. On )
13 1 11 12 sylancr 
 |-  ( ( a e. On /\ b e. _om ) -> ( _om .o a ) e. On )
14 oaordi 
 |-  ( ( _om e. On /\ ( _om .o a ) e. On ) -> ( b e. _om -> ( ( _om .o a ) +o b ) e. ( ( _om .o a ) +o _om ) ) )
15 1 13 14 sylancr 
 |-  ( ( a e. On /\ b e. _om ) -> ( b e. _om -> ( ( _om .o a ) +o b ) e. ( ( _om .o a ) +o _om ) ) )
16 10 15 mpd 
 |-  ( ( a e. On /\ b e. _om ) -> ( ( _om .o a ) +o b ) e. ( ( _om .o a ) +o _om ) )
17 omsuc 
 |-  ( ( _om e. On /\ a e. On ) -> ( _om .o suc a ) = ( ( _om .o a ) +o _om ) )
18 1 11 17 sylancr 
 |-  ( ( a e. On /\ b e. _om ) -> ( _om .o suc a ) = ( ( _om .o a ) +o _om ) )
19 16 18 eleqtrrd 
 |-  ( ( a e. On /\ b e. _om ) -> ( ( _om .o a ) +o b ) e. ( _om .o suc a ) )
20 19 adantr 
 |-  ( ( ( a e. On /\ b e. _om ) /\ ( ( _om .o a ) +o b ) = A ) -> ( ( _om .o a ) +o b ) e. ( _om .o suc a ) )
21 9 20 eqeltrrd 
 |-  ( ( ( a e. On /\ b e. _om ) /\ ( ( _om .o a ) +o b ) = A ) -> A e. ( _om .o suc a ) )
22 oveq2 
 |-  ( x = suc a -> ( _om .o x ) = ( _om .o suc a ) )
23 22 eleq2d 
 |-  ( x = suc a -> ( A e. ( _om .o x ) <-> A e. ( _om .o suc a ) ) )
24 23 rspcev 
 |-  ( ( suc a e. On /\ A e. ( _om .o suc a ) ) -> E. x e. On A e. ( _om .o x ) )
25 8 21 24 syl2an2r 
 |-  ( ( ( a e. On /\ b e. _om ) /\ ( ( _om .o a ) +o b ) = A ) -> E. x e. On A e. ( _om .o x ) )
26 25 ex 
 |-  ( ( a e. On /\ b e. _om ) -> ( ( ( _om .o a ) +o b ) = A -> E. x e. On A e. ( _om .o x ) ) )
27 26 adantld 
 |-  ( ( a e. On /\ b e. _om ) -> ( ( c = <. a , b >. /\ ( ( _om .o a ) +o b ) = A ) -> E. x e. On A e. ( _om .o x ) ) )
28 27 a1i 
 |-  ( A e. On -> ( ( a e. On /\ b e. _om ) -> ( ( c = <. a , b >. /\ ( ( _om .o a ) +o b ) = A ) -> E. x e. On A e. ( _om .o x ) ) ) )
29 28 rexlimdvv 
 |-  ( A e. On -> ( E. a e. On E. b e. _om ( c = <. a , b >. /\ ( ( _om .o a ) +o b ) = A ) -> E. x e. On A e. ( _om .o x ) ) )
30 29 exlimdv 
 |-  ( A e. On -> ( E. c E. a e. On E. b e. _om ( c = <. a , b >. /\ ( ( _om .o a ) +o b ) = A ) -> E. x e. On A e. ( _om .o x ) ) )
31 6 30 syl5 
 |-  ( A e. On -> ( E! c E. a e. On E. b e. _om ( c = <. a , b >. /\ ( ( _om .o a ) +o b ) = A ) -> E. x e. On A e. ( _om .o x ) ) )
32 5 31 mpd 
 |-  ( A e. On -> E. x e. On A e. ( _om .o x ) )