Metamath Proof Explorer

Theorem omord2

Description: Ordering property of ordinal multiplication. (Contributed by NM, 25-Dec-2004)

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

Proof

Step Hyp Ref Expression
1 omordi 
 |-  ( ( ( B e. On /\ C e. On ) /\ (/) e. C ) -> ( A e. B -> ( C .o A ) e. ( C .o B ) ) )
2 1 3adantl1 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ (/) e. C ) -> ( A e. B -> ( C .o A ) e. ( C .o B ) ) )
3 oveq2 
 |-  ( A = B -> ( C .o A ) = ( C .o B ) )
4 3 a1i 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ (/) e. C ) -> ( A = B -> ( C .o A ) = ( C .o B ) ) )
5 omordi 
 |-  ( ( ( A e. On /\ C e. On ) /\ (/) e. C ) -> ( B e. A -> ( C .o B ) e. ( C .o A ) ) )
6 5 3adantl2 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ (/) e. C ) -> ( B e. A -> ( C .o B ) e. ( C .o A ) ) )
7 4 6 orim12d 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ (/) e. C ) -> ( ( A = B \/ B e. A ) -> ( ( C .o A ) = ( C .o B ) \/ ( C .o B ) e. ( C .o A ) ) ) )
8 7 con3d 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ (/) e. C ) -> ( -. ( ( C .o A ) = ( C .o B ) \/ ( C .o B ) e. ( C .o A ) ) -> -. ( A = B \/ B e. A ) ) )
9 omcl 
 |-  ( ( C e. On /\ A e. On ) -> ( C .o A ) e. On )
10 omcl 
 |-  ( ( C e. On /\ B e. On ) -> ( C .o B ) e. On )
11 eloni 
 |-  ( ( C .o A ) e. On -> Ord ( C .o A ) )
12 eloni 
 |-  ( ( C .o B ) e. On -> Ord ( C .o B ) )
13 ordtri2 
 |-  ( ( Ord ( C .o A ) /\ Ord ( C .o B ) ) -> ( ( C .o A ) e. ( C .o B ) <-> -. ( ( C .o A ) = ( C .o B ) \/ ( C .o B ) e. ( C .o A ) ) ) )
14 11 12 13 syl2an 
 |-  ( ( ( C .o A ) e. On /\ ( C .o B ) e. On ) -> ( ( C .o A ) e. ( C .o B ) <-> -. ( ( C .o A ) = ( C .o B ) \/ ( C .o B ) e. ( C .o A ) ) ) )
15 9 10 14 syl2an 
 |-  ( ( ( C e. On /\ A e. On ) /\ ( C e. On /\ B e. On ) ) -> ( ( C .o A ) e. ( C .o B ) <-> -. ( ( C .o A ) = ( C .o B ) \/ ( C .o B ) e. ( C .o A ) ) ) )
16 15 anandis 
 |-  ( ( C e. On /\ ( A e. On /\ B e. On ) ) -> ( ( C .o A ) e. ( C .o B ) <-> -. ( ( C .o A ) = ( C .o B ) \/ ( C .o B ) e. ( C .o A ) ) ) )
17 16 ancoms 
 |-  ( ( ( A e. On /\ B e. On ) /\ C e. On ) -> ( ( C .o A ) e. ( C .o B ) <-> -. ( ( C .o A ) = ( C .o B ) \/ ( C .o B ) e. ( C .o A ) ) ) )
18 17 3impa 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( C .o A ) e. ( C .o B ) <-> -. ( ( C .o A ) = ( C .o B ) \/ ( C .o B ) e. ( C .o A ) ) ) )
19 18 adantr 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ (/) e. C ) -> ( ( C .o A ) e. ( C .o B ) <-> -. ( ( C .o A ) = ( C .o B ) \/ ( C .o B ) e. ( C .o A ) ) ) )
20 eloni 
 |-  ( A e. On -> Ord A )
21 eloni 
 |-  ( B e. On -> Ord B )
22 ordtri2 
 |-  ( ( Ord A /\ Ord B ) -> ( A e. B <-> -. ( A = B \/ B e. A ) ) )
23 20 21 22 syl2an 
 |-  ( ( A e. On /\ B e. On ) -> ( A e. B <-> -. ( A = B \/ B e. A ) ) )
24 23 3adant3 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( A e. B <-> -. ( A = B \/ B e. A ) ) )
25 24 adantr 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ (/) e. C ) -> ( A e. B <-> -. ( A = B \/ B e. A ) ) )
26 8 19 25 3imtr4d 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ (/) e. C ) -> ( ( C .o A ) e. ( C .o B ) -> A e. B ) )
27 2 26 impbid 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ (/) e. C ) -> ( A e. B <-> ( C .o A ) e. ( C .o B ) ) )