Metamath Proof Explorer

Theorem onexoegt

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

Ref Expression
Assertion onexoegt 
|- ( A e. On -> E. x e. On A e. ( _om ^o x ) )

Proof

Step Hyp Ref Expression
1 0elon 
 |-  (/) e. On
2 0lt1o 
 |-  (/) e. 1o
3 omelon 
 |-  _om e. On
4 oe0 
 |-  ( _om e. On -> ( _om ^o (/) ) = 1o )
5 3 4 ax-mp 
 |-  ( _om ^o (/) ) = 1o
6 2 5 eleqtrri 
 |-  (/) e. ( _om ^o (/) )
7 6 a1i 
 |-  ( A = (/) -> (/) e. ( _om ^o (/) ) )
8 oveq2 
 |-  ( x = (/) -> ( _om ^o x ) = ( _om ^o (/) ) )
9 8 eleq2d 
 |-  ( x = (/) -> ( (/) e. ( _om ^o x ) <-> (/) e. ( _om ^o (/) ) ) )
10 9 rspcev 
 |-  ( ( (/) e. On /\ (/) e. ( _om ^o (/) ) ) -> E. x e. On (/) e. ( _om ^o x ) )
11 1 7 10 sylancr 
 |-  ( A = (/) -> E. x e. On (/) e. ( _om ^o x ) )
12 eleq1 
 |-  ( A = (/) -> ( A e. ( _om ^o x ) <-> (/) e. ( _om ^o x ) ) )
13 12 rexbidv 
 |-  ( A = (/) -> ( E. x e. On A e. ( _om ^o x ) <-> E. x e. On (/) e. ( _om ^o x ) ) )
14 11 13 mpbird 
 |-  ( A = (/) -> E. x e. On A e. ( _om ^o x ) )
15 14 a1i 
 |-  ( A e. On -> ( A = (/) -> E. x e. On A e. ( _om ^o x ) ) )
16 1onn 
 |-  1o e. _om
17 ondif2 
 |-  ( _om e. ( On \ 2o ) <-> ( _om e. On /\ 1o e. _om ) )
18 3 16 17 mpbir2an 
 |-  _om e. ( On \ 2o )
19 ondif1 
 |-  ( A e. ( On \ 1o ) <-> ( A e. On /\ (/) e. A ) )
20 19 biimpri 
 |-  ( ( A e. On /\ (/) e. A ) -> A e. ( On \ 1o ) )
21 oeeu 
 |-  ( ( _om e. ( On \ 2o ) /\ A e. ( On \ 1o ) ) -> E! d E. a e. On E. b e. ( _om \ 1o ) E. c e. ( _om ^o a ) ( d = <. a , b , c >. /\ ( ( ( _om ^o a ) .o b ) +o c ) = A ) )
22 18 20 21 sylancr 
 |-  ( ( A e. On /\ (/) e. A ) -> E! d E. a e. On E. b e. ( _om \ 1o ) E. c e. ( _om ^o a ) ( d = <. a , b , c >. /\ ( ( ( _om ^o a ) .o b ) +o c ) = A ) )
23 euex 
 |-  ( E! d E. a e. On E. b e. ( _om \ 1o ) E. c e. ( _om ^o a ) ( d = <. a , b , c >. /\ ( ( ( _om ^o a ) .o b ) +o c ) = A ) -> E. d E. a e. On E. b e. ( _om \ 1o ) E. c e. ( _om ^o a ) ( d = <. a , b , c >. /\ ( ( ( _om ^o a ) .o b ) +o c ) = A ) )
24 simpr 
 |-  ( ( d = <. a , b , c >. /\ ( ( ( _om ^o a ) .o b ) +o c ) = A ) -> ( ( ( _om ^o a ) .o b ) +o c ) = A )
25 simp1 
 |-  ( ( a e. On /\ b e. ( _om \ 1o ) /\ c e. ( _om ^o a ) ) -> a e. On )
26 onsuc 
 |-  ( a e. On -> suc a e. On )
27 25 26 syl 
 |-  ( ( a e. On /\ b e. ( _om \ 1o ) /\ c e. ( _om ^o a ) ) -> suc a e. On )
28 27 adantl 
 |-  ( ( ( A e. On /\ (/) e. A ) /\ ( a e. On /\ b e. ( _om \ 1o ) /\ c e. ( _om ^o a ) ) ) -> suc a e. On )
