Metamath Proof Explorer

Theorem oen0

Description: Ordinal exponentiation with a nonzero base is nonzero. Proposition 8.32 of TakeutiZaring p. 67. (Contributed by NM, 4-Jan-2005)

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

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( x = (/) -> ( A ^o x ) = ( A ^o (/) ) )
2 1 eleq2d 
 |-  ( x = (/) -> ( (/) e. ( A ^o x ) <-> (/) e. ( A ^o (/) ) ) )
3 oveq2 
 |-  ( x = y -> ( A ^o x ) = ( A ^o y ) )
4 3 eleq2d 
 |-  ( x = y -> ( (/) e. ( A ^o x ) <-> (/) e. ( A ^o y ) ) )
5 oveq2 
 |-  ( x = suc y -> ( A ^o x ) = ( A ^o suc y ) )
6 5 eleq2d 
 |-  ( x = suc y -> ( (/) e. ( A ^o x ) <-> (/) e. ( A ^o suc y ) ) )
7 oveq2 
 |-  ( x = B -> ( A ^o x ) = ( A ^o B ) )
8 7 eleq2d 
 |-  ( x = B -> ( (/) e. ( A ^o x ) <-> (/) e. ( A ^o B ) ) )
9 0lt1o 
 |-  (/) e. 1o
10 oe0 
 |-  ( A e. On -> ( A ^o (/) ) = 1o )
11 9 10 eleqtrrid 
 |-  ( A e. On -> (/) e. ( A ^o (/) ) )
12 11 adantr 
 |-  ( ( A e. On /\ (/) e. A ) -> (/) e. ( A ^o (/) ) )
13 oecl 
 |-  ( ( A e. On /\ y e. On ) -> ( A ^o y ) e. On )
14 omordi 
 |-  ( ( ( A e. On /\ ( A ^o y ) e. On ) /\ (/) e. ( A ^o y ) ) -> ( (/) e. A -> ( ( A ^o y ) .o (/) ) e. ( ( A ^o y ) .o A ) ) )
15 om0 
 |-  ( ( A ^o y ) e. On -> ( ( A ^o y ) .o (/) ) = (/) )
16 15 eleq1d 
 |-  ( ( A ^o y ) e. On -> ( ( ( A ^o y ) .o (/) ) e. ( ( A ^o y ) .o A ) <-> (/) e. ( ( A ^o y ) .o A ) ) )
17 16 ad2antlr 
 |-  ( ( ( A e. On /\ ( A ^o y ) e. On ) /\ (/) e. ( A ^o y ) ) -> ( ( ( A ^o y ) .o (/) ) e. ( ( A ^o y ) .o A ) <-> (/) e. ( ( A ^o y ) .o A ) ) )
18 14 17 sylibd 
 |-  ( ( ( A e. On /\ ( A ^o y ) e. On ) /\ (/) e. ( A ^o y ) ) -> ( (/) e. A -> (/) e. ( ( A ^o y ) .o A ) ) )
19 13 18 syldanl 
 |-  ( ( ( A e. On /\ y e. On ) /\ (/) e. ( A ^o y ) ) -> ( (/) e. A -> (/) e. ( ( A ^o y ) .o A ) ) )
20 oesuc 
 |-  ( ( A e. On /\ y e. On ) -> ( A ^o suc y ) = ( ( A ^o y ) .o A ) )
21 20 eleq2d 
 |-  ( ( A e. On /\ y e. On ) -> ( (/) e. ( A ^o suc y ) <-> (/) e. ( ( A ^o y ) .o A ) ) )
22 21 adantr 
 |-  ( ( ( A e. On /\ y e. On ) /\ (/) e. ( A ^o y ) ) -> ( (/) e. ( A ^o suc y ) <-> (/) e. ( ( A ^o y ) .o A ) ) )
23 19 22 sylibrd 
 |-  ( ( ( A e. On /\ y e. On ) /\ (/) e. ( A ^o y ) ) -> ( (/) e. A -> (/) e. ( A ^o suc y ) ) )
24 23 exp31 
 |-  ( A e. On -> ( y e. On -> ( (/) e. ( A ^o y ) -> ( (/) e. A -> (/) e. ( A ^o suc y ) ) ) ) )
25 24 com12 
 |-  ( y e. On -> ( A e. On -> ( (/) e. ( A ^o y ) -> ( (/) e. A -> (/) e. ( A ^o suc y ) ) ) ) )
26 25 com34 
 |-  ( y e. On -> ( A e. On -> ( (/) e. A -> ( (/) e. ( A ^o y ) -> (/) e. ( A ^o suc y ) ) ) ) )
27 26 impd 
 |-  ( y e. On -> ( ( A e. On /\ (/) e. A ) -> ( (/) e. ( A ^o y ) -> (/) e. ( A ^o suc y ) ) ) )
