Metamath Proof Explorer

Theorem oeworde

Description: Ordinal exponentiation compared to its exponent. Proposition 8.37 of TakeutiZaring p. 68. (Contributed by NM, 7-Jan-2005) (Revised by Mario Carneiro, 24-May-2015)

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

Proof

Step Hyp Ref Expression
1 id 
 |-  ( x = (/) -> x = (/) )
2 oveq2 
 |-  ( x = (/) -> ( A ^o x ) = ( A ^o (/) ) )
3 1 2 sseq12d 
 |-  ( x = (/) -> ( x C_ ( A ^o x ) <-> (/) C_ ( A ^o (/) ) ) )
4 id 
 |-  ( x = y -> x = y )
5 oveq2 
 |-  ( x = y -> ( A ^o x ) = ( A ^o y ) )
6 4 5 sseq12d 
 |-  ( x = y -> ( x C_ ( A ^o x ) <-> y C_ ( A ^o y ) ) )
7 id 
 |-  ( x = suc y -> x = suc y )
8 oveq2 
 |-  ( x = suc y -> ( A ^o x ) = ( A ^o suc y ) )
9 7 8 sseq12d 
 |-  ( x = suc y -> ( x C_ ( A ^o x ) <-> suc y C_ ( A ^o suc y ) ) )
10 id 
 |-  ( x = B -> x = B )
11 oveq2 
 |-  ( x = B -> ( A ^o x ) = ( A ^o B ) )
12 10 11 sseq12d 
 |-  ( x = B -> ( x C_ ( A ^o x ) <-> B C_ ( A ^o B ) ) )
13 0ss 
 |-  (/) C_ ( A ^o (/) )
14 13 a1i 
 |-  ( A e. ( On \ 2o ) -> (/) C_ ( A ^o (/) ) )
15 eloni 
 |-  ( y e. On -> Ord y )
16 eldifi 
 |-  ( A e. ( On \ 2o ) -> A e. On )
17 oecl 
 |-  ( ( A e. On /\ y e. On ) -> ( A ^o y ) e. On )
18 16 17 sylan 
 |-  ( ( A e. ( On \ 2o ) /\ y e. On ) -> ( A ^o y ) e. On )
19 eloni 
 |-  ( ( A ^o y ) e. On -> Ord ( A ^o y ) )
20 18 19 syl 
 |-  ( ( A e. ( On \ 2o ) /\ y e. On ) -> Ord ( A ^o y ) )
21 ordsucsssuc 
 |-  ( ( Ord y /\ Ord ( A ^o y ) ) -> ( y C_ ( A ^o y ) <-> suc y C_ suc ( A ^o y ) ) )
22 15 20 21 syl2an2 
 |-  ( ( A e. ( On \ 2o ) /\ y e. On ) -> ( y C_ ( A ^o y ) <-> suc y C_ suc ( A ^o y ) ) )
23 suceloni 
 |-  ( y e. On -> suc y e. On )
24 oecl 
 |-  ( ( A e. On /\ suc y e. On ) -> ( A ^o suc y ) e. On )
25 16 23 24 syl2an 
 |-  ( ( A e. ( On \ 2o ) /\ y e. On ) -> ( A ^o suc y ) e. On )
26 eloni 
 |-  ( ( A ^o suc y ) e. On -> Ord ( A ^o suc y ) )
27 25 26 syl 
 |-  ( ( A e. ( On \ 2o ) /\ y e. On ) -> Ord ( A ^o suc y ) )
28 id 
 |-  ( A e. ( On \ 2o ) -> A e. ( On \ 2o ) )
29 vex 
 |-  y e. _V
30 29 sucid 
 |-  y e. suc y
31 oeordi 
 |-  ( ( suc y e. On /\ A e. ( On \ 2o ) ) -> ( y e. suc y -> ( A ^o y ) e. ( A ^o suc y ) ) )
32 30 31 mpi 
 |-  ( ( suc y e. On /\ A e. ( On \ 2o ) ) -> ( A ^o y ) e. ( A ^o suc y ) )
