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 ) ) )