Metamath Proof Explorer

Theorem oewordri

Description: Weak ordering property of ordinal exponentiation. Proposition 8.35 of TakeutiZaring p. 68. (Contributed by NM, 6-Jan-2005)

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

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( x = (/) -> ( A ^o x ) = ( A ^o (/) ) )
2 oveq2 
 |-  ( x = (/) -> ( B ^o x ) = ( B ^o (/) ) )
3 1 2 sseq12d 
 |-  ( x = (/) -> ( ( A ^o x ) C_ ( B ^o x ) <-> ( A ^o (/) ) C_ ( B ^o (/) ) ) )
4 oveq2 
 |-  ( x = y -> ( A ^o x ) = ( A ^o y ) )
5 oveq2 
 |-  ( x = y -> ( B ^o x ) = ( B ^o y ) )
6 4 5 sseq12d 
 |-  ( x = y -> ( ( A ^o x ) C_ ( B ^o x ) <-> ( A ^o y ) C_ ( B ^o y ) ) )
7 oveq2 
 |-  ( x = suc y -> ( A ^o x ) = ( A ^o suc y ) )
8 oveq2 
 |-  ( x = suc y -> ( B ^o x ) = ( B ^o suc y ) )
9 7 8 sseq12d 
 |-  ( x = suc y -> ( ( A ^o x ) C_ ( B ^o x ) <-> ( A ^o suc y ) C_ ( B ^o suc y ) ) )
10 oveq2 
 |-  ( x = C -> ( A ^o x ) = ( A ^o C ) )
11 oveq2 
 |-  ( x = C -> ( B ^o x ) = ( B ^o C ) )
12 10 11 sseq12d 
 |-  ( x = C -> ( ( A ^o x ) C_ ( B ^o x ) <-> ( A ^o C ) C_ ( B ^o C ) ) )
13 onelon 
 |-  ( ( B e. On /\ A e. B ) -> A e. On )
14 oe0 
 |-  ( A e. On -> ( A ^o (/) ) = 1o )
15 13 14 syl 
 |-  ( ( B e. On /\ A e. B ) -> ( A ^o (/) ) = 1o )
16 oe0 
 |-  ( B e. On -> ( B ^o (/) ) = 1o )
17 16 adantr 
 |-  ( ( B e. On /\ A e. B ) -> ( B ^o (/) ) = 1o )
18 15 17 eqtr4d 
 |-  ( ( B e. On /\ A e. B ) -> ( A ^o (/) ) = ( B ^o (/) ) )
19 eqimss 
 |-  ( ( A ^o (/) ) = ( B ^o (/) ) -> ( A ^o (/) ) C_ ( B ^o (/) ) )
20 18 19 syl 
 |-  ( ( B e. On /\ A e. B ) -> ( A ^o (/) ) C_ ( B ^o (/) ) )
21 simpl 
 |-  ( ( B e. On /\ A e. B ) -> B e. On )
22 onelss 
 |-  ( B e. On -> ( A e. B -> A C_ B ) )
23 22 imp 
 |-  ( ( B e. On /\ A e. B ) -> A C_ B )
24 13 21 23 jca31 
 |-  ( ( B e. On /\ A e. B ) -> ( ( A e. On /\ B e. On ) /\ A C_ B ) )
25 oecl 
 |-  ( ( A e. On /\ y e. On ) -> ( A ^o y ) e. On )
26 25 3adant2 
 |-  ( ( A e. On /\ B e. On /\ y e. On ) -> ( A ^o y ) e. On )
27 oecl 
 |-  ( ( B e. On /\ y e. On ) -> ( B ^o y ) e. On )
28 27 3adant1 
 |-  ( ( A e. On /\ B e. On /\ y e. On ) -> ( B ^o y ) e. On )
29 simp1 
 |-  ( ( A e. On /\ B e. On /\ y e. On ) -> A e. On )
30 omwordri 
 |-  ( ( ( A ^o y ) e. On /\ ( B ^o y ) e. On /\ A e. On ) -> ( ( A ^o y ) C_ ( B ^o y ) -> ( ( A ^o y ) .o A ) C_ ( ( B ^o y ) .o A ) ) )
31 26 28 29 30 syl3anc 
 |-  ( ( A e. On /\ B e. On /\ y e. On ) -> ( ( A ^o y ) C_ ( B ^o y ) -> ( ( A ^o y ) .o A ) C_ ( ( B ^o y ) .o A ) ) )
32 31 imp 
 |-  ( ( ( A e. On /\ B e. On /\ y e. On ) /\ ( A ^o y ) C_ ( B ^o y ) ) -> ( ( A ^o y ) .o A ) C_ ( ( B ^o y ) .o A ) )
33 32 adantrl 
 |-  ( ( ( A e. On /\ B e. On /\ y e. On ) /\ ( A C_ B /\ ( A ^o y ) C_ ( B ^o y ) ) ) -> ( ( A ^o y ) .o A ) C_ ( ( B ^o y ) .o A ) )
