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