Metamath Proof Explorer

Theorem om0suclim

Description: Closed form expression of the value of ordinal multiplication for the cases when the second ordinal is zero, a successor ordinal, or a limit ordinal. Definition 2.5 of Schloeder p. 4. See om0 , omsuc , and omlim . (Contributed by RP, 18-Jan-2025)

Ref Expression
Assertion om0suclim ⊢A∈On∧B∈On→B=∅→A⋅𝑜B=∅∧B=suc⁡C∧C∈On→A⋅𝑜B=A⋅𝑜C+𝑜A∧Lim⁡B→A⋅𝑜B=⋃c∈BA⋅𝑜c

Proof

Step Hyp Ref Expression
1 om0 ⊢A∈On→A⋅𝑜∅=∅
2 omsuc ⊢A∈On∧C∈On→A⋅𝑜suc⁡C=A⋅𝑜C+𝑜A
3 omlim ⊢A∈On∧B∈On∧Lim⁡B→A⋅𝑜B=⋃c∈BA⋅𝑜c
4 3 anassrs ⊢A∈On∧B∈On∧Lim⁡B→A⋅𝑜B=⋃c∈BA⋅𝑜c
5 1 2 4 onov0suclim ⊢A∈On∧B∈On→B=∅→A⋅𝑜B=∅∧B=suc⁡C∧C∈On→A⋅𝑜B=A⋅𝑜C+𝑜A∧Lim⁡B→A⋅𝑜B=⋃c∈BA⋅𝑜c