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 On B On A A 𝑜 B

Proof

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