Metamath Proof Explorer

Theorem oewordi

Description: Weak ordering property of ordinal exponentiation. (Contributed by NM, 6-Jan-2005)

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

Proof

Step Hyp Ref Expression
1 eloni 
 |-  ( C e. On -> Ord C )
2 ordgt0ge1 
 |-  ( Ord C -> ( (/) e. C <-> 1o C_ C ) )
3 1 2 syl 
 |-  ( C e. On -> ( (/) e. C <-> 1o C_ C ) )
4 1on 
 |-  1o e. On
5 onsseleq 
 |-  ( ( 1o e. On /\ C e. On ) -> ( 1o C_ C <-> ( 1o e. C \/ 1o = C ) ) )
6 4 5 mpan 
 |-  ( C e. On -> ( 1o C_ C <-> ( 1o e. C \/ 1o = C ) ) )
7 3 6 bitrd 
 |-  ( C e. On -> ( (/) e. C <-> ( 1o e. C \/ 1o = C ) ) )
8 7 3ad2ant3 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( (/) e. C <-> ( 1o e. C \/ 1o = C ) ) )
9 ondif2 
 |-  ( C e. ( On \ 2o ) <-> ( C e. On /\ 1o e. C ) )
10 oeword 
 |-  ( ( A e. On /\ B e. On /\ C e. ( On \ 2o ) ) -> ( A C_ B <-> ( C ^o A ) C_ ( C ^o B ) ) )
11 10 biimpd 
 |-  ( ( A e. On /\ B e. On /\ C e. ( On \ 2o ) ) -> ( A C_ B -> ( C ^o A ) C_ ( C ^o B ) ) )
12 11 3expia 
 |-  ( ( A e. On /\ B e. On ) -> ( C e. ( On \ 2o ) -> ( A C_ B -> ( C ^o A ) C_ ( C ^o B ) ) ) )
13 9 12 syl5bir 
 |-  ( ( A e. On /\ B e. On ) -> ( ( C e. On /\ 1o e. C ) -> ( A C_ B -> ( C ^o A ) C_ ( C ^o B ) ) ) )
14 13 expd 
 |-  ( ( A e. On /\ B e. On ) -> ( C e. On -> ( 1o e. C -> ( A C_ B -> ( C ^o A ) C_ ( C ^o B ) ) ) ) )
15 14 3impia 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( 1o e. C -> ( A C_ B -> ( C ^o A ) C_ ( C ^o B ) ) ) )
16 oe1m 
 |-  ( A e. On -> ( 1o ^o A ) = 1o )
17 16 adantr 
 |-  ( ( A e. On /\ B e. On ) -> ( 1o ^o A ) = 1o )
18 oe1m 
 |-  ( B e. On -> ( 1o ^o B ) = 1o )
19 18 adantl 
 |-  ( ( A e. On /\ B e. On ) -> ( 1o ^o B ) = 1o )
20 17 19 eqtr4d 
 |-  ( ( A e. On /\ B e. On ) -> ( 1o ^o A ) = ( 1o ^o B ) )
21 eqimss 
 |-  ( ( 1o ^o A ) = ( 1o ^o B ) -> ( 1o ^o A ) C_ ( 1o ^o B ) )
22 20 21 syl 
 |-  ( ( A e. On /\ B e. On ) -> ( 1o ^o A ) C_ ( 1o ^o B ) )
23 oveq1 
 |-  ( 1o = C -> ( 1o ^o A ) = ( C ^o A ) )
24 oveq1 
 |-  ( 1o = C -> ( 1o ^o B ) = ( C ^o B ) )
25 23 24 sseq12d 
 |-  ( 1o = C -> ( ( 1o ^o A ) C_ ( 1o ^o B ) <-> ( C ^o A ) C_ ( C ^o B ) ) )
26 22 25 syl5ibcom 
 |-  ( ( A e. On /\ B e. On ) -> ( 1o = C -> ( C ^o A ) C_ ( C ^o B ) ) )
27 26 3adant3 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( 1o = C -> ( C ^o A ) C_ ( C ^o B ) ) )
28 27 a1dd 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( 1o = C -> ( A C_ B -> ( C ^o A ) C_ ( C ^o B ) ) ) )
29 15 28 jaod 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( 1o e. C \/ 1o = C ) -> ( A C_ B -> ( C ^o A ) C_ ( C ^o B ) ) ) )
30 8 29 sylbid 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( (/) e. C -> ( A C_ B -> ( C ^o A ) C_ ( C ^o B ) ) ) )
31 30 imp 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ (/) e. C ) -> ( A C_ B -> ( C ^o A ) C_ ( C ^o B ) ) )