Metamath Proof Explorer

Theorem nnoeomeqom

Description: Any natural number at least as large as two raised to the power of omega is omega. Lemma 3.25 of Schloeder p. 11. (Contributed by RP, 30-Jan-2025)

Ref Expression
Assertion nnoeomeqom 
|- ( ( A e. _om /\ 1o e. A ) -> ( A ^o _om ) = _om )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( A e. _om /\ 1o e. A ) -> A e. _om )
2 nnon 
 |-  ( A e. _om -> A e. On )
3 1 2 syl 
 |-  ( ( A e. _om /\ 1o e. A ) -> A e. On )
4 omelon 
 |-  _om e. On
5 limom 
 |-  Lim _om
6 4 5 pm3.2i 
 |-  ( _om e. On /\ Lim _om )
7 6 a1i 
 |-  ( ( A e. _om /\ 1o e. A ) -> ( _om e. On /\ Lim _om ) )
8 0elon 
 |-  (/) e. On
9 8 a1i 
 |-  ( ( A e. _om /\ 1o e. A ) -> (/) e. On )
10 0ss 
 |-  (/) C_ 1o
11 10 a1i 
 |-  ( ( A e. _om /\ 1o e. A ) -> (/) C_ 1o )
12 simpr 
 |-  ( ( A e. _om /\ 1o e. A ) -> 1o e. A )
13 ontr2 
 |-  ( ( (/) e. On /\ A e. On ) -> ( ( (/) C_ 1o /\ 1o e. A ) -> (/) e. A ) )
14 13 imp 
 |-  ( ( ( (/) e. On /\ A e. On ) /\ ( (/) C_ 1o /\ 1o e. A ) ) -> (/) e. A )
15 9 3 11 12 14 syl22anc 
 |-  ( ( A e. _om /\ 1o e. A ) -> (/) e. A )
16 oelim 
 |-  ( ( ( A e. On /\ ( _om e. On /\ Lim _om ) ) /\ (/) e. A ) -> ( A ^o _om ) = U_ x e. _om ( A ^o x ) )
17 3 7 15 16 syl21anc 
 |-  ( ( A e. _om /\ 1o e. A ) -> ( A ^o _om ) = U_ x e. _om ( A ^o x ) )
18 ovex 
 |-  ( A ^o x ) e. _V
19 18 dfiun2 
 |-  U_ x e. _om ( A ^o x ) = U. { y | E. x e. _om y = ( A ^o x ) }
20 eluniab 
 |-  ( z e. U. { y | E. x e. _om y = ( A ^o x ) } <-> E. y ( z e. y /\ E. x e. _om y = ( A ^o x ) ) )
21 19.42v 
 |-  ( E. x ( z e. y /\ ( x e. _om /\ y = ( A ^o x ) ) ) <-> ( z e. y /\ E. x ( x e. _om /\ y = ( A ^o x ) ) ) )
22 3anass 
 |-  ( ( z e. y /\ x e. _om /\ y = ( A ^o x ) ) <-> ( z e. y /\ ( x e. _om /\ y = ( A ^o x ) ) ) )
23 22 exbii 
 |-  ( E. x ( z e. y /\ x e. _om /\ y = ( A ^o x ) ) <-> E. x ( z e. y /\ ( x e. _om /\ y = ( A ^o x ) ) ) )
24 df-rex 
 |-  ( E. x e. _om y = ( A ^o x ) <-> E. x ( x e. _om /\ y = ( A ^o x ) ) )
25 24 anbi2i 
 |-  ( ( z e. y /\ E. x e. _om y = ( A ^o x ) ) <-> ( z e. y /\ E. x ( x e. _om /\ y = ( A ^o x ) ) ) )
26 21 23 25 3bitr4ri 
 |-  ( ( z e. y /\ E. x e. _om y = ( A ^o x ) ) <-> E. x ( z e. y /\ x e. _om /\ y = ( A ^o x ) ) )