33 23 28 32 syl2anr 
 |-  ( ( A e. ( On \ 2o ) /\ y e. On ) -> ( A ^o y ) e. ( A ^o suc y ) )
34 ordsucss 
 |-  ( Ord ( A ^o suc y ) -> ( ( A ^o y ) e. ( A ^o suc y ) -> suc ( A ^o y ) C_ ( A ^o suc y ) ) )
35 27 33 34 sylc 
 |-  ( ( A e. ( On \ 2o ) /\ y e. On ) -> suc ( A ^o y ) C_ ( A ^o suc y ) )
36 sstr2 
 |-  ( suc y C_ suc ( A ^o y ) -> ( suc ( A ^o y ) C_ ( A ^o suc y ) -> suc y C_ ( A ^o suc y ) ) )
37 35 36 syl5com 
 |-  ( ( A e. ( On \ 2o ) /\ y e. On ) -> ( suc y C_ suc ( A ^o y ) -> suc y C_ ( A ^o suc y ) ) )
38 22 37 sylbid 
 |-  ( ( A e. ( On \ 2o ) /\ y e. On ) -> ( y C_ ( A ^o y ) -> suc y C_ ( A ^o suc y ) ) )
39 38 expcom 
 |-  ( y e. On -> ( A e. ( On \ 2o ) -> ( y C_ ( A ^o y ) -> suc y C_ ( A ^o suc y ) ) ) )
40 dif20el 
 |-  ( A e. ( On \ 2o ) -> (/) e. A )
41 16 40 jca 
 |-  ( A e. ( On \ 2o ) -> ( A e. On /\ (/) e. A ) )
42 ss2iun 
 |-  ( A. y e. x y C_ ( A ^o y ) -> U_ y e. x y C_ U_ y e. x ( A ^o y ) )
43 limuni 
 |-  ( Lim x -> x = U. x )
44 uniiun 
 |-  U. x = U_ y e. x y
45 43 44 eqtrdi 
 |-  ( Lim x -> x = U_ y e. x y )
46 45 adantr 
 |-  ( ( Lim x /\ ( A e. On /\ (/) e. A ) ) -> x = U_ y e. x y )
47 vex 
 |-  x e. _V
48 oelim 
 |-  ( ( ( A e. On /\ ( x e. _V /\ Lim x ) ) /\ (/) e. A ) -> ( A ^o x ) = U_ y e. x ( A ^o y ) )
49 47 48 mpanlr1 
 |-  ( ( ( A e. On /\ Lim x ) /\ (/) e. A ) -> ( A ^o x ) = U_ y e. x ( A ^o y ) )
50 49 anasss 
 |-  ( ( A e. On /\ ( Lim x /\ (/) e. A ) ) -> ( A ^o x ) = U_ y e. x ( A ^o y ) )
51 50 an12s 
 |-  ( ( Lim x /\ ( A e. On /\ (/) e. A ) ) -> ( A ^o x ) = U_ y e. x ( A ^o y ) )
52 46 51 sseq12d 
 |-  ( ( Lim x /\ ( A e. On /\ (/) e. A ) ) -> ( x C_ ( A ^o x ) <-> U_ y e. x y C_ U_ y e. x ( A ^o y ) ) )
53 42 52 syl5ibr 
 |-  ( ( Lim x /\ ( A e. On /\ (/) e. A ) ) -> ( A. y e. x y C_ ( A ^o y ) -> x C_ ( A ^o x ) ) )
54 53 ex 
 |-  ( Lim x -> ( ( A e. On /\ (/) e. A ) -> ( A. y e. x y C_ ( A ^o y ) -> x C_ ( A ^o x ) ) ) )
55 41 54 syl5 
 |-  ( Lim x -> ( A e. ( On \ 2o ) -> ( A. y e. x y C_ ( A ^o y ) -> x C_ ( A ^o x ) ) ) )
56 3 6 9 12 14 39 55 tfinds3 
 |-  ( B e. On -> ( A e. ( On \ 2o ) -> B C_ ( A ^o B ) ) )
57 56 impcom 
 |-  ( ( A e. ( On \ 2o ) /\ B e. On ) -> B C_ ( A ^o B ) )