29 simpr 
 |-  ( ( ( a e. On /\ b e. ( _om \ 1o ) /\ c e. ( _om ^o a ) ) /\ ( ( ( _om ^o a ) .o b ) +o c ) = A ) -> ( ( ( _om ^o a ) .o b ) +o c ) = A )
30 oecl 
 |-  ( ( _om e. On /\ a e. On ) -> ( _om ^o a ) e. On )
31 3 25 30 sylancr 
 |-  ( ( a e. On /\ b e. ( _om \ 1o ) /\ c e. ( _om ^o a ) ) -> ( _om ^o a ) e. On )
32 3 a1i 
 |-  ( ( a e. On /\ b e. ( _om \ 1o ) /\ c e. ( _om ^o a ) ) -> _om e. On )
33 omcl 
 |-  ( ( ( _om ^o a ) e. On /\ _om e. On ) -> ( ( _om ^o a ) .o _om ) e. On )
34 31 32 33 syl2anc 
 |-  ( ( a e. On /\ b e. ( _om \ 1o ) /\ c e. ( _om ^o a ) ) -> ( ( _om ^o a ) .o _om ) e. On )
35 simp3 
 |-  ( ( a e. On /\ b e. ( _om \ 1o ) /\ c e. ( _om ^o a ) ) -> c e. ( _om ^o a ) )
36 eldifi 
 |-  ( b e. ( _om \ 1o ) -> b e. _om )
37 nnon 
 |-  ( b e. _om -> b e. On )
38 36 37 syl 
 |-  ( b e. ( _om \ 1o ) -> b e. On )
39 38 3ad2ant2 
 |-  ( ( a e. On /\ b e. ( _om \ 1o ) /\ c e. ( _om ^o a ) ) -> b e. On )
40 omcl 
 |-  ( ( ( _om ^o a ) e. On /\ b e. On ) -> ( ( _om ^o a ) .o b ) e. On )
41 31 39 40 syl2anc 
 |-  ( ( a e. On /\ b e. ( _om \ 1o ) /\ c e. ( _om ^o a ) ) -> ( ( _om ^o a ) .o b ) e. On )
42 oaordi 
 |-  ( ( ( _om ^o a ) e. On /\ ( ( _om ^o a ) .o b ) e. On ) -> ( c e. ( _om ^o a ) -> ( ( ( _om ^o a ) .o b ) +o c ) e. ( ( ( _om ^o a ) .o b ) +o ( _om ^o a ) ) ) )
43 31 41 42 syl2anc 
 |-  ( ( a e. On /\ b e. ( _om \ 1o ) /\ c e. ( _om ^o a ) ) -> ( c e. ( _om ^o a ) -> ( ( ( _om ^o a ) .o b ) +o c ) e. ( ( ( _om ^o a ) .o b ) +o ( _om ^o a ) ) ) )
44 35 43 mpd 
 |-  ( ( a e. On /\ b e. ( _om \ 1o ) /\ c e. ( _om ^o a ) ) -> ( ( ( _om ^o a ) .o b ) +o c ) e. ( ( ( _om ^o a ) .o b ) +o ( _om ^o a ) ) )
45 omsuc 
 |-  ( ( ( _om ^o a ) e. On /\ b e. On ) -> ( ( _om ^o a ) .o suc b ) = ( ( ( _om ^o a ) .o b ) +o ( _om ^o a ) ) )
46 31 39 45 syl2anc 
 |-  ( ( a e. On /\ b e. ( _om \ 1o ) /\ c e. ( _om ^o a ) ) -> ( ( _om ^o a ) .o suc b ) = ( ( ( _om ^o a ) .o b ) +o ( _om ^o a ) ) )
47 44 46 eleqtrrd 
 |-  ( ( a e. On /\ b e. ( _om \ 1o ) /\ c e. ( _om ^o a ) ) -> ( ( ( _om ^o a ) .o b ) +o c ) e. ( ( _om ^o a ) .o suc b ) )
48 36 3ad2ant2 
 |-  ( ( a e. On /\ b e. ( _om \ 1o ) /\ c e. ( _om ^o a ) ) -> b e. _om )
49 peano2 
 |-  ( b e. _om -> suc b e. _om )
