# Metamath Proof Explorer

## Theorem oelim

Description: Ordinal exponentiation with a limit exponent and nonzero mantissa. Definition 8.30 of TakeutiZaring p. 67. (Contributed by NM, 1-Jan-2005) (Revised by Mario Carneiro, 8-Sep-2013)

Ref Expression
Assertion oelim ${⊢}\left(\left({A}\in \mathrm{On}\wedge \left({B}\in {C}\wedge \mathrm{Lim}{B}\right)\right)\wedge \varnothing \in {A}\right)\to {A}{↑}_{𝑜}{B}=\bigcup _{{x}\in {B}}\left({A}{↑}_{𝑜}{x}\right)$

### Proof

Step Hyp Ref Expression
1 limelon ${⊢}\left({B}\in {C}\wedge \mathrm{Lim}{B}\right)\to {B}\in \mathrm{On}$
2 simpr ${⊢}\left({B}\in {C}\wedge \mathrm{Lim}{B}\right)\to \mathrm{Lim}{B}$
3 1 2 jca ${⊢}\left({B}\in {C}\wedge \mathrm{Lim}{B}\right)\to \left({B}\in \mathrm{On}\wedge \mathrm{Lim}{B}\right)$
4 rdglim2a ${⊢}\left({B}\in \mathrm{On}\wedge \mathrm{Lim}{B}\right)\to \mathrm{rec}\left(\left({y}\in \mathrm{V}⟼{y}{\cdot }_{𝑜}{A}\right),{1}_{𝑜}\right)\left({B}\right)=\bigcup _{{x}\in {B}}\mathrm{rec}\left(\left({y}\in \mathrm{V}⟼{y}{\cdot }_{𝑜}{A}\right),{1}_{𝑜}\right)\left({x}\right)$
5 4 ad2antlr ${⊢}\left(\left({A}\in \mathrm{On}\wedge \left({B}\in \mathrm{On}\wedge \mathrm{Lim}{B}\right)\right)\wedge \varnothing \in {A}\right)\to \mathrm{rec}\left(\left({y}\in \mathrm{V}⟼{y}{\cdot }_{𝑜}{A}\right),{1}_{𝑜}\right)\left({B}\right)=\bigcup _{{x}\in {B}}\mathrm{rec}\left(\left({y}\in \mathrm{V}⟼{y}{\cdot }_{𝑜}{A}\right),{1}_{𝑜}\right)\left({x}\right)$
6 oevn0 ${⊢}\left(\left({A}\in \mathrm{On}\wedge {B}\in \mathrm{On}\right)\wedge \varnothing \in {A}\right)\to {A}{↑}_{𝑜}{B}=\mathrm{rec}\left(\left({y}\in \mathrm{V}⟼{y}{\cdot }_{𝑜}{A}\right),{1}_{𝑜}\right)\left({B}\right)$
7 onelon ${⊢}\left({B}\in \mathrm{On}\wedge {x}\in {B}\right)\to {x}\in \mathrm{On}$
8 oevn0 ${⊢}\left(\left({A}\in \mathrm{On}\wedge {x}\in \mathrm{On}\right)\wedge \varnothing \in {A}\right)\to {A}{↑}_{𝑜}{x}=\mathrm{rec}\left(\left({y}\in \mathrm{V}⟼{y}{\cdot }_{𝑜}{A}\right),{1}_{𝑜}\right)\left({x}\right)$
9 7 8 sylanl2 ${⊢}\left(\left({A}\in \mathrm{On}\wedge \left({B}\in \mathrm{On}\wedge {x}\in {B}\right)\right)\wedge \varnothing \in {A}\right)\to {A}{↑}_{𝑜}{x}=\mathrm{rec}\left(\left({y}\in \mathrm{V}⟼{y}{\cdot }_{𝑜}{A}\right),{1}_{𝑜}\right)\left({x}\right)$
10 9 exp42 ${⊢}{A}\in \mathrm{On}\to \left({B}\in \mathrm{On}\to \left({x}\in {B}\to \left(\varnothing \in {A}\to {A}{↑}_{𝑜}{x}=\mathrm{rec}\left(\left({y}\in \mathrm{V}⟼{y}{\cdot }_{𝑜}{A}\right),{1}_{𝑜}\right)\left({x}\right)\right)\right)\right)$
11 10 com34 ${⊢}{A}\in \mathrm{On}\to \left({B}\in \mathrm{On}\to \left(\varnothing \in {A}\to \left({x}\in {B}\to {A}{↑}_{𝑜}{x}=\mathrm{rec}\left(\left({y}\in \mathrm{V}⟼{y}{\cdot }_{𝑜}{A}\right),{1}_{𝑜}\right)\left({x}\right)\right)\right)\right)$
12 11 imp41 ${⊢}\left(\left(\left({A}\in \mathrm{On}\wedge {B}\in \mathrm{On}\right)\wedge \varnothing \in {A}\right)\wedge {x}\in {B}\right)\to {A}{↑}_{𝑜}{x}=\mathrm{rec}\left(\left({y}\in \mathrm{V}⟼{y}{\cdot }_{𝑜}{A}\right),{1}_{𝑜}\right)\left({x}\right)$
13 12 iuneq2dv ${⊢}\left(\left({A}\in \mathrm{On}\wedge {B}\in \mathrm{On}\right)\wedge \varnothing \in {A}\right)\to \bigcup _{{x}\in {B}}\left({A}{↑}_{𝑜}{x}\right)=\bigcup _{{x}\in {B}}\mathrm{rec}\left(\left({y}\in \mathrm{V}⟼{y}{\cdot }_{𝑜}{A}\right),{1}_{𝑜}\right)\left({x}\right)$
14 6 13 eqeq12d ${⊢}\left(\left({A}\in \mathrm{On}\wedge {B}\in \mathrm{On}\right)\wedge \varnothing \in {A}\right)\to \left({A}{↑}_{𝑜}{B}=\bigcup _{{x}\in {B}}\left({A}{↑}_{𝑜}{x}\right)↔\mathrm{rec}\left(\left({y}\in \mathrm{V}⟼{y}{\cdot }_{𝑜}{A}\right),{1}_{𝑜}\right)\left({B}\right)=\bigcup _{{x}\in {B}}\mathrm{rec}\left(\left({y}\in \mathrm{V}⟼{y}{\cdot }_{𝑜}{A}\right),{1}_{𝑜}\right)\left({x}\right)\right)$
15 14 adantlrr ${⊢}\left(\left({A}\in \mathrm{On}\wedge \left({B}\in \mathrm{On}\wedge \mathrm{Lim}{B}\right)\right)\wedge \varnothing \in {A}\right)\to \left({A}{↑}_{𝑜}{B}=\bigcup _{{x}\in {B}}\left({A}{↑}_{𝑜}{x}\right)↔\mathrm{rec}\left(\left({y}\in \mathrm{V}⟼{y}{\cdot }_{𝑜}{A}\right),{1}_{𝑜}\right)\left({B}\right)=\bigcup _{{x}\in {B}}\mathrm{rec}\left(\left({y}\in \mathrm{V}⟼{y}{\cdot }_{𝑜}{A}\right),{1}_{𝑜}\right)\left({x}\right)\right)$
16 5 15 mpbird ${⊢}\left(\left({A}\in \mathrm{On}\wedge \left({B}\in \mathrm{On}\wedge \mathrm{Lim}{B}\right)\right)\wedge \varnothing \in {A}\right)\to {A}{↑}_{𝑜}{B}=\bigcup _{{x}\in {B}}\left({A}{↑}_{𝑜}{x}\right)$
17 3 16 sylanl2 ${⊢}\left(\left({A}\in \mathrm{On}\wedge \left({B}\in {C}\wedge \mathrm{Lim}{B}\right)\right)\wedge \varnothing \in {A}\right)\to {A}{↑}_{𝑜}{B}=\bigcup _{{x}\in {B}}\left({A}{↑}_{𝑜}{x}\right)$