27 26 exbii 
 |-  ( E. y ( z e. y /\ E. x e. _om y = ( A ^o x ) ) <-> E. y E. x ( z e. y /\ x e. _om /\ y = ( A ^o x ) ) )
28 excom 
 |-  ( E. y E. x ( z e. y /\ x e. _om /\ y = ( A ^o x ) ) <-> E. x E. y ( z e. y /\ x e. _om /\ y = ( A ^o x ) ) )
29 20 27 28 3bitri 
 |-  ( z e. U. { y | E. x e. _om y = ( A ^o x ) } <-> E. x E. y ( z e. y /\ x e. _om /\ y = ( A ^o x ) ) )
30 simpr3 
 |-  ( ( ( A e. _om /\ 1o e. A ) /\ ( z e. y /\ x e. _om /\ y = ( A ^o x ) ) ) -> y = ( A ^o x ) )
31 simp2 
 |-  ( ( z e. y /\ x e. _om /\ y = ( A ^o x ) ) -> x e. _om )
32 nnecl 
 |-  ( ( A e. _om /\ x e. _om ) -> ( A ^o x ) e. _om )
33 1 31 32 syl2an 
 |-  ( ( ( A e. _om /\ 1o e. A ) /\ ( z e. y /\ x e. _om /\ y = ( A ^o x ) ) ) -> ( A ^o x ) e. _om )
34 onelss 
 |-  ( _om e. On -> ( ( A ^o x ) e. _om -> ( A ^o x ) C_ _om ) )
35 4 33 34 mpsyl 
 |-  ( ( ( A e. _om /\ 1o e. A ) /\ ( z e. y /\ x e. _om /\ y = ( A ^o x ) ) ) -> ( A ^o x ) C_ _om )
36 30 35 eqsstrd 
 |-  ( ( ( A e. _om /\ 1o e. A ) /\ ( z e. y /\ x e. _om /\ y = ( A ^o x ) ) ) -> y C_ _om )
37 simpr1 
 |-  ( ( ( A e. _om /\ 1o e. A ) /\ ( z e. y /\ x e. _om /\ y = ( A ^o x ) ) ) -> z e. y )
38 36 37 sseldd 
 |-  ( ( ( A e. _om /\ 1o e. A ) /\ ( z e. y /\ x e. _om /\ y = ( A ^o x ) ) ) -> z e. _om )
39 38 ex 
 |-  ( ( A e. _om /\ 1o e. A ) -> ( ( z e. y /\ x e. _om /\ y = ( A ^o x ) ) -> z e. _om ) )
40 39 exlimdvv 
 |-  ( ( A e. _om /\ 1o e. A ) -> ( E. x E. y ( z e. y /\ x e. _om /\ y = ( A ^o x ) ) -> z e. _om ) )
41 peano2 
 |-  ( z e. _om -> suc z e. _om )
42 41 adantl 
 |-  ( ( ( A e. _om /\ 1o e. A ) /\ z e. _om ) -> suc z e. _om )
43 ovex 
 |-  ( A ^o suc z ) e. _V
44 43 a1i 
 |-  ( ( ( A e. _om /\ 1o e. A ) /\ z e. _om ) -> ( A ^o suc z ) e. _V )
45 2 anim1i 
 |-  ( ( A e. _om /\ 1o e. A ) -> ( A e. On /\ 1o e. A ) )
46 ondif2 
 |-  ( A e. ( On \ 2o ) <-> ( A e. On /\ 1o e. A ) )
47 45 46 sylibr 
 |-  ( ( A e. _om /\ 1o e. A ) -> A e. ( On \ 2o ) )
48 nnon 
 |-  ( suc z e. _om -> suc z e. On )
49 41 48 syl 
 |-  ( z e. _om -> suc z e. On )
50 oeworde 
 |-  ( ( A e. ( On \ 2o ) /\ suc z e. On ) -> suc z C_ ( A ^o suc z ) )
51 47 49 50 syl2an 
 |-  ( ( ( A e. _om /\ 1o e. A ) /\ z e. _om ) -> suc z C_ ( A ^o suc z ) )
