Metamath Proof Explorer

Theorem oege2

Description: Any power of an ordinal at least as large as two is greater-than-or-equal to the term on the right. Lemma 3.20 of Schloeder p. 10. See oeworde . (Contributed by RP, 29-Jan-2025)

Ref Expression
Assertion oege2 
|- ( ( ( A e. On /\ 1o e. A ) /\ B e. On ) -> B C_ ( A ^o B ) )

Proof

Step Hyp Ref Expression
1 2on 
 |-  2o e. On
2 1oex 
 |-  1o e. _V
3 2 prid2 
 |-  1o e. { (/) , 1o }
4 df2o3 
 |-  2o = { (/) , 1o }
5 3 4 eleqtrri 
 |-  1o e. 2o
6 ondif2 
 |-  ( 2o e. ( On \ 2o ) <-> ( 2o e. On /\ 1o e. 2o ) )
7 1 5 6 mpbir2an 
 |-  2o e. ( On \ 2o )
8 oeworde 
 |-  ( ( 2o e. ( On \ 2o ) /\ B e. On ) -> B C_ ( 2o ^o B ) )
9 7 8 mpan 
 |-  ( B e. On -> B C_ ( 2o ^o B ) )
10 9 adantl 
 |-  ( ( ( A e. On /\ 1o e. A ) /\ B e. On ) -> B C_ ( 2o ^o B ) )
11 df-2o 
 |-  2o = suc 1o
12 onsucss 
 |-  ( A e. On -> ( 1o e. A -> suc 1o C_ A ) )
13 12 imp 
 |-  ( ( A e. On /\ 1o e. A ) -> suc 1o C_ A )
14 13 adantr 
 |-  ( ( ( A e. On /\ 1o e. A ) /\ B e. On ) -> suc 1o C_ A )
15 11 14 eqsstrid 
 |-  ( ( ( A e. On /\ 1o e. A ) /\ B e. On ) -> 2o C_ A )
16 simpll 
 |-  ( ( ( A e. On /\ 1o e. A ) /\ B e. On ) -> A e. On )
17 onsseleq 
 |-  ( ( 2o e. On /\ A e. On ) -> ( 2o C_ A <-> ( 2o e. A \/ 2o = A ) ) )
18 1 16 17 sylancr 
 |-  ( ( ( A e. On /\ 1o e. A ) /\ B e. On ) -> ( 2o C_ A <-> ( 2o e. A \/ 2o = A ) ) )
19 oewordri 
 |-  ( ( A e. On /\ B e. On ) -> ( 2o e. A -> ( 2o ^o B ) C_ ( A ^o B ) ) )
20 19 adantlr 
 |-  ( ( ( A e. On /\ 1o e. A ) /\ B e. On ) -> ( 2o e. A -> ( 2o ^o B ) C_ ( A ^o B ) ) )
21 oveq1 
 |-  ( 2o = A -> ( 2o ^o B ) = ( A ^o B ) )
22 ssid 
 |-  ( A ^o B ) C_ ( A ^o B )
23 21 22 eqsstrdi 
 |-  ( 2o = A -> ( 2o ^o B ) C_ ( A ^o B ) )
24 23 a1i 
 |-  ( ( ( A e. On /\ 1o e. A ) /\ B e. On ) -> ( 2o = A -> ( 2o ^o B ) C_ ( A ^o B ) ) )
25 20 24 jaod 
 |-  ( ( ( A e. On /\ 1o e. A ) /\ B e. On ) -> ( ( 2o e. A \/ 2o = A ) -> ( 2o ^o B ) C_ ( A ^o B ) ) )
26 18 25 sylbid 
 |-  ( ( ( A e. On /\ 1o e. A ) /\ B e. On ) -> ( 2o C_ A -> ( 2o ^o B ) C_ ( A ^o B ) ) )
27 15 26 mpd 
 |-  ( ( ( A e. On /\ 1o e. A ) /\ B e. On ) -> ( 2o ^o B ) C_ ( A ^o B ) )
28 10 27 sstrd 
 |-  ( ( ( A e. On /\ 1o e. A ) /\ B e. On ) -> B C_ ( A ^o B ) )