34 omwordi 
 |-  ( ( A e. On /\ B e. On /\ ( B ^o y ) e. On ) -> ( A C_ B -> ( ( B ^o y ) .o A ) C_ ( ( B ^o y ) .o B ) ) )
35 28 34 syld3an3 
 |-  ( ( A e. On /\ B e. On /\ y e. On ) -> ( A C_ B -> ( ( B ^o y ) .o A ) C_ ( ( B ^o y ) .o B ) ) )
36 35 imp 
 |-  ( ( ( A e. On /\ B e. On /\ y e. On ) /\ A C_ B ) -> ( ( B ^o y ) .o A ) C_ ( ( B ^o y ) .o B ) )
37 36 adantrr 
 |-  ( ( ( A e. On /\ B e. On /\ y e. On ) /\ ( A C_ B /\ ( A ^o y ) C_ ( B ^o y ) ) ) -> ( ( B ^o y ) .o A ) C_ ( ( B ^o y ) .o B ) )
38 33 37 sstrd 
 |-  ( ( ( A e. On /\ B e. On /\ y e. On ) /\ ( A C_ B /\ ( A ^o y ) C_ ( B ^o y ) ) ) -> ( ( A ^o y ) .o A ) C_ ( ( B ^o y ) .o B ) )
39 oesuc 
 |-  ( ( A e. On /\ y e. On ) -> ( A ^o suc y ) = ( ( A ^o y ) .o A ) )
40 39 3adant2 
 |-  ( ( A e. On /\ B e. On /\ y e. On ) -> ( A ^o suc y ) = ( ( A ^o y ) .o A ) )
41 40 adantr 
 |-  ( ( ( A e. On /\ B e. On /\ y e. On ) /\ ( A C_ B /\ ( A ^o y ) C_ ( B ^o y ) ) ) -> ( A ^o suc y ) = ( ( A ^o y ) .o A ) )
42 oesuc 
 |-  ( ( B e. On /\ y e. On ) -> ( B ^o suc y ) = ( ( B ^o y ) .o B ) )
43 42 3adant1 
 |-  ( ( A e. On /\ B e. On /\ y e. On ) -> ( B ^o suc y ) = ( ( B ^o y ) .o B ) )
44 43 adantr 
 |-  ( ( ( A e. On /\ B e. On /\ y e. On ) /\ ( A C_ B /\ ( A ^o y ) C_ ( B ^o y ) ) ) -> ( B ^o suc y ) = ( ( B ^o y ) .o B ) )
45 38 41 44 3sstr4d 
 |-  ( ( ( A e. On /\ B e. On /\ y e. On ) /\ ( A C_ B /\ ( A ^o y ) C_ ( B ^o y ) ) ) -> ( A ^o suc y ) C_ ( B ^o suc y ) )
46 45 exp520 
 |-  ( A e. On -> ( B e. On -> ( y e. On -> ( A C_ B -> ( ( A ^o y ) C_ ( B ^o y ) -> ( A ^o suc y ) C_ ( B ^o suc y ) ) ) ) ) )
47 46 com3r 
 |-  ( y e. On -> ( A e. On -> ( B e. On -> ( A C_ B -> ( ( A ^o y ) C_ ( B ^o y ) -> ( A ^o suc y ) C_ ( B ^o suc y ) ) ) ) ) )
48 47 imp4c 
 |-  ( y e. On -> ( ( ( A e. On /\ B e. On ) /\ A C_ B ) -> ( ( A ^o y ) C_ ( B ^o y ) -> ( A ^o suc y ) C_ ( B ^o suc y ) ) ) )
49 24 48 syl5 
 |-  ( y e. On -> ( ( B e. On /\ A e. B ) -> ( ( A ^o y ) C_ ( B ^o y ) -> ( A ^o suc y ) C_ ( B ^o suc y ) ) ) )
50 vex 
 |-  x e. _V
51 limelon 
 |-  ( ( x e. _V /\ Lim x ) -> x e. On )
52 50 51 mpan 
 |-  ( Lim x -> x e. On )
53 0ellim 
 |-  ( Lim x -> (/) e. x )
54 oe0m1 
 |-  ( x e. On -> ( (/) e. x <-> ( (/) ^o x ) = (/) ) )
55 54 biimpa 
 |-  ( ( x e. On /\ (/) e. x ) -> ( (/) ^o x ) = (/) )
56 52 53 55 syl2anc 
 |-  ( Lim x -> ( (/) ^o x ) = (/) )
57 0ss 
 |-  (/) C_ ( B ^o x )
58 56 57 eqsstrdi 
 |-  ( Lim x -> ( (/) ^o x ) C_ ( B ^o x ) )
59 oveq1 
 |-  ( A = (/) -> ( A ^o x ) = ( (/) ^o x ) )
60 59 sseq1d 
 |-  ( A = (/) -> ( ( A ^o x ) C_ ( B ^o x ) <-> ( (/) ^o x ) C_ ( B ^o x ) ) )
61 58 60 imbitrrid 
 |-  ( A = (/) -> ( Lim x -> ( A ^o x ) C_ ( B ^o x ) ) )
