Metamath Proof Explorer

Theorem oacan

Description: Left cancellation law for ordinal addition. Corollary 8.5 of TakeutiZaring p. 58. (Contributed by NM, 5-Dec-2004)

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

Proof

Step Hyp Ref Expression
1 oaord 
 |-  ( ( B e. On /\ C e. On /\ A e. On ) -> ( B e. C <-> ( A +o B ) e. ( A +o C ) ) )
2 1 3comr 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( B e. C <-> ( A +o B ) e. ( A +o C ) ) )
3 oaord 
 |-  ( ( C e. On /\ B e. On /\ A e. On ) -> ( C e. B <-> ( A +o C ) e. ( A +o B ) ) )
4 3 3com13 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( C e. B <-> ( A +o C ) e. ( A +o B ) ) )
5 2 4 orbi12d 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( B e. C \/ C e. B ) <-> ( ( A +o B ) e. ( A +o C ) \/ ( A +o C ) e. ( A +o B ) ) ) )
6 5 notbid 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( -. ( B e. C \/ C e. B ) <-> -. ( ( A +o B ) e. ( A +o C ) \/ ( A +o C ) e. ( A +o B ) ) ) )
7 eloni 
 |-  ( B e. On -> Ord B )
8 eloni 
 |-  ( C e. On -> Ord C )
9 ordtri3 
 |-  ( ( Ord B /\ Ord C ) -> ( B = C <-> -. ( B e. C \/ C e. B ) ) )
10 7 8 9 syl2an 
 |-  ( ( B e. On /\ C e. On ) -> ( B = C <-> -. ( B e. C \/ C e. B ) ) )
11 10 3adant1 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( B = C <-> -. ( B e. C \/ C e. B ) ) )
12 oacl 
 |-  ( ( A e. On /\ B e. On ) -> ( A +o B ) e. On )
13 eloni 
 |-  ( ( A +o B ) e. On -> Ord ( A +o B ) )
14 12 13 syl 
 |-  ( ( A e. On /\ B e. On ) -> Ord ( A +o B ) )
15 oacl 
 |-  ( ( A e. On /\ C e. On ) -> ( A +o C ) e. On )
16 eloni 
 |-  ( ( A +o C ) e. On -> Ord ( A +o C ) )
17 15 16 syl 
 |-  ( ( A e. On /\ C e. On ) -> Ord ( A +o C ) )
18 ordtri3 
 |-  ( ( Ord ( A +o B ) /\ Ord ( A +o C ) ) -> ( ( A +o B ) = ( A +o C ) <-> -. ( ( A +o B ) e. ( A +o C ) \/ ( A +o C ) e. ( A +o B ) ) ) )
19 14 17 18 syl2an 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( A e. On /\ C e. On ) ) -> ( ( A +o B ) = ( A +o C ) <-> -. ( ( A +o B ) e. ( A +o C ) \/ ( A +o C ) e. ( A +o B ) ) ) )
20 19 3impdi 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( A +o B ) = ( A +o C ) <-> -. ( ( A +o B ) e. ( A +o C ) \/ ( A +o C ) e. ( A +o B ) ) ) )
21 6 11 20 3bitr4rd 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( A +o B ) = ( A +o C ) <-> B = C ) )