Metamath Proof Explorer

Theorem oaword

Description: Weak ordering property of ordinal addition. (Contributed by NM, 6-Dec-2004) (Proof shortened by Andrew Salmon, 22-Oct-2011)

Ref Expression
Assertion oaword 
|- ( ( 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 oaord 
 |-  ( ( B e. On /\ A e. On /\ C e. On ) -> ( B e. A <-> ( C +o B ) e. ( C +o A ) ) )
2 1 3com12 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( B e. A <-> ( C +o B ) e. ( C +o A ) ) )
3 2 notbid 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( -. B e. A <-> -. ( C +o B ) e. ( C +o A ) ) )
4 ontri1 
 |-  ( ( A e. On /\ B e. On ) -> ( A C_ B <-> -. B e. A ) )
5 4 3adant3 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( A C_ B <-> -. B e. A ) )
6 oacl 
 |-  ( ( C e. On /\ A e. On ) -> ( C +o A ) e. On )
7 6 ancoms 
 |-  ( ( A e. On /\ C e. On ) -> ( C +o A ) e. On )
8 7 3adant2 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( C +o A ) e. On )
9 oacl 
 |-  ( ( C e. On /\ B e. On ) -> ( C +o B ) e. On )
10 9 ancoms 
 |-  ( ( B e. On /\ C e. On ) -> ( C +o B ) e. On )
11 10 3adant1 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( C +o B ) e. On )
12 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 ) ) )
13 8 11 12 syl2anc 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( C +o A ) C_ ( C +o B ) <-> -. ( C +o B ) e. ( C +o A ) ) )
14 3 5 13 3bitr4d 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( A C_ B <-> ( C +o A ) C_ ( C +o B ) ) )