Metamath Proof Explorer

Theorem oecl

Description: Closure law for ordinal exponentiation. (Contributed by NM, 1-Jan-2005) (Proof shortened by Andrew Salmon, 22-Oct-2011)

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

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( B = (/) -> ( (/) ^o B ) = ( (/) ^o (/) ) )
2 oe0m0 
 |-  ( (/) ^o (/) ) = 1o
3 1on 
 |-  1o e. On
4 2 3 eqeltri 
 |-  ( (/) ^o (/) ) e. On
5 1 4 eqeltrdi 
 |-  ( B = (/) -> ( (/) ^o B ) e. On )
6 5 adantl 
 |-  ( ( B e. On /\ B = (/) ) -> ( (/) ^o B ) e. On )
7 oe0m1 
 |-  ( B e. On -> ( (/) e. B <-> ( (/) ^o B ) = (/) ) )
8 7 biimpa 
 |-  ( ( B e. On /\ (/) e. B ) -> ( (/) ^o B ) = (/) )
9 0elon 
 |-  (/) e. On
10 8 9 eqeltrdi 
 |-  ( ( B e. On /\ (/) e. B ) -> ( (/) ^o B ) e. On )
11 10 adantll 
 |-  ( ( ( B e. On /\ B e. On ) /\ (/) e. B ) -> ( (/) ^o B ) e. On )
12 6 11 oe0lem 
 |-  ( ( B e. On /\ B e. On ) -> ( (/) ^o B ) e. On )
13 12 anidms 
 |-  ( B e. On -> ( (/) ^o B ) e. On )
14 oveq1 
 |-  ( A = (/) -> ( A ^o B ) = ( (/) ^o B ) )
15 14 eleq1d 
 |-  ( A = (/) -> ( ( A ^o B ) e. On <-> ( (/) ^o B ) e. On ) )
16 13 15 syl5ibr 
 |-  ( A = (/) -> ( B e. On -> ( A ^o B ) e. On ) )
17 16 impcom 
 |-  ( ( B e. On /\ A = (/) ) -> ( A ^o B ) e. On )
18 oveq2 
 |-  ( x = (/) -> ( A ^o x ) = ( A ^o (/) ) )
19 18 eleq1d 
 |-  ( x = (/) -> ( ( A ^o x ) e. On <-> ( A ^o (/) ) e. On ) )
20 oveq2 
 |-  ( x = y -> ( A ^o x ) = ( A ^o y ) )
21 20 eleq1d 
 |-  ( x = y -> ( ( A ^o x ) e. On <-> ( A ^o y ) e. On ) )
22 oveq2 
 |-  ( x = suc y -> ( A ^o x ) = ( A ^o suc y ) )
23 22 eleq1d 
 |-  ( x = suc y -> ( ( A ^o x ) e. On <-> ( A ^o suc y ) e. On ) )
24 oveq2 
 |-  ( x = B -> ( A ^o x ) = ( A ^o B ) )
25 24 eleq1d 
 |-  ( x = B -> ( ( A ^o x ) e. On <-> ( A ^o B ) e. On ) )
26 oe0 
 |-  ( A e. On -> ( A ^o (/) ) = 1o )
27 26 3 eqeltrdi 
 |-  ( A e. On -> ( A ^o (/) ) e. On )
28 27 adantr 
 |-  ( ( A e. On /\ (/) e. A ) -> ( A ^o (/) ) e. On )
29 omcl 
 |-  ( ( ( A ^o y ) e. On /\ A e. On ) -> ( ( A ^o y ) .o A ) e. On )
30 29 expcom 
 |-  ( A e. On -> ( ( A ^o y ) e. On -> ( ( A ^o y ) .o A ) e. On ) )
31 30 adantr 
 |-  ( ( A e. On /\ y e. On ) -> ( ( A ^o y ) e. On -> ( ( A ^o y ) .o A ) e. On ) )
32 oesuc 
 |-  ( ( A e. On /\ y e. On ) -> ( A ^o suc y ) = ( ( A ^o y ) .o A ) )
33 32 eleq1d 
 |-  ( ( A e. On /\ y e. On ) -> ( ( A ^o suc y ) e. On <-> ( ( A ^o y ) .o A ) e. On ) )
34 31 33 sylibrd 
 |-  ( ( A e. On /\ y e. On ) -> ( ( A ^o y ) e. On -> ( A ^o suc y ) e. On ) )
35 34 expcom 
 |-  ( y e. On -> ( A e. On -> ( ( A ^o y ) e. On -> ( A ^o suc y ) e. On ) ) )
36 35 adantrd 
 |-  ( y e. On -> ( ( A e. On /\ (/) e. A ) -> ( ( A ^o y ) e. On -> ( A ^o suc y ) e. On ) ) )
37 vex 
 |-  x e. _V
38 iunon 
 |-  ( ( x e. _V /\ A. y e. x ( A ^o y ) e. On ) -> U_ y e. x ( A ^o y ) e. On )
39 37 38 mpan 
 |-  ( A. y e. x ( A ^o y ) e. On -> U_ y e. x ( A ^o y ) e. On )
40 oelim 
 |-  ( ( ( A e. On /\ ( x e. _V /\ Lim x ) ) /\ (/) e. A ) -> ( A ^o x ) = U_ y e. x ( A ^o y ) )
41 37 40 mpanlr1 
 |-  ( ( ( A e. On /\ Lim x ) /\ (/) e. A ) -> ( A ^o x ) = U_ y e. x ( A ^o y ) )
42 41 anasss 
 |-  ( ( A e. On /\ ( Lim x /\ (/) e. A ) ) -> ( A ^o x ) = U_ y e. x ( A ^o y ) )
43 42 an12s 
 |-  ( ( Lim x /\ ( A e. On /\ (/) e. A ) ) -> ( A ^o x ) = U_ y e. x ( A ^o y ) )
44 43 eleq1d 
 |-  ( ( Lim x /\ ( A e. On /\ (/) e. A ) ) -> ( ( A ^o x ) e. On <-> U_ y e. x ( A ^o y ) e. On ) )
45 39 44 syl5ibr 
 |-  ( ( Lim x /\ ( A e. On /\ (/) e. A ) ) -> ( A. y e. x ( A ^o y ) e. On -> ( A ^o x ) e. On ) )
46 45 ex 
 |-  ( Lim x -> ( ( A e. On /\ (/) e. A ) -> ( A. y e. x ( A ^o y ) e. On -> ( A ^o x ) e. On ) ) )
47 19 21 23 25 28 36 46 tfinds3 
 |-  ( B e. On -> ( ( A e. On /\ (/) e. A ) -> ( A ^o B ) e. On ) )
48 47 expd 
 |-  ( B e. On -> ( A e. On -> ( (/) e. A -> ( A ^o B ) e. On ) ) )
49 48 com12 
 |-  ( A e. On -> ( B e. On -> ( (/) e. A -> ( A ^o B ) e. On ) ) )
50 49 imp31 
 |-  ( ( ( A e. On /\ B e. On ) /\ (/) e. A ) -> ( A ^o B ) e. On )
51 17 50 oe0lem 
 |-  ( ( A e. On /\ B e. On ) -> ( A ^o B ) e. On )