Metamath Proof Explorer

Theorem nnmword

Description: Weak ordering property of ordinal multiplication. (Contributed by Mario Carneiro, 17-Nov-2014)

Ref Expression
Assertion nnmword 
|- ( ( ( A e. _om /\ B e. _om /\ C e. _om ) /\ (/) e. C ) -> ( A C_ B <-> ( C .o A ) C_ ( C .o B ) ) )

Proof

Step Hyp Ref Expression
1 iba 
 |-  ( (/) e. C -> ( B e. A <-> ( B e. A /\ (/) e. C ) ) )
2 nnmord 
 |-  ( ( B e. _om /\ A e. _om /\ C e. _om ) -> ( ( B e. A /\ (/) e. C ) <-> ( C .o B ) e. ( C .o A ) ) )
3 2 3com12 
 |-  ( ( A e. _om /\ B e. _om /\ C e. _om ) -> ( ( B e. A /\ (/) e. C ) <-> ( C .o B ) e. ( C .o A ) ) )
4 1 3 sylan9bbr 
 |-  ( ( ( A e. _om /\ B e. _om /\ C e. _om ) /\ (/) e. C ) -> ( B e. A <-> ( C .o B ) e. ( C .o A ) ) )
5 4 notbid 
 |-  ( ( ( A e. _om /\ B e. _om /\ C e. _om ) /\ (/) e. C ) -> ( -. B e. A <-> -. ( C .o B ) e. ( C .o A ) ) )
6 simpl1 
 |-  ( ( ( A e. _om /\ B e. _om /\ C e. _om ) /\ (/) e. C ) -> A e. _om )
7 nnon 
 |-  ( A e. _om -> A e. On )
8 6 7 syl 
 |-  ( ( ( A e. _om /\ B e. _om /\ C e. _om ) /\ (/) e. C ) -> A e. On )
9 simpl2 
 |-  ( ( ( A e. _om /\ B e. _om /\ C e. _om ) /\ (/) e. C ) -> B e. _om )
10 nnon 
 |-  ( B e. _om -> B e. On )
11 9 10 syl 
 |-  ( ( ( A e. _om /\ B e. _om /\ C e. _om ) /\ (/) e. C ) -> B e. On )
12 ontri1 
 |-  ( ( A e. On /\ B e. On ) -> ( A C_ B <-> -. B e. A ) )
13 8 11 12 syl2anc 
 |-  ( ( ( A e. _om /\ B e. _om /\ C e. _om ) /\ (/) e. C ) -> ( A C_ B <-> -. B e. A ) )
14 simpl3 
 |-  ( ( ( A e. _om /\ B e. _om /\ C e. _om ) /\ (/) e. C ) -> C e. _om )
15 nnmcl 
 |-  ( ( C e. _om /\ A e. _om ) -> ( C .o A ) e. _om )
16 14 6 15 syl2anc 
 |-  ( ( ( A e. _om /\ B e. _om /\ C e. _om ) /\ (/) e. C ) -> ( C .o A ) e. _om )
17 nnon 
 |-  ( ( C .o A ) e. _om -> ( C .o A ) e. On )
18 16 17 syl 
 |-  ( ( ( A e. _om /\ B e. _om /\ C e. _om ) /\ (/) e. C ) -> ( C .o A ) e. On )
19 nnmcl 
 |-  ( ( C e. _om /\ B e. _om ) -> ( C .o B ) e. _om )
20 14 9 19 syl2anc 
 |-  ( ( ( A e. _om /\ B e. _om /\ C e. _om ) /\ (/) e. C ) -> ( C .o B ) e. _om )
21 nnon 
 |-  ( ( C .o B ) e. _om -> ( C .o B ) e. On )
22 20 21 syl 
 |-  ( ( ( A e. _om /\ B e. _om /\ C e. _om ) /\ (/) e. C ) -> ( C .o B ) e. On )
23 ontri1 
 |-  ( ( ( C .o A ) e. On /\ ( C .o B ) e. On ) -> ( ( C .o A ) C_ ( C .o B ) <-> -. ( C .o B ) e. ( C .o A ) ) )
24 18 22 23 syl2anc 
 |-  ( ( ( A e. _om /\ B e. _om /\ C e. _om ) /\ (/) e. C ) -> ( ( C .o A ) C_ ( C .o B ) <-> -. ( C .o B ) e. ( C .o A ) ) )
25 5 13 24 3bitr4d 
 |-  ( ( ( A e. _om /\ B e. _om /\ C e. _om ) /\ (/) e. C ) -> ( A C_ B <-> ( C .o A ) C_ ( C .o B ) ) )