28 0ellim 
 |-  ( Lim x -> (/) e. x )
29 eqimss2 
 |-  ( ( A ^o (/) ) = 1o -> 1o C_ ( A ^o (/) ) )
30 10 29 syl 
 |-  ( A e. On -> 1o C_ ( A ^o (/) ) )
31 oveq2 
 |-  ( y = (/) -> ( A ^o y ) = ( A ^o (/) ) )
32 31 sseq2d 
 |-  ( y = (/) -> ( 1o C_ ( A ^o y ) <-> 1o C_ ( A ^o (/) ) ) )
33 32 rspcev 
 |-  ( ( (/) e. x /\ 1o C_ ( A ^o (/) ) ) -> E. y e. x 1o C_ ( A ^o y ) )
34 28 30 33 syl2an 
 |-  ( ( Lim x /\ A e. On ) -> E. y e. x 1o C_ ( A ^o y ) )
35 ssiun 
 |-  ( E. y e. x 1o C_ ( A ^o y ) -> 1o C_ U_ y e. x ( A ^o y ) )
36 34 35 syl 
 |-  ( ( Lim x /\ A e. On ) -> 1o C_ U_ y e. x ( A ^o y ) )
37 36 adantrr 
 |-  ( ( Lim x /\ ( A e. On /\ (/) e. A ) ) -> 1o C_ U_ y e. x ( A ^o y ) )
38 vex 
 |-  x e. _V
39 oelim 
 |-  ( ( ( A e. On /\ ( x e. _V /\ Lim x ) ) /\ (/) e. A ) -> ( A ^o x ) = U_ y e. x ( A ^o y ) )
40 38 39 mpanlr1 
 |-  ( ( ( A e. On /\ Lim x ) /\ (/) e. A ) -> ( A ^o x ) = U_ y e. x ( A ^o y ) )
41 40 anasss 
 |-  ( ( A e. On /\ ( Lim x /\ (/) e. A ) ) -> ( A ^o x ) = U_ y e. x ( A ^o y ) )
42 41 an12s 
 |-  ( ( Lim x /\ ( A e. On /\ (/) e. A ) ) -> ( A ^o x ) = U_ y e. x ( A ^o y ) )
43 37 42 sseqtrrd 
 |-  ( ( Lim x /\ ( A e. On /\ (/) e. A ) ) -> 1o C_ ( A ^o x ) )
44 limelon 
 |-  ( ( x e. _V /\ Lim x ) -> x e. On )
45 38 44 mpan 
 |-  ( Lim x -> x e. On )
46 oecl 
 |-  ( ( A e. On /\ x e. On ) -> ( A ^o x ) e. On )
47 46 ancoms 
 |-  ( ( x e. On /\ A e. On ) -> ( A ^o x ) e. On )
48 45 47 sylan 
 |-  ( ( Lim x /\ A e. On ) -> ( A ^o x ) e. On )
49 eloni 
 |-  ( ( A ^o x ) e. On -> Ord ( A ^o x ) )
50 ordgt0ge1 
 |-  ( Ord ( A ^o x ) -> ( (/) e. ( A ^o x ) <-> 1o C_ ( A ^o x ) ) )
51 48 49 50 3syl 
 |-  ( ( Lim x /\ A e. On ) -> ( (/) e. ( A ^o x ) <-> 1o C_ ( A ^o x ) ) )
52 51 adantrr 
 |-  ( ( Lim x /\ ( A e. On /\ (/) e. A ) ) -> ( (/) e. ( A ^o x ) <-> 1o C_ ( A ^o x ) ) )
53 43 52 mpbird 
 |-  ( ( Lim x /\ ( A e. On /\ (/) e. A ) ) -> (/) e. ( A ^o x ) )
54 53 ex 
 |-  ( Lim x -> ( ( A e. On /\ (/) e. A ) -> (/) e. ( A ^o x ) ) )
55 54 a1dd 
 |-  ( Lim x -> ( ( A e. On /\ (/) e. A ) -> ( A. y e. x (/) e. ( A ^o y ) -> (/) e. ( A ^o x ) ) ) )
56 2 4 6 8 12 27 55 tfinds3 
 |-  ( B e. On -> ( ( A e. On /\ (/) e. A ) -> (/) e. ( A ^o B ) ) )
57 56 expd 
 |-  ( B e. On -> ( A e. On -> ( (/) e. A -> (/) e. ( A ^o B ) ) ) )
58 57 com12 
 |-  ( A e. On -> ( B e. On -> ( (/) e. A -> (/) e. ( A ^o B ) ) ) )
59 58 imp31 
 |-  ( ( ( A e. On /\ B e. On ) /\ (/) e. A ) -> (/) e. ( A ^o B ) )