# Metamath Proof Explorer

## Theorem oeworde

Description: Ordinal exponentiation compared to its exponent. Proposition 8.37 of TakeutiZaring p. 68. (Contributed by NM, 7-Jan-2005) (Revised by Mario Carneiro, 24-May-2015)

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

### Proof

Step Hyp Ref Expression
1 id ${⊢}{x}=\varnothing \to {x}=\varnothing$
2 oveq2 ${⊢}{x}=\varnothing \to {A}{↑}_{𝑜}{x}={A}{↑}_{𝑜}\varnothing$
3 1 2 sseq12d ${⊢}{x}=\varnothing \to \left({x}\subseteq {A}{↑}_{𝑜}{x}↔\varnothing \subseteq {A}{↑}_{𝑜}\varnothing \right)$
4 id ${⊢}{x}={y}\to {x}={y}$
5 oveq2 ${⊢}{x}={y}\to {A}{↑}_{𝑜}{x}={A}{↑}_{𝑜}{y}$
6 4 5 sseq12d ${⊢}{x}={y}\to \left({x}\subseteq {A}{↑}_{𝑜}{x}↔{y}\subseteq {A}{↑}_{𝑜}{y}\right)$
7 id ${⊢}{x}=\mathrm{suc}{y}\to {x}=\mathrm{suc}{y}$
8 oveq2 ${⊢}{x}=\mathrm{suc}{y}\to {A}{↑}_{𝑜}{x}={A}{↑}_{𝑜}\mathrm{suc}{y}$
9 7 8 sseq12d ${⊢}{x}=\mathrm{suc}{y}\to \left({x}\subseteq {A}{↑}_{𝑜}{x}↔\mathrm{suc}{y}\subseteq {A}{↑}_{𝑜}\mathrm{suc}{y}\right)$
10 id ${⊢}{x}={B}\to {x}={B}$
11 oveq2 ${⊢}{x}={B}\to {A}{↑}_{𝑜}{x}={A}{↑}_{𝑜}{B}$
12 10 11 sseq12d ${⊢}{x}={B}\to \left({x}\subseteq {A}{↑}_{𝑜}{x}↔{B}\subseteq {A}{↑}_{𝑜}{B}\right)$
13 0ss ${⊢}\varnothing \subseteq {A}{↑}_{𝑜}\varnothing$
14 13 a1i ${⊢}{A}\in \left(\mathrm{On}\setminus {2}_{𝑜}\right)\to \varnothing \subseteq {A}{↑}_{𝑜}\varnothing$
15 eloni ${⊢}{y}\in \mathrm{On}\to \mathrm{Ord}{y}$
16 eldifi ${⊢}{A}\in \left(\mathrm{On}\setminus {2}_{𝑜}\right)\to {A}\in \mathrm{On}$
17 oecl ${⊢}\left({A}\in \mathrm{On}\wedge {y}\in \mathrm{On}\right)\to {A}{↑}_{𝑜}{y}\in \mathrm{On}$
18 16 17 sylan ${⊢}\left({A}\in \left(\mathrm{On}\setminus {2}_{𝑜}\right)\wedge {y}\in \mathrm{On}\right)\to {A}{↑}_{𝑜}{y}\in \mathrm{On}$
19 eloni ${⊢}{A}{↑}_{𝑜}{y}\in \mathrm{On}\to \mathrm{Ord}\left({A}{↑}_{𝑜}{y}\right)$
20 18 19 syl ${⊢}\left({A}\in \left(\mathrm{On}\setminus {2}_{𝑜}\right)\wedge {y}\in \mathrm{On}\right)\to \mathrm{Ord}\left({A}{↑}_{𝑜}{y}\right)$
21 ordsucsssuc ${⊢}\left(\mathrm{Ord}{y}\wedge \mathrm{Ord}\left({A}{↑}_{𝑜}{y}\right)\right)\to \left({y}\subseteq {A}{↑}_{𝑜}{y}↔\mathrm{suc}{y}\subseteq \mathrm{suc}\left({A}{↑}_{𝑜}{y}\right)\right)$
22 15 20 21 syl2an2 ${⊢}\left({A}\in \left(\mathrm{On}\setminus {2}_{𝑜}\right)\wedge {y}\in \mathrm{On}\right)\to \left({y}\subseteq {A}{↑}_{𝑜}{y}↔\mathrm{suc}{y}\subseteq \mathrm{suc}\left({A}{↑}_{𝑜}{y}\right)\right)$
23 suceloni ${⊢}{y}\in \mathrm{On}\to \mathrm{suc}{y}\in \mathrm{On}$
24 oecl ${⊢}\left({A}\in \mathrm{On}\wedge \mathrm{suc}{y}\in \mathrm{On}\right)\to {A}{↑}_{𝑜}\mathrm{suc}{y}\in \mathrm{On}$
25 16 23 24 syl2an ${⊢}\left({A}\in \left(\mathrm{On}\setminus {2}_{𝑜}\right)\wedge {y}\in \mathrm{On}\right)\to {A}{↑}_{𝑜}\mathrm{suc}{y}\in \mathrm{On}$
26 eloni ${⊢}{A}{↑}_{𝑜}\mathrm{suc}{y}\in \mathrm{On}\to \mathrm{Ord}\left({A}{↑}_{𝑜}\mathrm{suc}{y}\right)$
27 25 26 syl ${⊢}\left({A}\in \left(\mathrm{On}\setminus {2}_{𝑜}\right)\wedge {y}\in \mathrm{On}\right)\to \mathrm{Ord}\left({A}{↑}_{𝑜}\mathrm{suc}{y}\right)$
28 id ${⊢}{A}\in \left(\mathrm{On}\setminus {2}_{𝑜}\right)\to {A}\in \left(\mathrm{On}\setminus {2}_{𝑜}\right)$
29 vex ${⊢}{y}\in \mathrm{V}$
30 29 sucid ${⊢}{y}\in \mathrm{suc}{y}$
31 oeordi ${⊢}\left(\mathrm{suc}{y}\in \mathrm{On}\wedge {A}\in \left(\mathrm{On}\setminus {2}_{𝑜}\right)\right)\to \left({y}\in \mathrm{suc}{y}\to {A}{↑}_{𝑜}{y}\in \left({A}{↑}_{𝑜}\mathrm{suc}{y}\right)\right)$
32 30 31 mpi ${⊢}\left(\mathrm{suc}{y}\in \mathrm{On}\wedge {A}\in \left(\mathrm{On}\setminus {2}_{𝑜}\right)\right)\to {A}{↑}_{𝑜}{y}\in \left({A}{↑}_{𝑜}\mathrm{suc}{y}\right)$
33 23 28 32 syl2anr ${⊢}\left({A}\in \left(\mathrm{On}\setminus {2}_{𝑜}\right)\wedge {y}\in \mathrm{On}\right)\to {A}{↑}_{𝑜}{y}\in \left({A}{↑}_{𝑜}\mathrm{suc}{y}\right)$
34 ordsucss ${⊢}\mathrm{Ord}\left({A}{↑}_{𝑜}\mathrm{suc}{y}\right)\to \left({A}{↑}_{𝑜}{y}\in \left({A}{↑}_{𝑜}\mathrm{suc}{y}\right)\to \mathrm{suc}\left({A}{↑}_{𝑜}{y}\right)\subseteq {A}{↑}_{𝑜}\mathrm{suc}{y}\right)$
35 27 33 34 sylc ${⊢}\left({A}\in \left(\mathrm{On}\setminus {2}_{𝑜}\right)\wedge {y}\in \mathrm{On}\right)\to \mathrm{suc}\left({A}{↑}_{𝑜}{y}\right)\subseteq {A}{↑}_{𝑜}\mathrm{suc}{y}$
36 sstr2 ${⊢}\mathrm{suc}{y}\subseteq \mathrm{suc}\left({A}{↑}_{𝑜}{y}\right)\to \left(\mathrm{suc}\left({A}{↑}_{𝑜}{y}\right)\subseteq {A}{↑}_{𝑜}\mathrm{suc}{y}\to \mathrm{suc}{y}\subseteq {A}{↑}_{𝑜}\mathrm{suc}{y}\right)$
37 35 36 syl5com ${⊢}\left({A}\in \left(\mathrm{On}\setminus {2}_{𝑜}\right)\wedge {y}\in \mathrm{On}\right)\to \left(\mathrm{suc}{y}\subseteq \mathrm{suc}\left({A}{↑}_{𝑜}{y}\right)\to \mathrm{suc}{y}\subseteq {A}{↑}_{𝑜}\mathrm{suc}{y}\right)$
38 22 37 sylbid ${⊢}\left({A}\in \left(\mathrm{On}\setminus {2}_{𝑜}\right)\wedge {y}\in \mathrm{On}\right)\to \left({y}\subseteq {A}{↑}_{𝑜}{y}\to \mathrm{suc}{y}\subseteq {A}{↑}_{𝑜}\mathrm{suc}{y}\right)$
39 38 expcom ${⊢}{y}\in \mathrm{On}\to \left({A}\in \left(\mathrm{On}\setminus {2}_{𝑜}\right)\to \left({y}\subseteq {A}{↑}_{𝑜}{y}\to \mathrm{suc}{y}\subseteq {A}{↑}_{𝑜}\mathrm{suc}{y}\right)\right)$
40 dif20el ${⊢}{A}\in \left(\mathrm{On}\setminus {2}_{𝑜}\right)\to \varnothing \in {A}$
41 16 40 jca ${⊢}{A}\in \left(\mathrm{On}\setminus {2}_{𝑜}\right)\to \left({A}\in \mathrm{On}\wedge \varnothing \in {A}\right)$
42 ss2iun ${⊢}\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{y}\subseteq {A}{↑}_{𝑜}{y}\to \bigcup _{{y}\in {x}}{y}\subseteq \bigcup _{{y}\in {x}}\left({A}{↑}_{𝑜}{y}\right)$
43 limuni ${⊢}\mathrm{Lim}{x}\to {x}=\bigcup {x}$
44 uniiun ${⊢}\bigcup {x}=\bigcup _{{y}\in {x}}{y}$
45 43 44 syl6eq ${⊢}\mathrm{Lim}{x}\to {x}=\bigcup _{{y}\in {x}}{y}$
46 45 adantr ${⊢}\left(\mathrm{Lim}{x}\wedge \left({A}\in \mathrm{On}\wedge \varnothing \in {A}\right)\right)\to {x}=\bigcup _{{y}\in {x}}{y}$
47 vex ${⊢}{x}\in \mathrm{V}$
48 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)$
49 47 48 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)$
50 49 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)$
51 50 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)$
52 46 51 sseq12d ${⊢}\left(\mathrm{Lim}{x}\wedge \left({A}\in \mathrm{On}\wedge \varnothing \in {A}\right)\right)\to \left({x}\subseteq {A}{↑}_{𝑜}{x}↔\bigcup _{{y}\in {x}}{y}\subseteq \bigcup _{{y}\in {x}}\left({A}{↑}_{𝑜}{y}\right)\right)$
53 42 52 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}}{y}\subseteq {A}{↑}_{𝑜}{y}\to {x}\subseteq {A}{↑}_{𝑜}{x}\right)$
54 53 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}}{y}\subseteq {A}{↑}_{𝑜}{y}\to {x}\subseteq {A}{↑}_{𝑜}{x}\right)\right)$
55 41 54 syl5 ${⊢}\mathrm{Lim}{x}\to \left({A}\in \left(\mathrm{On}\setminus {2}_{𝑜}\right)\to \left(\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{y}\subseteq {A}{↑}_{𝑜}{y}\to {x}\subseteq {A}{↑}_{𝑜}{x}\right)\right)$
56 3 6 9 12 14 39 55 tfinds3 ${⊢}{B}\in \mathrm{On}\to \left({A}\in \left(\mathrm{On}\setminus {2}_{𝑜}\right)\to {B}\subseteq {A}{↑}_{𝑜}{B}\right)$
57 56 impcom ${⊢}\left({A}\in \left(\mathrm{On}\setminus {2}_{𝑜}\right)\wedge {B}\in \mathrm{On}\right)\to {B}\subseteq {A}{↑}_{𝑜}{B}$