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 ) ) )