50 48 49 syl 
 |-  ( ( a e. On /\ b e. ( _om \ 1o ) /\ c e. ( _om ^o a ) ) -> suc b e. _om )
51 peano1 
 |-  (/) e. _om
52 51 a1i 
 |-  ( ( a e. On /\ b e. ( _om \ 1o ) /\ c e. ( _om ^o a ) ) -> (/) e. _om )
53 oen0 
 |-  ( ( ( _om e. On /\ a e. On ) /\ (/) e. _om ) -> (/) e. ( _om ^o a ) )
54 32 25 52 53 syl21anc 
 |-  ( ( a e. On /\ b e. ( _om \ 1o ) /\ c e. ( _om ^o a ) ) -> (/) e. ( _om ^o a ) )
55 omordi 
 |-  ( ( ( _om e. On /\ ( _om ^o a ) e. On ) /\ (/) e. ( _om ^o a ) ) -> ( suc b e. _om -> ( ( _om ^o a ) .o suc b ) e. ( ( _om ^o a ) .o _om ) ) )
56 32 31 54 55 syl21anc 
 |-  ( ( a e. On /\ b e. ( _om \ 1o ) /\ c e. ( _om ^o a ) ) -> ( suc b e. _om -> ( ( _om ^o a ) .o suc b ) e. ( ( _om ^o a ) .o _om ) ) )
57 50 56 mpd 
 |-  ( ( a e. On /\ b e. ( _om \ 1o ) /\ c e. ( _om ^o a ) ) -> ( ( _om ^o a ) .o suc b ) e. ( ( _om ^o a ) .o _om ) )
58 ontr1 
 |-  ( ( ( _om ^o a ) .o _om ) e. On -> ( ( ( ( ( _om ^o a ) .o b ) +o c ) e. ( ( _om ^o a ) .o suc b ) /\ ( ( _om ^o a ) .o suc b ) e. ( ( _om ^o a ) .o _om ) ) -> ( ( ( _om ^o a ) .o b ) +o c ) e. ( ( _om ^o a ) .o _om ) ) )
59 58 imp 
 |-  ( ( ( ( _om ^o a ) .o _om ) e. On /\ ( ( ( ( _om ^o a ) .o b ) +o c ) e. ( ( _om ^o a ) .o suc b ) /\ ( ( _om ^o a ) .o suc b ) e. ( ( _om ^o a ) .o _om ) ) ) -> ( ( ( _om ^o a ) .o b ) +o c ) e. ( ( _om ^o a ) .o _om ) )
60 34 47 57 59 syl12anc 
 |-  ( ( a e. On /\ b e. ( _om \ 1o ) /\ c e. ( _om ^o a ) ) -> ( ( ( _om ^o a ) .o b ) +o c ) e. ( ( _om ^o a ) .o _om ) )
61 oesuc 
 |-  ( ( _om e. On /\ a e. On ) -> ( _om ^o suc a ) = ( ( _om ^o a ) .o _om ) )
62 3 25 61 sylancr 
 |-  ( ( a e. On /\ b e. ( _om \ 1o ) /\ c e. ( _om ^o a ) ) -> ( _om ^o suc a ) = ( ( _om ^o a ) .o _om ) )
63 60 62 eleqtrrd 
 |-  ( ( a e. On /\ b e. ( _om \ 1o ) /\ c e. ( _om ^o a ) ) -> ( ( ( _om ^o a ) .o b ) +o c ) e. ( _om ^o suc a ) )
64 63 adantr 
 |-  ( ( ( a e. On /\ b e. ( _om \ 1o ) /\ c e. ( _om ^o a ) ) /\ ( ( ( _om ^o a ) .o b ) +o c ) = A ) -> ( ( ( _om ^o a ) .o b ) +o c ) e. ( _om ^o suc a ) )
65 29 64 eqeltrrd 
 |-  ( ( ( a e. On /\ b e. ( _om \ 1o ) /\ c e. ( _om ^o a ) ) /\ ( ( ( _om ^o a ) .o b ) +o c ) = A ) -> A e. ( _om ^o suc a ) )
66 65 adantll 
 |-  ( ( ( ( A e. On /\ (/) e. A ) /\ ( a e. On /\ b e. ( _om \ 1o ) /\ c e. ( _om ^o a ) ) ) /\ ( ( ( _om ^o a ) .o b ) +o c ) = A ) -> A e. ( _om ^o suc a ) )
