Metamath Proof Explorer


Theorem oeordi

Description: Ordering law for ordinal exponentiation. Proposition 8.33 of TakeutiZaring p. 67. (Contributed by NM, 5-Jan-2005) (Revised by Mario Carneiro, 24-May-2015)

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

Proof

Step Hyp Ref Expression
1 oveq2
 |-  ( x = suc A -> ( C ^o x ) = ( C ^o suc A ) )
2 1 eleq2d
 |-  ( x = suc A -> ( ( C ^o A ) e. ( C ^o x ) <-> ( C ^o A ) e. ( C ^o suc A ) ) )
3 2 imbi2d
 |-  ( x = suc A -> ( ( C e. ( On \ 2o ) -> ( C ^o A ) e. ( C ^o x ) ) <-> ( C e. ( On \ 2o ) -> ( C ^o A ) e. ( C ^o suc A ) ) ) )
4 oveq2
 |-  ( x = y -> ( C ^o x ) = ( C ^o y ) )
5 4 eleq2d
 |-  ( x = y -> ( ( C ^o A ) e. ( C ^o x ) <-> ( C ^o A ) e. ( C ^o y ) ) )
6 5 imbi2d
 |-  ( x = y -> ( ( C e. ( On \ 2o ) -> ( C ^o A ) e. ( C ^o x ) ) <-> ( C e. ( On \ 2o ) -> ( C ^o A ) e. ( C ^o y ) ) ) )
7 oveq2
 |-  ( x = suc y -> ( C ^o x ) = ( C ^o suc y ) )
8 7 eleq2d
 |-  ( x = suc y -> ( ( C ^o A ) e. ( C ^o x ) <-> ( C ^o A ) e. ( C ^o suc y ) ) )
9 8 imbi2d
 |-  ( x = suc y -> ( ( C e. ( On \ 2o ) -> ( C ^o A ) e. ( C ^o x ) ) <-> ( C e. ( On \ 2o ) -> ( C ^o A ) e. ( C ^o suc y ) ) ) )
10 oveq2
 |-  ( x = B -> ( C ^o x ) = ( C ^o B ) )
11 10 eleq2d
 |-  ( x = B -> ( ( C ^o A ) e. ( C ^o x ) <-> ( C ^o A ) e. ( C ^o B ) ) )
12 11 imbi2d
 |-  ( x = B -> ( ( C e. ( On \ 2o ) -> ( C ^o A ) e. ( C ^o x ) ) <-> ( C e. ( On \ 2o ) -> ( C ^o A ) e. ( C ^o B ) ) ) )
13 eldifi
 |-  ( C e. ( On \ 2o ) -> C e. On )
14 oecl
 |-  ( ( C e. On /\ A e. On ) -> ( C ^o A ) e. On )
15 13 14 sylan
 |-  ( ( C e. ( On \ 2o ) /\ A e. On ) -> ( C ^o A ) e. On )
16 om1
 |-  ( ( C ^o A ) e. On -> ( ( C ^o A ) .o 1o ) = ( C ^o A ) )
17 15 16 syl
 |-  ( ( C e. ( On \ 2o ) /\ A e. On ) -> ( ( C ^o A ) .o 1o ) = ( C ^o A ) )
18 ondif2
 |-  ( C e. ( On \ 2o ) <-> ( C e. On /\ 1o e. C ) )
19 18 simprbi
 |-  ( C e. ( On \ 2o ) -> 1o e. C )
20 19 adantr
 |-  ( ( C e. ( On \ 2o ) /\ A e. On ) -> 1o e. C )
21 13 adantr
 |-  ( ( C e. ( On \ 2o ) /\ A e. On ) -> C e. On )
22 simpr
 |-  ( ( C e. ( On \ 2o ) /\ A e. On ) -> A e. On )
23 dif20el
 |-  ( C e. ( On \ 2o ) -> (/) e. C )
24 23 adantr
 |-  ( ( C e. ( On \ 2o ) /\ A e. On ) -> (/) e. C )
25 oen0
 |-  ( ( ( C e. On /\ A e. On ) /\ (/) e. C ) -> (/) e. ( C ^o A ) )
26 21 22 24 25 syl21anc
 |-  ( ( C e. ( On \ 2o ) /\ A e. On ) -> (/) e. ( C ^o A ) )
27 omordi
 |-  ( ( ( C e. On /\ ( C ^o A ) e. On ) /\ (/) e. ( C ^o A ) ) -> ( 1o e. C -> ( ( C ^o A ) .o 1o ) e. ( ( C ^o A ) .o C ) ) )
