Metamath Proof Explorer

Theorem omword

Description: Weak ordering property of ordinal multiplication. (Contributed by NM, 21-Dec-2004)

Ref Expression
Assertion omword 
|- ( ( ( 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 omord2 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ (/) e. C ) -> ( A e. B <-> ( C .o A ) e. ( C .o B ) ) )
2 3anrot 
 |-  ( ( C e. On /\ A e. On /\ B e. On ) <-> ( A e. On /\ B e. On /\ C e. On ) )
3 omcan 
 |-  ( ( ( C e. On /\ A e. On /\ B e. On ) /\ (/) e. C ) -> ( ( C .o A ) = ( C .o B ) <-> A = B ) )
4 2 3 sylanbr 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ (/) e. C ) -> ( ( C .o A ) = ( C .o B ) <-> A = B ) )
5 4 bicomd 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ (/) e. C ) -> ( A = B <-> ( C .o A ) = ( C .o B ) ) )
6 1 5 orbi12d 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ (/) e. C ) -> ( ( A e. B \/ A = B ) <-> ( ( C .o A ) e. ( C .o B ) \/ ( C .o A ) = ( C .o B ) ) ) )
7 onsseleq 
 |-  ( ( A e. On /\ B e. On ) -> ( A C_ B <-> ( A e. B \/ A = B ) ) )
8 7 3adant3 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( A C_ B <-> ( A e. B \/ A = B ) ) )
9 8 adantr 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ (/) e. C ) -> ( A C_ B <-> ( A e. B \/ A = B ) ) )
10 omcl 
 |-  ( ( C e. On /\ A e. On ) -> ( C .o A ) e. On )
11 omcl 
 |-  ( ( 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 12 ancoms 
 |-  ( ( ( A e. On /\ B e. On ) /\ C e. On ) -> ( ( C .o A ) e. On /\ ( C .o B ) e. On ) )
14 13 3impa 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( C .o A ) e. On /\ ( C .o B ) e. On ) )
15 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 ) ) ) )
16 14 15 syl 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( C .o A ) C_ ( C .o B ) <-> ( ( C .o A ) e. ( C .o B ) \/ ( C .o A ) = ( C .o B ) ) ) )
17 16 adantr 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ (/) e. C ) -> ( ( C .o A ) C_ ( C .o B ) <-> ( ( C .o A ) e. ( C .o B ) \/ ( C .o A ) = ( C .o B ) ) ) )
18 6 9 17 3bitr4d 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ (/) e. C ) -> ( A C_ B <-> ( C .o A ) C_ ( C .o B ) ) )