Metamath Proof Explorer

Theorem omwordi

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

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

Proof

Step Hyp Ref Expression
1 omword 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ (/) e. C ) -> ( A C_ B <-> ( C .o A ) C_ ( C .o B ) ) )
2 1 biimpd 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ (/) e. C ) -> ( A C_ B -> ( C .o A ) C_ ( C .o B ) ) )
3 2 ex 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( (/) e. C -> ( A C_ B -> ( C .o A ) C_ ( C .o B ) ) ) )
4 eloni 
 |-  ( C e. On -> Ord C )
5 ord0eln0 
 |-  ( Ord C -> ( (/) e. C <-> C =/= (/) ) )
6 5 necon2bbid 
 |-  ( Ord C -> ( C = (/) <-> -. (/) e. C ) )
7 4 6 syl 
 |-  ( C e. On -> ( C = (/) <-> -. (/) e. C ) )
8 7 3ad2ant3 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( C = (/) <-> -. (/) e. C ) )
9 ssid 
 |-  (/) C_ (/)
10 om0r 
 |-  ( A e. On -> ( (/) .o A ) = (/) )
11 10 adantr 
 |-  ( ( A e. On /\ B e. On ) -> ( (/) .o A ) = (/) )
12 om0r 
 |-  ( B e. On -> ( (/) .o B ) = (/) )
13 12 adantl 
 |-  ( ( A e. On /\ B e. On ) -> ( (/) .o B ) = (/) )
14 11 13 sseq12d 
 |-  ( ( A e. On /\ B e. On ) -> ( ( (/) .o A ) C_ ( (/) .o B ) <-> (/) C_ (/) ) )
15 9 14 mpbiri 
 |-  ( ( A e. On /\ B e. On ) -> ( (/) .o A ) C_ ( (/) .o B ) )
16 oveq1 
 |-  ( C = (/) -> ( C .o A ) = ( (/) .o A ) )
17 oveq1 
 |-  ( C = (/) -> ( C .o B ) = ( (/) .o B ) )
18 16 17 sseq12d 
 |-  ( C = (/) -> ( ( C .o A ) C_ ( C .o B ) <-> ( (/) .o A ) C_ ( (/) .o B ) ) )
19 15 18 syl5ibrcom 
 |-  ( ( A e. On /\ B e. On ) -> ( C = (/) -> ( C .o A ) C_ ( C .o B ) ) )
20 19 3adant3 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( C = (/) -> ( C .o A ) C_ ( C .o B ) ) )
21 8 20 sylbird 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( -. (/) e. C -> ( C .o A ) C_ ( C .o B ) ) )
22 21 a1dd 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( -. (/) e. C -> ( A C_ B -> ( C .o A ) C_ ( C .o B ) ) ) )
23 3 22 pm2.61d 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( A C_ B -> ( C .o A ) C_ ( C .o B ) ) )