62 61 adantl 
 |-  ( ( ( B e. On /\ A e. B ) /\ A = (/) ) -> ( Lim x -> ( A ^o x ) C_ ( B ^o x ) ) )
63 62 a1dd 
 |-  ( ( ( B e. On /\ A e. B ) /\ A = (/) ) -> ( Lim x -> ( A. y e. x ( A ^o y ) C_ ( B ^o y ) -> ( A ^o x ) C_ ( B ^o x ) ) ) )
64 ss2iun 
 |-  ( A. y e. x ( A ^o y ) C_ ( B ^o y ) -> U_ y e. x ( A ^o y ) C_ U_ y e. x ( B ^o y ) )
65 oelim 
 |-  ( ( ( A e. On /\ ( x e. _V /\ Lim x ) ) /\ (/) e. A ) -> ( A ^o x ) = U_ y e. x ( A ^o y ) )
66 50 65 mpanlr1 
 |-  ( ( ( A e. On /\ Lim x ) /\ (/) e. A ) -> ( A ^o x ) = U_ y e. x ( A ^o y ) )
67 66 an32s 
 |-  ( ( ( A e. On /\ (/) e. A ) /\ Lim x ) -> ( A ^o x ) = U_ y e. x ( A ^o y ) )
68 67 adantllr 
 |-  ( ( ( ( A e. On /\ ( B e. On /\ A e. B ) ) /\ (/) e. A ) /\ Lim x ) -> ( A ^o x ) = U_ y e. x ( A ^o y ) )
69 21 anim1i 
 |-  ( ( ( B e. On /\ A e. B ) /\ Lim x ) -> ( B e. On /\ Lim x ) )
70 ne0i 
 |-  ( A e. B -> B =/= (/) )
71 on0eln0 
 |-  ( B e. On -> ( (/) e. B <-> B =/= (/) ) )
72 70 71 imbitrrid 
 |-  ( B e. On -> ( A e. B -> (/) e. B ) )
73 72 imp 
 |-  ( ( B e. On /\ A e. B ) -> (/) e. B )
74 73 adantr 
 |-  ( ( ( B e. On /\ A e. B ) /\ Lim x ) -> (/) e. B )
75 oelim 
 |-  ( ( ( B e. On /\ ( x e. _V /\ Lim x ) ) /\ (/) e. B ) -> ( B ^o x ) = U_ y e. x ( B ^o y ) )
76 50 75 mpanlr1 
 |-  ( ( ( B e. On /\ Lim x ) /\ (/) e. B ) -> ( B ^o x ) = U_ y e. x ( B ^o y ) )
77 69 74 76 syl2anc 
 |-  ( ( ( B e. On /\ A e. B ) /\ Lim x ) -> ( B ^o x ) = U_ y e. x ( B ^o y ) )
78 77 ad4ant24 
 |-  ( ( ( ( A e. On /\ ( B e. On /\ A e. B ) ) /\ (/) e. A ) /\ Lim x ) -> ( B ^o x ) = U_ y e. x ( B ^o y ) )
79 68 78 sseq12d 
 |-  ( ( ( ( A e. On /\ ( B e. On /\ A e. B ) ) /\ (/) e. A ) /\ Lim x ) -> ( ( A ^o x ) C_ ( B ^o x ) <-> U_ y e. x ( A ^o y ) C_ U_ y e. x ( B ^o y ) ) )
80 64 79 imbitrrid 
 |-  ( ( ( ( A e. On /\ ( B e. On /\ A e. B ) ) /\ (/) e. A ) /\ Lim x ) -> ( A. y e. x ( A ^o y ) C_ ( B ^o y ) -> ( A ^o x ) C_ ( B ^o x ) ) )
81 80 ex 
 |-  ( ( ( A e. On /\ ( B e. On /\ A e. B ) ) /\ (/) e. A ) -> ( Lim x -> ( A. y e. x ( A ^o y ) C_ ( B ^o y ) -> ( A ^o x ) C_ ( B ^o x ) ) ) )
82 63 81 oe0lem 
 |-  ( ( A e. On /\ ( B e. On /\ A e. B ) ) -> ( Lim x -> ( A. y e. x ( A ^o y ) C_ ( B ^o y ) -> ( A ^o x ) C_ ( B ^o x ) ) ) )
83 13 ancri 
 |-  ( ( B e. On /\ A e. B ) -> ( A e. On /\ ( B e. On /\ A e. B ) ) )
84 82 83 syl11 
 |-  ( Lim x -> ( ( B e. On /\ A e. B ) -> ( A. y e. x ( A ^o y ) C_ ( B ^o y ) -> ( A ^o x ) C_ ( B ^o x ) ) ) )
85 3 6 9 12 20 49 84 tfinds3 
 |-  ( C e. On -> ( ( B e. On /\ A e. B ) -> ( A ^o C ) C_ ( B ^o C ) ) )
86 85 expd 
 |-  ( C e. On -> ( B e. On -> ( A e. B -> ( A ^o C ) C_ ( B ^o C ) ) ) )
87 86 impcom 
 |-  ( ( B e. On /\ C e. On ) -> ( A e. B -> ( A ^o C ) C_ ( B ^o C ) ) )