Metamath Proof Explorer

Theorem omord

Description: Ordering property of ordinal multiplication. Proposition 8.19 of TakeutiZaring p. 63. (Contributed by NM, 14-Dec-2004)

Ref Expression
Assertion omord 
|- ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( A e. B /\ (/) e. C ) <-> ( C .o A ) e. ( 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 1 ex 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( (/) e. C -> ( A e. B <-> ( C .o A ) e. ( C .o B ) ) ) )
3 2 pm5.32rd 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( A e. B /\ (/) e. C ) <-> ( ( C .o A ) e. ( C .o B ) /\ (/) e. C ) ) )
4 simpl 
 |-  ( ( ( C .o A ) e. ( C .o B ) /\ (/) e. C ) -> ( C .o A ) e. ( C .o B ) )
5 ne0i 
 |-  ( ( C .o A ) e. ( C .o B ) -> ( C .o B ) =/= (/) )
6 om0r 
 |-  ( B e. On -> ( (/) .o B ) = (/) )
7 oveq1 
 |-  ( C = (/) -> ( C .o B ) = ( (/) .o B ) )
8 7 eqeq1d 
 |-  ( C = (/) -> ( ( C .o B ) = (/) <-> ( (/) .o B ) = (/) ) )
9 6 8 syl5ibrcom 
 |-  ( B e. On -> ( C = (/) -> ( C .o B ) = (/) ) )
10 9 necon3d 
 |-  ( B e. On -> ( ( C .o B ) =/= (/) -> C =/= (/) ) )
11 5 10 syl5 
 |-  ( B e. On -> ( ( C .o A ) e. ( C .o B ) -> C =/= (/) ) )
12 11 adantr 
 |-  ( ( B e. On /\ C e. On ) -> ( ( C .o A ) e. ( C .o B ) -> C =/= (/) ) )
13 on0eln0 
 |-  ( C e. On -> ( (/) e. C <-> C =/= (/) ) )
14 13 adantl 
 |-  ( ( B e. On /\ C e. On ) -> ( (/) e. C <-> C =/= (/) ) )
15 12 14 sylibrd 
 |-  ( ( B e. On /\ C e. On ) -> ( ( C .o A ) e. ( C .o B ) -> (/) e. C ) )
16 15 3adant1 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( C .o A ) e. ( C .o B ) -> (/) e. C ) )
17 16 ancld 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( C .o A ) e. ( C .o B ) -> ( ( C .o A ) e. ( C .o B ) /\ (/) e. C ) ) )
18 4 17 impbid2 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( ( C .o A ) e. ( C .o B ) /\ (/) e. C ) <-> ( C .o A ) e. ( C .o B ) ) )
19 3 18 bitrd 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( A e. B /\ (/) e. C ) <-> ( C .o A ) e. ( C .o B ) ) )