Metamath Proof Explorer

Theorem oeword

Description: Weak ordering property of ordinal exponentiation. (Contributed by NM, 6-Jan-2005) (Revised by Mario Carneiro, 24-May-2015)

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

Proof

Step Hyp Ref Expression
1 oeord 
 |-  ( ( A e. On /\ B e. On /\ C e. ( On \ 2o ) ) -> ( A e. B <-> ( C ^o A ) e. ( C ^o B ) ) )
2 oecan 
 |-  ( ( C e. ( On \ 2o ) /\ A e. On /\ B e. On ) -> ( ( C ^o A ) = ( C ^o B ) <-> A = B ) )
3 2 3coml 
 |-  ( ( A e. On /\ B e. On /\ C e. ( On \ 2o ) ) -> ( ( C ^o A ) = ( C ^o B ) <-> A = B ) )
4 3 bicomd 
 |-  ( ( A e. On /\ B e. On /\ C e. ( On \ 2o ) ) -> ( A = B <-> ( C ^o A ) = ( C ^o B ) ) )
5 1 4 orbi12d 
 |-  ( ( A e. On /\ B e. On /\ C e. ( On \ 2o ) ) -> ( ( A e. B \/ A = B ) <-> ( ( C ^o A ) e. ( C ^o B ) \/ ( C ^o A ) = ( C ^o B ) ) ) )
6 onsseleq 
 |-  ( ( A e. On /\ B e. On ) -> ( A C_ B <-> ( A e. B \/ A = B ) ) )
7 6 3adant3 
 |-  ( ( A e. On /\ B e. On /\ C e. ( On \ 2o ) ) -> ( A C_ B <-> ( A e. B \/ A = B ) ) )
8 eldifi 
 |-  ( C e. ( On \ 2o ) -> C e. On )
9 id 
 |-  ( ( A e. On /\ B e. On ) -> ( A e. On /\ B e. On ) )
10 oecl 
 |-  ( ( C e. On /\ A e. On ) -> ( C ^o A ) e. On )
11 oecl 
 |-  ( ( C e. On /\ B e. On ) -> ( C ^o B ) e. On )
12 10 11 anim12dan 
 |-  ( ( C e. On /\ ( A e. On /\ B e. On ) ) -> ( ( C ^o A ) e. On /\ ( C ^o B ) e. On ) )
13 onsseleq 
 |-  ( ( ( C ^o A ) e. On /\ ( C ^o B ) e. On ) -> ( ( C ^o A ) C_ ( C ^o B ) <-> ( ( C ^o A ) e. ( C ^o B ) \/ ( C ^o A ) = ( C ^o B ) ) ) )
14 12 13 syl 
 |-  ( ( C e. On /\ ( A e. On /\ B e. On ) ) -> ( ( C ^o A ) C_ ( C ^o B ) <-> ( ( C ^o A ) e. ( C ^o B ) \/ ( C ^o A ) = ( C ^o B ) ) ) )
15 8 9 14 syl2anr 
 |-  ( ( ( A e. On /\ B e. On ) /\ C e. ( On \ 2o ) ) -> ( ( C ^o A ) C_ ( C ^o B ) <-> ( ( C ^o A ) e. ( C ^o B ) \/ ( C ^o A ) = ( C ^o B ) ) ) )
16 15 3impa 
 |-  ( ( A e. On /\ B e. On /\ C e. ( On \ 2o ) ) -> ( ( C ^o A ) C_ ( C ^o B ) <-> ( ( C ^o A ) e. ( C ^o B ) \/ ( C ^o A ) = ( C ^o B ) ) ) )
17 5 7 16 3bitr4d 
 |-  ( ( A e. On /\ B e. On /\ C e. ( On \ 2o ) ) -> ( A C_ B <-> ( C ^o A ) C_ ( C ^o B ) ) )