Metamath Proof Explorer

Theorem oe0suclim

Description: Closed form expression of the value of ordinal exponentiation for the cases when the second ordinal is zero, a successor ordinal, or a limit ordinal. Definition 2.6 of Schloeder p. 4. See oe0 , oesuc , oe0m1 , and oelim . (Contributed by RP, 18-Jan-2025)

Ref Expression
Assertion oe0suclim ⊢A∈On∧B∈On→B=∅→A↑𝑜B=1𝑜∧B=suc⁡C∧C∈On→A↑𝑜B=A↑𝑜C⋅𝑜A∧Lim⁡B→A↑𝑜B=if∅∈A⋃c∈BA↑𝑜c∅

Proof

Step Hyp Ref Expression
1 oe0 ⊢A∈On→A↑𝑜∅=1𝑜
2 oesuc ⊢A∈On∧C∈On→A↑𝑜suc⁡C=A↑𝑜C⋅𝑜A
3 oelim ⊢A∈On∧B∈On∧Lim⁡B∧∅∈A→A↑𝑜B=⋃c∈BA↑𝑜c
4 simpr ⊢A∈On∧B∈On∧Lim⁡B∧∅∈A→∅∈A
5 4 iftrued ⊢A∈On∧B∈On∧Lim⁡B∧∅∈A→if∅∈A⋃c∈BA↑𝑜c∅=⋃c∈BA↑𝑜c
6 3 5 eqtr4d ⊢A∈On∧B∈On∧Lim⁡B∧∅∈A→A↑𝑜B=if∅∈A⋃c∈BA↑𝑜c∅
7 simpl ⊢A∈On∧B∈On∧Lim⁡B→A∈On
8 0elon ⊢∅∈On
9 ontri1 ⊢A∈On∧∅∈On→A⊆∅↔¬∅∈A
10 ss0 ⊢A⊆∅→A=∅
11 9 10 syl6bir ⊢A∈On∧∅∈On→¬∅∈A→A=∅
12 7 8 11 sylancl ⊢A∈On∧B∈On∧Lim⁡B→¬∅∈A→A=∅
13 oveq1 ⊢A=∅→A↑𝑜B=∅↑𝑜B
14 oe0m1 ⊢B∈On→∅∈B↔∅↑𝑜B=∅
15 14 biimpd ⊢B∈On→∅∈B→∅↑𝑜B=∅
16 0ellim ⊢Lim⁡B→∅∈B
17 15 16 impel ⊢B∈On∧Lim⁡B→∅↑𝑜B=∅
18 17 adantl ⊢A∈On∧B∈On∧Lim⁡B→∅↑𝑜B=∅
19 13 18 sylan9eqr ⊢A∈On∧B∈On∧Lim⁡B∧A=∅→A↑𝑜B=∅
20 19 ex ⊢A∈On∧B∈On∧Lim⁡B→A=∅→A↑𝑜B=∅
21 12 20 syld ⊢A∈On∧B∈On∧Lim⁡B→¬∅∈A→A↑𝑜B=∅
22 21 imp ⊢A∈On∧B∈On∧Lim⁡B∧¬∅∈A→A↑𝑜B=∅
23 simpr ⊢A∈On∧B∈On∧Lim⁡B∧¬∅∈A→¬∅∈A
24 23 iffalsed ⊢A∈On∧B∈On∧Lim⁡B∧¬∅∈A→if∅∈A⋃c∈BA↑𝑜c∅=∅
25 22 24 eqtr4d ⊢A∈On∧B∈On∧Lim⁡B∧¬∅∈A→A↑𝑜B=if∅∈A⋃c∈BA↑𝑜c∅
26 6 25 pm2.61dan ⊢A∈On∧B∈On∧Lim⁡B→A↑𝑜B=if∅∈A⋃c∈BA↑𝑜c∅
27 26 anassrs ⊢A∈On∧B∈On∧Lim⁡B→A↑𝑜B=if∅∈A⋃c∈BA↑𝑜c∅
28 1 2 27 onov0suclim ⊢A∈On∧B∈On→B=∅→A↑𝑜B=1𝑜∧B=suc⁡C∧C∈On→A↑𝑜B=A↑𝑜C⋅𝑜A∧Lim⁡B→A↑𝑜B=if∅∈A⋃c∈BA↑𝑜c∅