52 vex 
 |-  z e. _V
53 52 sucid 
 |-  z e. suc z
54 53 a1i 
 |-  ( ( ( A e. _om /\ 1o e. A ) /\ z e. _om ) -> z e. suc z )
55 51 54 sseldd 
 |-  ( ( ( A e. _om /\ 1o e. A ) /\ z e. _om ) -> z e. ( A ^o suc z ) )
56 eqidd 
 |-  ( ( ( A e. _om /\ 1o e. A ) /\ z e. _om ) -> ( A ^o suc z ) = ( A ^o suc z ) )
57 55 42 56 3jca 
 |-  ( ( ( A e. _om /\ 1o e. A ) /\ z e. _om ) -> ( z e. ( A ^o suc z ) /\ suc z e. _om /\ ( A ^o suc z ) = ( A ^o suc z ) ) )
58 eleq2 
 |-  ( y = ( A ^o suc z ) -> ( z e. y <-> z e. ( A ^o suc z ) ) )
59 eqeq1 
 |-  ( y = ( A ^o suc z ) -> ( y = ( A ^o suc z ) <-> ( A ^o suc z ) = ( A ^o suc z ) ) )
60 58 59 3anbi13d 
 |-  ( y = ( A ^o suc z ) -> ( ( z e. y /\ suc z e. _om /\ y = ( A ^o suc z ) ) <-> ( z e. ( A ^o suc z ) /\ suc z e. _om /\ ( A ^o suc z ) = ( A ^o suc z ) ) ) )
61 44 57 60 spcedv 
 |-  ( ( ( A e. _om /\ 1o e. A ) /\ z e. _om ) -> E. y ( z e. y /\ suc z e. _om /\ y = ( A ^o suc z ) ) )
62 eleq1 
 |-  ( x = suc z -> ( x e. _om <-> suc z e. _om ) )
63 oveq2 
 |-  ( x = suc z -> ( A ^o x ) = ( A ^o suc z ) )
64 63 eqeq2d 
 |-  ( x = suc z -> ( y = ( A ^o x ) <-> y = ( A ^o suc z ) ) )
65 62 64 3anbi23d 
 |-  ( x = suc z -> ( ( z e. y /\ x e. _om /\ y = ( A ^o x ) ) <-> ( z e. y /\ suc z e. _om /\ y = ( A ^o suc z ) ) ) )
66 65 exbidv 
 |-  ( x = suc z -> ( E. y ( z e. y /\ x e. _om /\ y = ( A ^o x ) ) <-> E. y ( z e. y /\ suc z e. _om /\ y = ( A ^o suc z ) ) ) )
67 42 61 66 spcedv 
 |-  ( ( ( A e. _om /\ 1o e. A ) /\ z e. _om ) -> E. x E. y ( z e. y /\ x e. _om /\ y = ( A ^o x ) ) )
68 67 ex 
 |-  ( ( A e. _om /\ 1o e. A ) -> ( z e. _om -> E. x E. y ( z e. y /\ x e. _om /\ y = ( A ^o x ) ) ) )
69 40 68 impbid 
 |-  ( ( A e. _om /\ 1o e. A ) -> ( E. x E. y ( z e. y /\ x e. _om /\ y = ( A ^o x ) ) <-> z e. _om ) )
70 29 69 bitrid 
 |-  ( ( A e. _om /\ 1o e. A ) -> ( z e. U. { y | E. x e. _om y = ( A ^o x ) } <-> z e. _om ) )
71 70 eqrdv 
 |-  ( ( A e. _om /\ 1o e. A ) -> U. { y | E. x e. _om y = ( A ^o x ) } = _om )
72 19 71 eqtrid 
 |-  ( ( A e. _om /\ 1o e. A ) -> U_ x e. _om ( A ^o x ) = _om )
73 17 72 eqtrd 
 |-  ( ( A e. _om /\ 1o e. A ) -> ( A ^o _om ) = _om )