# Metamath Proof Explorer

## Theorem oecl

Description: Closure law for ordinal exponentiation. (Contributed by NM, 1-Jan-2005) (Proof shortened by Andrew Salmon, 22-Oct-2011)

Ref Expression
Assertion oecl ${⊢}\left({A}\in \mathrm{On}\wedge {B}\in \mathrm{On}\right)\to {A}{↑}_{𝑜}{B}\in \mathrm{On}$

### Proof

Step Hyp Ref Expression
1 oveq2 ${⊢}{B}=\varnothing \to \varnothing {↑}_{𝑜}{B}=\varnothing {↑}_{𝑜}\varnothing$
2 oe0m0 ${⊢}\varnothing {↑}_{𝑜}\varnothing ={1}_{𝑜}$
3 1on ${⊢}{1}_{𝑜}\in \mathrm{On}$
4 2 3 eqeltri ${⊢}\varnothing {↑}_{𝑜}\varnothing \in \mathrm{On}$
5 1 4 syl6eqel ${⊢}{B}=\varnothing \to \varnothing {↑}_{𝑜}{B}\in \mathrm{On}$
6 5 adantl ${⊢}\left({B}\in \mathrm{On}\wedge {B}=\varnothing \right)\to \varnothing {↑}_{𝑜}{B}\in \mathrm{On}$
7 oe0m1 ${⊢}{B}\in \mathrm{On}\to \left(\varnothing \in {B}↔\varnothing {↑}_{𝑜}{B}=\varnothing \right)$
8 7 biimpa ${⊢}\left({B}\in \mathrm{On}\wedge \varnothing \in {B}\right)\to \varnothing {↑}_{𝑜}{B}=\varnothing$
9 0elon ${⊢}\varnothing \in \mathrm{On}$
10 8 9 syl6eqel ${⊢}\left({B}\in \mathrm{On}\wedge \varnothing \in {B}\right)\to \varnothing {↑}_{𝑜}{B}\in \mathrm{On}$
11 10 adantll ${⊢}\left(\left({B}\in \mathrm{On}\wedge {B}\in \mathrm{On}\right)\wedge \varnothing \in {B}\right)\to \varnothing {↑}_{𝑜}{B}\in \mathrm{On}$
12 6 11 oe0lem ${⊢}\left({B}\in \mathrm{On}\wedge {B}\in \mathrm{On}\right)\to \varnothing {↑}_{𝑜}{B}\in \mathrm{On}$
13 12 anidms ${⊢}{B}\in \mathrm{On}\to \varnothing {↑}_{𝑜}{B}\in \mathrm{On}$
14 oveq1 ${⊢}{A}=\varnothing \to {A}{↑}_{𝑜}{B}=\varnothing {↑}_{𝑜}{B}$
15 14 eleq1d ${⊢}{A}=\varnothing \to \left({A}{↑}_{𝑜}{B}\in \mathrm{On}↔\varnothing {↑}_{𝑜}{B}\in \mathrm{On}\right)$
16 13 15 syl5ibr ${⊢}{A}=\varnothing \to \left({B}\in \mathrm{On}\to {A}{↑}_{𝑜}{B}\in \mathrm{On}\right)$
17 16 impcom ${⊢}\left({B}\in \mathrm{On}\wedge {A}=\varnothing \right)\to {A}{↑}_{𝑜}{B}\in \mathrm{On}$
18 oveq2 ${⊢}{x}=\varnothing \to {A}{↑}_{𝑜}{x}={A}{↑}_{𝑜}\varnothing$
19 18 eleq1d ${⊢}{x}=\varnothing \to \left({A}{↑}_{𝑜}{x}\in \mathrm{On}↔{A}{↑}_{𝑜}\varnothing \in \mathrm{On}\right)$
20 oveq2 ${⊢}{x}={y}\to {A}{↑}_{𝑜}{x}={A}{↑}_{𝑜}{y}$
21 20 eleq1d ${⊢}{x}={y}\to \left({A}{↑}_{𝑜}{x}\in \mathrm{On}↔{A}{↑}_{𝑜}{y}\in \mathrm{On}\right)$
22 oveq2 ${⊢}{x}=\mathrm{suc}{y}\to {A}{↑}_{𝑜}{x}={A}{↑}_{𝑜}\mathrm{suc}{y}$
23 22 eleq1d ${⊢}{x}=\mathrm{suc}{y}\to \left({A}{↑}_{𝑜}{x}\in \mathrm{On}↔{A}{↑}_{𝑜}\mathrm{suc}{y}\in \mathrm{On}\right)$
24 oveq2 ${⊢}{x}={B}\to {A}{↑}_{𝑜}{x}={A}{↑}_{𝑜}{B}$
25 24 eleq1d ${⊢}{x}={B}\to \left({A}{↑}_{𝑜}{x}\in \mathrm{On}↔{A}{↑}_{𝑜}{B}\in \mathrm{On}\right)$
26 oe0 ${⊢}{A}\in \mathrm{On}\to {A}{↑}_{𝑜}\varnothing ={1}_{𝑜}$
27 26 3 syl6eqel ${⊢}{A}\in \mathrm{On}\to {A}{↑}_{𝑜}\varnothing \in \mathrm{On}$
28 27 adantr ${⊢}\left({A}\in \mathrm{On}\wedge \varnothing \in {A}\right)\to {A}{↑}_{𝑜}\varnothing \in \mathrm{On}$
29 omcl ${⊢}\left({A}{↑}_{𝑜}{y}\in \mathrm{On}\wedge {A}\in \mathrm{On}\right)\to \left({A}{↑}_{𝑜}{y}\right){\cdot }_{𝑜}{A}\in \mathrm{On}$
30 29 expcom ${⊢}{A}\in \mathrm{On}\to \left({A}{↑}_{𝑜}{y}\in \mathrm{On}\to \left({A}{↑}_{𝑜}{y}\right){\cdot }_{𝑜}{A}\in \mathrm{On}\right)$
31 30 adantr ${⊢}\left({A}\in \mathrm{On}\wedge {y}\in \mathrm{On}\right)\to \left({A}{↑}_{𝑜}{y}\in \mathrm{On}\to \left({A}{↑}_{𝑜}{y}\right){\cdot }_{𝑜}{A}\in \mathrm{On}\right)$
32 oesuc ${⊢}\left({A}\in \mathrm{On}\wedge {y}\in \mathrm{On}\right)\to {A}{↑}_{𝑜}\mathrm{suc}{y}=\left({A}{↑}_{𝑜}{y}\right){\cdot }_{𝑜}{A}$
33 32 eleq1d ${⊢}\left({A}\in \mathrm{On}\wedge {y}\in \mathrm{On}\right)\to \left({A}{↑}_{𝑜}\mathrm{suc}{y}\in \mathrm{On}↔\left({A}{↑}_{𝑜}{y}\right){\cdot }_{𝑜}{A}\in \mathrm{On}\right)$
34 31 33 sylibrd ${⊢}\left({A}\in \mathrm{On}\wedge {y}\in \mathrm{On}\right)\to \left({A}{↑}_{𝑜}{y}\in \mathrm{On}\to {A}{↑}_{𝑜}\mathrm{suc}{y}\in \mathrm{On}\right)$
35 34 expcom ${⊢}{y}\in \mathrm{On}\to \left({A}\in \mathrm{On}\to \left({A}{↑}_{𝑜}{y}\in \mathrm{On}\to {A}{↑}_{𝑜}\mathrm{suc}{y}\in \mathrm{On}\right)\right)$
36 35 adantrd ${⊢}{y}\in \mathrm{On}\to \left(\left({A}\in \mathrm{On}\wedge \varnothing \in {A}\right)\to \left({A}{↑}_{𝑜}{y}\in \mathrm{On}\to {A}{↑}_{𝑜}\mathrm{suc}{y}\in \mathrm{On}\right)\right)$
37 vex ${⊢}{x}\in \mathrm{V}$
38 iunon ${⊢}\left({x}\in \mathrm{V}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{A}{↑}_{𝑜}{y}\in \mathrm{On}\right)\to \bigcup _{{y}\in {x}}\left({A}{↑}_{𝑜}{y}\right)\in \mathrm{On}$
39 37 38 mpan ${⊢}\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{A}{↑}_{𝑜}{y}\in \mathrm{On}\to \bigcup _{{y}\in {x}}\left({A}{↑}_{𝑜}{y}\right)\in \mathrm{On}$
40 oelim ${⊢}\left(\left({A}\in \mathrm{On}\wedge \left({x}\in \mathrm{V}\wedge \mathrm{Lim}{x}\right)\right)\wedge \varnothing \in {A}\right)\to {A}{↑}_{𝑜}{x}=\bigcup _{{y}\in {x}}\left({A}{↑}_{𝑜}{y}\right)$
41 37 40 mpanlr1 ${⊢}\left(\left({A}\in \mathrm{On}\wedge \mathrm{Lim}{x}\right)\wedge \varnothing \in {A}\right)\to {A}{↑}_{𝑜}{x}=\bigcup _{{y}\in {x}}\left({A}{↑}_{𝑜}{y}\right)$
42 41 anasss ${⊢}\left({A}\in \mathrm{On}\wedge \left(\mathrm{Lim}{x}\wedge \varnothing \in {A}\right)\right)\to {A}{↑}_{𝑜}{x}=\bigcup _{{y}\in {x}}\left({A}{↑}_{𝑜}{y}\right)$
43 42 an12s ${⊢}\left(\mathrm{Lim}{x}\wedge \left({A}\in \mathrm{On}\wedge \varnothing \in {A}\right)\right)\to {A}{↑}_{𝑜}{x}=\bigcup _{{y}\in {x}}\left({A}{↑}_{𝑜}{y}\right)$
44 43 eleq1d ${⊢}\left(\mathrm{Lim}{x}\wedge \left({A}\in \mathrm{On}\wedge \varnothing \in {A}\right)\right)\to \left({A}{↑}_{𝑜}{x}\in \mathrm{On}↔\bigcup _{{y}\in {x}}\left({A}{↑}_{𝑜}{y}\right)\in \mathrm{On}\right)$
45 39 44 syl5ibr ${⊢}\left(\mathrm{Lim}{x}\wedge \left({A}\in \mathrm{On}\wedge \varnothing \in {A}\right)\right)\to \left(\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{A}{↑}_{𝑜}{y}\in \mathrm{On}\to {A}{↑}_{𝑜}{x}\in \mathrm{On}\right)$
46 45 ex ${⊢}\mathrm{Lim}{x}\to \left(\left({A}\in \mathrm{On}\wedge \varnothing \in {A}\right)\to \left(\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{A}{↑}_{𝑜}{y}\in \mathrm{On}\to {A}{↑}_{𝑜}{x}\in \mathrm{On}\right)\right)$
47 19 21 23 25 28 36 46 tfinds3 ${⊢}{B}\in \mathrm{On}\to \left(\left({A}\in \mathrm{On}\wedge \varnothing \in {A}\right)\to {A}{↑}_{𝑜}{B}\in \mathrm{On}\right)$
48 47 expd ${⊢}{B}\in \mathrm{On}\to \left({A}\in \mathrm{On}\to \left(\varnothing \in {A}\to {A}{↑}_{𝑜}{B}\in \mathrm{On}\right)\right)$
49 48 com12 ${⊢}{A}\in \mathrm{On}\to \left({B}\in \mathrm{On}\to \left(\varnothing \in {A}\to {A}{↑}_{𝑜}{B}\in \mathrm{On}\right)\right)$
50 49 imp31 ${⊢}\left(\left({A}\in \mathrm{On}\wedge {B}\in \mathrm{On}\right)\wedge \varnothing \in {A}\right)\to {A}{↑}_{𝑜}{B}\in \mathrm{On}$
51 17 50 oe0lem ${⊢}\left({A}\in \mathrm{On}\wedge {B}\in \mathrm{On}\right)\to {A}{↑}_{𝑜}{B}\in \mathrm{On}$