67 oveq2 
 |-  ( x = suc a -> ( _om ^o x ) = ( _om ^o suc a ) )
68 67 eleq2d 
 |-  ( x = suc a -> ( A e. ( _om ^o x ) <-> A e. ( _om ^o suc a ) ) )
69 68 rspcev 
 |-  ( ( suc a e. On /\ A e. ( _om ^o suc a ) ) -> E. x e. On A e. ( _om ^o x ) )
70 28 66 69 syl2an2r 
 |-  ( ( ( ( A e. On /\ (/) e. A ) /\ ( a e. On /\ b e. ( _om \ 1o ) /\ c e. ( _om ^o a ) ) ) /\ ( ( ( _om ^o a ) .o b ) +o c ) = A ) -> E. x e. On A e. ( _om ^o x ) )
71 70 ex 
 |-  ( ( ( A e. On /\ (/) e. A ) /\ ( a e. On /\ b e. ( _om \ 1o ) /\ c e. ( _om ^o a ) ) ) -> ( ( ( ( _om ^o a ) .o b ) +o c ) = A -> E. x e. On A e. ( _om ^o x ) ) )
72 24 71 syl5 
 |-  ( ( ( A e. On /\ (/) e. A ) /\ ( a e. On /\ b e. ( _om \ 1o ) /\ c e. ( _om ^o a ) ) ) -> ( ( d = <. a , b , c >. /\ ( ( ( _om ^o a ) .o b ) +o c ) = A ) -> E. x e. On A e. ( _om ^o x ) ) )
73 72 3exp2 
 |-  ( ( A e. On /\ (/) e. A ) -> ( a e. On -> ( b e. ( _om \ 1o ) -> ( c e. ( _om ^o a ) -> ( ( d = <. a , b , c >. /\ ( ( ( _om ^o a ) .o b ) +o c ) = A ) -> E. x e. On A e. ( _om ^o x ) ) ) ) ) )
74 73 imp4b 
 |-  ( ( ( A e. On /\ (/) e. A ) /\ a e. On ) -> ( ( b e. ( _om \ 1o ) /\ c e. ( _om ^o a ) ) -> ( ( d = <. a , b , c >. /\ ( ( ( _om ^o a ) .o b ) +o c ) = A ) -> E. x e. On A e. ( _om ^o x ) ) ) )
75 74 rexlimdvv 
 |-  ( ( ( A e. On /\ (/) e. A ) /\ a e. On ) -> ( E. b e. ( _om \ 1o ) E. c e. ( _om ^o a ) ( d = <. a , b , c >. /\ ( ( ( _om ^o a ) .o b ) +o c ) = A ) -> E. x e. On A e. ( _om ^o x ) ) )
76 75 rexlimdva 
 |-  ( ( A e. On /\ (/) e. A ) -> ( E. a e. On E. b e. ( _om \ 1o ) E. c e. ( _om ^o a ) ( d = <. a , b , c >. /\ ( ( ( _om ^o a ) .o b ) +o c ) = A ) -> E. x e. On A e. ( _om ^o x ) ) )
77 76 exlimdv 
 |-  ( ( A e. On /\ (/) e. A ) -> ( E. d E. a e. On E. b e. ( _om \ 1o ) E. c e. ( _om ^o a ) ( d = <. a , b , c >. /\ ( ( ( _om ^o a ) .o b ) +o c ) = A ) -> E. x e. On A e. ( _om ^o x ) ) )
78 23 77 syl5 
 |-  ( ( A e. On /\ (/) e. A ) -> ( E! d E. a e. On E. b e. ( _om \ 1o ) E. c e. ( _om ^o a ) ( d = <. a , b , c >. /\ ( ( ( _om ^o a ) .o b ) +o c ) = A ) -> E. x e. On A e. ( _om ^o x ) ) )
79 22 78 mpd 
 |-  ( ( A e. On /\ (/) e. A ) -> E. x e. On A e. ( _om ^o x ) )
80 79 ex 
 |-  ( A e. On -> ( (/) e. A -> E. x e. On A e. ( _om ^o x ) ) )
81 on0eqel 
 |-  ( A e. On -> ( A = (/) \/ (/) e. A ) )
82 15 80 81 mpjaod 
 |-  ( A e. On -> E. x e. On A e. ( _om ^o x ) )