Metamath Proof Explorer

Theorem oaord

Description: Ordering property of ordinal addition. Proposition 8.4 of TakeutiZaring p. 58 and its converse. (Contributed by NM, 5-Dec-2004)

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

Proof

Step Hyp Ref Expression
1 oaordi 
 |-  ( ( B e. On /\ C e. On ) -> ( A e. B -> ( C +o A ) e. ( C +o B ) ) )
2 1 3adant1 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( 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 ) -> ( A = B -> ( C +o A ) = ( C +o B ) ) )
5 oaordi 
 |-  ( ( A e. On /\ C e. On ) -> ( B e. A -> ( C +o B ) e. ( C +o A ) ) )
6 5 3adant2 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( B e. A -> ( C +o B ) e. ( C +o A ) ) )
7 4 6 orim12d 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( 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 ) -> ( -. ( ( C +o A ) = ( C +o B ) \/ ( C +o B ) e. ( C +o A ) ) -> -. ( A = B \/ B e. A ) ) )
9 df-3an 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) <-> ( ( A e. On /\ B e. On ) /\ C e. On ) )
10 ancom 
 |-  ( ( ( A e. On /\ B e. On ) /\ C e. On ) <-> ( C e. On /\ ( A e. On /\ B e. On ) ) )
11 anandi 
 |-  ( ( C e. On /\ ( A e. On /\ B e. On ) ) <-> ( ( C e. On /\ A e. On ) /\ ( C e. On /\ B e. On ) ) )
12 9 10 11 3bitri 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) <-> ( ( C e. On /\ A e. On ) /\ ( C e. On /\ B e. On ) ) )
13 oacl 
 |-  ( ( C e. On /\ A e. On ) -> ( C +o A ) e. On )
14 eloni 
 |-  ( ( C +o A ) e. On -> Ord ( C +o A ) )
15 13 14 syl 
 |-  ( ( C e. On /\ A e. On ) -> Ord ( C +o A ) )
16 oacl 
 |-  ( ( C e. On /\ B e. On ) -> ( C +o B ) e. On )
17 eloni 
 |-  ( ( C +o B ) e. On -> Ord ( C +o B ) )
18 16 17 syl 
 |-  ( ( C e. On /\ B e. On ) -> Ord ( C +o B ) )
19 15 18 anim12i 
 |-  ( ( ( C e. On /\ A e. On ) /\ ( C e. On /\ B e. On ) ) -> ( Ord ( C +o A ) /\ Ord ( C +o B ) ) )
20 12 19 sylbi 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( Ord ( C +o A ) /\ Ord ( C +o B ) ) )
21 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 ) ) ) )
22 20 21 syl 
 |-  ( ( 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 ) ) ) )
23 eloni 
 |-  ( A e. On -> Ord A )
24 eloni 
 |-  ( B e. On -> Ord B )
25 23 24 anim12i 
 |-  ( ( A e. On /\ B e. On ) -> ( Ord A /\ Ord B ) )
26 25 3adant3 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( Ord A /\ Ord B ) )
27 ordtri2 
 |-  ( ( Ord A /\ Ord B ) -> ( A e. B <-> -. ( A = B \/ B e. A ) ) )
28 26 27 syl 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( A e. B <-> -. ( A = B \/ B e. A ) ) )
29 8 22 28 3imtr4d 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( C +o A ) e. ( C +o B ) -> A e. B ) )
30 2 29 impbid 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( A e. B <-> ( C +o A ) e. ( C +o B ) ) )