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

Metamath Proof Explorer

Theorem oeord

Description: Ordering property of ordinal exponentiation. Corollary 8.34 of TakeutiZaring p. 68 and its converse. (Contributed by NM, 6-Jan-2005) (Revised by Mario Carneiro, 24-May-2015)

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

Proof

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