28 21 15 26 27 syl21anc
 |-  ( ( C e. ( On \ 2o ) /\ A e. On ) -> ( 1o e. C -> ( ( C ^o A ) .o 1o ) e. ( ( C ^o A ) .o C ) ) )
29 20 28 mpd
 |-  ( ( C e. ( On \ 2o ) /\ A e. On ) -> ( ( C ^o A ) .o 1o ) e. ( ( C ^o A ) .o C ) )
30 17 29 eqeltrrd
 |-  ( ( C e. ( On \ 2o ) /\ A e. On ) -> ( C ^o A ) e. ( ( C ^o A ) .o C ) )
31 oesuc
 |-  ( ( C e. On /\ A e. On ) -> ( C ^o suc A ) = ( ( C ^o A ) .o C ) )
32 13 31 sylan
 |-  ( ( C e. ( On \ 2o ) /\ A e. On ) -> ( C ^o suc A ) = ( ( C ^o A ) .o C ) )
33 30 32 eleqtrrd
 |-  ( ( C e. ( On \ 2o ) /\ A e. On ) -> ( C ^o A ) e. ( C ^o suc A ) )
34 33 expcom
 |-  ( A e. On -> ( C e. ( On \ 2o ) -> ( C ^o A ) e. ( C ^o suc A ) ) )
35 oecl
 |-  ( ( C e. On /\ y e. On ) -> ( C ^o y ) e. On )
36 13 35 sylan
 |-  ( ( C e. ( On \ 2o ) /\ y e. On ) -> ( C ^o y ) e. On )
37 om1
 |-  ( ( C ^o y ) e. On -> ( ( C ^o y ) .o 1o ) = ( C ^o y ) )
38 36 37 syl
 |-  ( ( C e. ( On \ 2o ) /\ y e. On ) -> ( ( C ^o y ) .o 1o ) = ( C ^o y ) )
39 19 adantr
 |-  ( ( C e. ( On \ 2o ) /\ y e. On ) -> 1o e. C )
40 13 adantr
 |-  ( ( C e. ( On \ 2o ) /\ y e. On ) -> C e. On )
41 simpr
 |-  ( ( C e. ( On \ 2o ) /\ y e. On ) -> y e. On )
42 23 adantr
 |-  ( ( C e. ( On \ 2o ) /\ y e. On ) -> (/) e. C )
43 oen0
 |-  ( ( ( C e. On /\ y e. On ) /\ (/) e. C ) -> (/) e. ( C ^o y ) )
44 40 41 42 43 syl21anc
 |-  ( ( C e. ( On \ 2o ) /\ y e. On ) -> (/) e. ( C ^o y ) )
45 omordi
 |-  ( ( ( C e. On /\ ( C ^o y ) e. On ) /\ (/) e. ( C ^o y ) ) -> ( 1o e. C -> ( ( C ^o y ) .o 1o ) e. ( ( C ^o y ) .o C ) ) )
46 40 36 44 45 syl21anc
 |-  ( ( C e. ( On \ 2o ) /\ y e. On ) -> ( 1o e. C -> ( ( C ^o y ) .o 1o ) e. ( ( C ^o y ) .o C ) ) )
47 39 46 mpd
 |-  ( ( C e. ( On \ 2o ) /\ y e. On ) -> ( ( C ^o y ) .o 1o ) e. ( ( C ^o y ) .o C ) )
48 38 47 eqeltrrd
 |-  ( ( C e. ( On \ 2o ) /\ y e. On ) -> ( C ^o y ) e. ( ( C ^o y ) .o C ) )
49 oesuc
 |-  ( ( C e. On /\ y e. On ) -> ( C ^o suc y ) = ( ( C ^o y ) .o C ) )
50 13 49 sylan
 |-  ( ( C e. ( On \ 2o ) /\ y e. On ) -> ( C ^o suc y ) = ( ( C ^o y ) .o C ) )
51 48 50 eleqtrrd
 |-  ( ( C e. ( On \ 2o ) /\ y e. On ) -> ( C ^o y ) e. ( C ^o suc y ) )
52 suceloni
 |-  ( y e. On -> suc y e. On )
53 oecl
 |-  ( ( C e. On /\ suc y e. On ) -> ( C ^o suc y ) e. On )
54 13 52 53 syl2an
 |-  ( ( C e. ( On \ 2o ) /\ y e. On ) -> ( C ^o suc y ) e. On )
