This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem oecan

Description: Left cancellation law for ordinal exponentiation. (Contributed by NM, 6-Jan-2005) (Revised by Mario Carneiro, 24-May-2015)

Ref Expression
Assertion oecan 
|- ( ( A e. ( On \ 2o ) /\ B e. On /\ C e. On ) -> ( ( A ^o B ) = ( A ^o C ) <-> B = C ) )

Proof

Step Hyp Ref Expression
1 oeordi 
 |-  ( ( C e. On /\ A e. ( On \ 2o ) ) -> ( B e. C -> ( A ^o B ) e. ( A ^o C ) ) )
2 1 ancoms 
 |-  ( ( A e. ( On \ 2o ) /\ C e. On ) -> ( B e. C -> ( A ^o B ) e. ( A ^o C ) ) )
3 2 3adant2 
 |-  ( ( A e. ( On \ 2o ) /\ B e. On /\ C e. On ) -> ( B e. C -> ( A ^o B ) e. ( A ^o C ) ) )
4 oeordi 
 |-  ( ( B e. On /\ A e. ( On \ 2o ) ) -> ( C e. B -> ( A ^o C ) e. ( A ^o B ) ) )
5 4 ancoms 
 |-  ( ( A e. ( On \ 2o ) /\ B e. On ) -> ( C e. B -> ( A ^o C ) e. ( A ^o B ) ) )
6 5 3adant3 
 |-  ( ( A e. ( On \ 2o ) /\ B e. On /\ C e. On ) -> ( C e. B -> ( A ^o C ) e. ( A ^o B ) ) )
7 3 6 orim12d 
 |-  ( ( A e. ( On \ 2o ) /\ 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 ) ) ) )
8 7 con3d 
 |-  ( ( A e. ( On \ 2o ) /\ B e. On /\ C e. On ) -> ( -. ( ( A ^o B ) e. ( A ^o C ) \/ ( A ^o C ) e. ( A ^o B ) ) -> -. ( B e. C \/ C e. B ) ) )
9 eldifi 
 |-  ( A e. ( On \ 2o ) -> A e. On )
10 9 3ad2ant1 
 |-  ( ( A e. ( On \ 2o ) /\ B e. On /\ C e. On ) -> A e. On )
11 simp2 
 |-  ( ( A e. ( On \ 2o ) /\ B e. On /\ C e. On ) -> B e. On )
12 oecl 
 |-  ( ( A e. On /\ B e. On ) -> ( A ^o B ) e. On )
13 10 11 12 syl2anc 
 |-  ( ( A e. ( On \ 2o ) /\ B e. On /\ C e. On ) -> ( A ^o B ) e. On )
14 simp3 
 |-  ( ( A e. ( On \ 2o ) /\ B e. On /\ C e. On ) -> C e. On )
15 oecl 
 |-  ( ( A e. On /\ C e. On ) -> ( A ^o C ) e. On )
16 10 14 15 syl2anc 
 |-  ( ( A e. ( On \ 2o ) /\ B e. On /\ C e. On ) -> ( A ^o C ) e. On )
17 eloni 
 |-  ( ( A ^o B ) e. On -> Ord ( A ^o B ) )
18 eloni 
 |-  ( ( A ^o C ) e. On -> Ord ( A ^o C ) )
19 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 ) ) ) )
20 17 18 19 syl2an 
 |-  ( ( ( A ^o B ) e. On /\ ( A ^o C ) e. On ) -> ( ( A ^o B ) = ( A ^o C ) <-> -. ( ( A ^o B ) e. ( A ^o C ) \/ ( A ^o C ) e. ( A ^o B ) ) ) )
21 13 16 20 syl2anc 
 |-  ( ( A e. ( On \ 2o ) /\ 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 ) ) ) )
22 eloni 
 |-  ( B e. On -> Ord B )
23 eloni 
 |-  ( C e. On -> Ord C )
24 ordtri3 
 |-  ( ( Ord B /\ Ord C ) -> ( B = C <-> -. ( B e. C \/ C e. B ) ) )
25 22 23 24 syl2an 
 |-  ( ( B e. On /\ C e. On ) -> ( B = C <-> -. ( B e. C \/ C e. B ) ) )
26 25 3adant1 
 |-  ( ( A e. ( On \ 2o ) /\ B e. On /\ C e. On ) -> ( B = C <-> -. ( B e. C \/ C e. B ) ) )
27 8 21 26 3imtr4d 
 |-  ( ( A e. ( On \ 2o ) /\ B e. On /\ C e. On ) -> ( ( A ^o B ) = ( A ^o C ) -> B = C ) )
28 oveq2 
 |-  ( B = C -> ( A ^o B ) = ( A ^o C ) )
29 27 28 impbid1 
 |-  ( ( A e. ( On \ 2o ) /\ B e. On /\ C e. On ) -> ( ( A ^o B ) = ( A ^o C ) <-> B = C ) )