Metamath Proof Explorer

Theorem omltoe

Description: Exponentiation eventually dominates multiplication. (Contributed by RP, 3-Jan-2025)

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

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( A e. On /\ B e. On ) -> B e. On )
2 1 adantr 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( 1o e. A /\ A e. B ) ) -> B e. On )
3 oe2 
 |-  ( B e. On -> ( B .o B ) = ( B ^o 2o ) )
4 2 3 syl 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( 1o e. A /\ A e. B ) ) -> ( B .o B ) = ( B ^o 2o ) )
5 2on 
 |-  2o e. On
6 5 a1i 
 |-  ( ( A e. On /\ B e. On ) -> 2o e. On )
7 simpl 
 |-  ( ( A e. On /\ B e. On ) -> A e. On )
8 6 7 1 3jca 
 |-  ( ( A e. On /\ B e. On ) -> ( 2o e. On /\ A e. On /\ B e. On ) )
9 8 adantr 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( 1o e. A /\ A e. B ) ) -> ( 2o e. On /\ A e. On /\ B e. On ) )
10 simpr 
 |-  ( ( 1o e. A /\ A e. B ) -> A e. B )
11 10 adantl 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( 1o e. A /\ A e. B ) ) -> A e. B )
12 11 ne0d 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( 1o e. A /\ A e. B ) ) -> B =/= (/) )
13 on0eln0 
 |-  ( B e. On -> ( (/) e. B <-> B =/= (/) ) )
14 2 13 syl 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( 1o e. A /\ A e. B ) ) -> ( (/) e. B <-> B =/= (/) ) )
15 12 14 mpbird 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( 1o e. A /\ A e. B ) ) -> (/) e. B )
16 9 15 jca 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( 1o e. A /\ A e. B ) ) -> ( ( 2o e. On /\ A e. On /\ B e. On ) /\ (/) e. B ) )
17 df-2o 
 |-  2o = suc 1o
18 17 a1i 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( 1o e. A /\ A e. B ) ) -> 2o = suc 1o )
19 simpl 
 |-  ( ( 1o e. A /\ A e. B ) -> 1o e. A )
20 19 adantl 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( 1o e. A /\ A e. B ) ) -> 1o e. A )
21 eloni 
 |-  ( A e. On -> Ord A )
22 21 adantr 
 |-  ( ( A e. On /\ B e. On ) -> Ord A )
23 22 adantr 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( 1o e. A /\ A e. B ) ) -> Ord A )
24 20 23 jca 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( 1o e. A /\ A e. B ) ) -> ( 1o e. A /\ Ord A ) )
25 ordelsuc 
 |-  ( ( 1o e. A /\ Ord A ) -> ( 1o e. A <-> suc 1o C_ A ) )
26 25 biimpd 
 |-  ( ( 1o e. A /\ Ord A ) -> ( 1o e. A -> suc 1o C_ A ) )
27 24 20 26 sylc 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( 1o e. A /\ A e. B ) ) -> suc 1o C_ A )
28 18 27 eqsstrd 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( 1o e. A /\ A e. B ) ) -> 2o C_ A )
29 oewordi 
 |-  ( ( ( 2o e. On /\ A e. On /\ B e. On ) /\ (/) e. B ) -> ( 2o C_ A -> ( B ^o 2o ) C_ ( B ^o A ) ) )
30 16 28 29 sylc 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( 1o e. A /\ A e. B ) ) -> ( B ^o 2o ) C_ ( B ^o A ) )
31 4 30 eqsstrd 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( 1o e. A /\ A e. B ) ) -> ( B .o B ) C_ ( B ^o A ) )
32 2 2 15 jca31 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( 1o e. A /\ A e. B ) ) -> ( ( B e. On /\ B e. On ) /\ (/) e. B ) )
33 omordi 
 |-  ( ( ( B e. On /\ B e. On ) /\ (/) e. B ) -> ( A e. B -> ( B .o A ) e. ( B .o B ) ) )
34 32 11 33 sylc 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( 1o e. A /\ A e. B ) ) -> ( B .o A ) e. ( B .o B ) )
35 31 34 sseldd 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( 1o e. A /\ A e. B ) ) -> ( B .o A ) e. ( B ^o A ) )
36 35 ex 
 |-  ( ( A e. On /\ B e. On ) -> ( ( 1o e. A /\ A e. B ) -> ( B .o A ) e. ( B ^o A ) ) )