55 ontr1
 |-  ( ( C ^o suc y ) e. On -> ( ( ( C ^o A ) e. ( C ^o y ) /\ ( C ^o y ) e. ( C ^o suc y ) ) -> ( C ^o A ) e. ( C ^o suc y ) ) )
56 54 55 syl
 |-  ( ( C e. ( On \ 2o ) /\ y e. On ) -> ( ( ( C ^o A ) e. ( C ^o y ) /\ ( C ^o y ) e. ( C ^o suc y ) ) -> ( C ^o A ) e. ( C ^o suc y ) ) )
57 51 56 mpan2d
 |-  ( ( C e. ( On \ 2o ) /\ y e. On ) -> ( ( C ^o A ) e. ( C ^o y ) -> ( C ^o A ) e. ( C ^o suc y ) ) )
58 57 expcom
 |-  ( y e. On -> ( C e. ( On \ 2o ) -> ( ( C ^o A ) e. ( C ^o y ) -> ( C ^o A ) e. ( C ^o suc y ) ) ) )
59 58 adantr
 |-  ( ( y e. On /\ A e. y ) -> ( C e. ( On \ 2o ) -> ( ( C ^o A ) e. ( C ^o y ) -> ( C ^o A ) e. ( C ^o suc y ) ) ) )
60 59 a2d
 |-  ( ( y e. On /\ A e. y ) -> ( ( C e. ( On \ 2o ) -> ( C ^o A ) e. ( C ^o y ) ) -> ( C e. ( On \ 2o ) -> ( C ^o A ) e. ( C ^o suc y ) ) ) )
61 bi2.04
 |-  ( ( A e. y -> ( C e. ( On \ 2o ) -> ( C ^o A ) e. ( C ^o y ) ) ) <-> ( C e. ( On \ 2o ) -> ( A e. y -> ( C ^o A ) e. ( C ^o y ) ) ) )
62 61 ralbii
 |-  ( A. y e. x ( A e. y -> ( C e. ( On \ 2o ) -> ( C ^o A ) e. ( C ^o y ) ) ) <-> A. y e. x ( C e. ( On \ 2o ) -> ( A e. y -> ( C ^o A ) e. ( C ^o y ) ) ) )
63 r19.21v
 |-  ( A. y e. x ( C e. ( On \ 2o ) -> ( A e. y -> ( C ^o A ) e. ( C ^o y ) ) ) <-> ( C e. ( On \ 2o ) -> A. y e. x ( A e. y -> ( C ^o A ) e. ( C ^o y ) ) ) )
64 62 63 bitri
 |-  ( A. y e. x ( A e. y -> ( C e. ( On \ 2o ) -> ( C ^o A ) e. ( C ^o y ) ) ) <-> ( C e. ( On \ 2o ) -> A. y e. x ( A e. y -> ( C ^o A ) e. ( C ^o y ) ) ) )
65 limsuc
 |-  ( Lim x -> ( A e. x <-> suc A e. x ) )
66 65 biimpa
 |-  ( ( Lim x /\ A e. x ) -> suc A e. x )
67 elex
 |-  ( suc A e. x -> suc A e. _V )
68 sucexb
 |-  ( A e. _V <-> suc A e. _V )
69 sucidg
 |-  ( A e. _V -> A e. suc A )
70 68 69 sylbir
 |-  ( suc A e. _V -> A e. suc A )
71 67 70 syl
 |-  ( suc A e. x -> A e. suc A )
72 eleq2
 |-  ( y = suc A -> ( A e. y <-> A e. suc A ) )
73 oveq2
 |-  ( y = suc A -> ( C ^o y ) = ( C ^o suc A ) )
74 73 eleq2d
 |-  ( y = suc A -> ( ( C ^o A ) e. ( C ^o y ) <-> ( C ^o A ) e. ( C ^o suc A ) ) )
75 72 74 imbi12d
 |-  ( y = suc A -> ( ( A e. y -> ( C ^o A ) e. ( C ^o y ) ) <-> ( A e. suc A -> ( C ^o A ) e. ( C ^o suc A ) ) ) )
76 75 rspcv
 |-  ( suc A e. x -> ( A. y e. x ( A e. y -> ( C ^o A ) e. ( C ^o y ) ) -> ( A e. suc A -> ( C ^o A ) e. ( C ^o suc A ) ) ) )
77 71 76 mpid
 |-  ( suc A e. x -> ( A. y e. x ( A e. y -> ( C ^o A ) e. ( C ^o y ) ) -> ( C ^o A ) e. ( C ^o suc A ) ) )
78 77 anc2li
 |-  ( suc A e. x -> ( A. y e. x ( A e. y -> ( C ^o A ) e. ( C ^o y ) ) -> ( suc A e. x /\ ( C ^o A ) e. ( C ^o suc A ) ) ) )
79 73 eliuni
 |-  ( ( suc A e. x /\ ( C ^o A ) e. ( C ^o suc A ) ) -> ( C ^o A ) e. U_ y e. x ( C ^o y ) )
80 78 79 syl6
 |-  ( suc A e. x -> ( A. y e. x ( A e. y -> ( C ^o A ) e. ( C ^o y ) ) -> ( C ^o A ) e. U_ y e. x ( C ^o y ) ) )
81 66 80 syl
 |-  ( ( Lim x /\ A e. x ) -> ( A. y e. x ( A e. y -> ( C ^o A ) e. ( C ^o y ) ) -> ( C ^o A ) e. U_ y e. x ( C ^o y ) ) )
82 81 adantr
 |-  ( ( ( Lim x /\ A e. x ) /\ C e. ( On \ 2o ) ) -> ( A. y e. x ( A e. y -> ( C ^o A ) e. ( C ^o y ) ) -> ( C ^o A ) e. U_ y e. x ( C ^o y ) ) )
83 13 adantl
 |-  ( ( Lim x /\ C e. ( On \ 2o ) ) -> C e. On )
84 simpl
 |-  ( ( Lim x /\ C e. ( On \ 2o ) ) -> Lim x )
85 23 adantl
 |-  ( ( Lim x /\ C e. ( On \ 2o ) ) -> (/) e. C )
86 vex
 |-  x e. _V
87 oelim
 |-  ( ( ( C e. On /\ ( x e. _V /\ Lim x ) ) /\ (/) e. C ) -> ( C ^o x ) = U_ y e. x ( C ^o y ) )
88 86 87 mpanlr1
 |-  ( ( ( C e. On /\ Lim x ) /\ (/) e. C ) -> ( C ^o x ) = U_ y e. x ( C ^o y ) )
89 83 84 85 88 syl21anc
 |-  ( ( Lim x /\ C e. ( On \ 2o ) ) -> ( C ^o x ) = U_ y e. x ( C ^o y ) )
90 89 adantlr
 |-  ( ( ( Lim x /\ A e. x ) /\ C e. ( On \ 2o ) ) -> ( C ^o x ) = U_ y e. x ( C ^o y ) )
91 90 eleq2d
 |-  ( ( ( Lim x /\ A e. x ) /\ C e. ( On \ 2o ) ) -> ( ( C ^o A ) e. ( C ^o x ) <-> ( C ^o A ) e. U_ y e. x ( C ^o y ) ) )
92 82 91 sylibrd
 |-  ( ( ( Lim x /\ A e. x ) /\ C e. ( On \ 2o ) ) -> ( A. y e. x ( A e. y -> ( C ^o A ) e. ( C ^o y ) ) -> ( C ^o A ) e. ( C ^o x ) ) )
93 92 ex
 |-  ( ( Lim x /\ A e. x ) -> ( C e. ( On \ 2o ) -> ( A. y e. x ( A e. y -> ( C ^o A ) e. ( C ^o y ) ) -> ( C ^o A ) e. ( C ^o x ) ) ) )
94 93 a2d
 |-  ( ( Lim x /\ A e. x ) -> ( ( C e. ( On \ 2o ) -> A. y e. x ( A e. y -> ( C ^o A ) e. ( C ^o y ) ) ) -> ( C e. ( On \ 2o ) -> ( C ^o A ) e. ( C ^o x ) ) ) )
95 64 94 syl5bi
 |-  ( ( Lim x /\ A e. x ) -> ( A. y e. x ( A e. y -> ( C e. ( On \ 2o ) -> ( C ^o A ) e. ( C ^o y ) ) ) -> ( C e. ( On \ 2o ) -> ( C ^o A ) e. ( C ^o x ) ) ) )
96 3 6 9 12 34 60 95 tfindsg2
 |-  ( ( B e. On /\ A e. B ) -> ( C e. ( On \ 2o ) -> ( C ^o A ) e. ( C ^o B ) ) )
97 96 impancom
 |-  ( ( B e. On /\ C e. ( On \ 2o ) ) -> ( A e. B -> ( C ^o A ) e. ( C ^o B ) ) )