# Metamath Proof Explorer

## Theorem oeoelem

Description: Lemma for oeoe . (Contributed by Eric Schmidt, 26-May-2009)

Ref Expression
Hypotheses oeoelem.1 ${⊢}{A}\in \mathrm{On}$
oeoelem.2 ${⊢}\varnothing \in {A}$
Assertion oeoelem ${⊢}\left({B}\in \mathrm{On}\wedge {C}\in \mathrm{On}\right)\to \left({A}{↑}_{𝑜}{B}\right){↑}_{𝑜}{C}={A}{↑}_{𝑜}\left({B}{\cdot }_{𝑜}{C}\right)$

### Proof

Step Hyp Ref Expression
1 oeoelem.1 ${⊢}{A}\in \mathrm{On}$
2 oeoelem.2 ${⊢}\varnothing \in {A}$
3 oveq2 ${⊢}{x}=\varnothing \to \left({A}{↑}_{𝑜}{B}\right){↑}_{𝑜}{x}=\left({A}{↑}_{𝑜}{B}\right){↑}_{𝑜}\varnothing$
4 oveq2 ${⊢}{x}=\varnothing \to {B}{\cdot }_{𝑜}{x}={B}{\cdot }_{𝑜}\varnothing$
5 4 oveq2d ${⊢}{x}=\varnothing \to {A}{↑}_{𝑜}\left({B}{\cdot }_{𝑜}{x}\right)={A}{↑}_{𝑜}\left({B}{\cdot }_{𝑜}\varnothing \right)$
6 3 5 eqeq12d ${⊢}{x}=\varnothing \to \left(\left({A}{↑}_{𝑜}{B}\right){↑}_{𝑜}{x}={A}{↑}_{𝑜}\left({B}{\cdot }_{𝑜}{x}\right)↔\left({A}{↑}_{𝑜}{B}\right){↑}_{𝑜}\varnothing ={A}{↑}_{𝑜}\left({B}{\cdot }_{𝑜}\varnothing \right)\right)$
7 oveq2 ${⊢}{x}={y}\to \left({A}{↑}_{𝑜}{B}\right){↑}_{𝑜}{x}=\left({A}{↑}_{𝑜}{B}\right){↑}_{𝑜}{y}$
8 oveq2 ${⊢}{x}={y}\to {B}{\cdot }_{𝑜}{x}={B}{\cdot }_{𝑜}{y}$
9 8 oveq2d ${⊢}{x}={y}\to {A}{↑}_{𝑜}\left({B}{\cdot }_{𝑜}{x}\right)={A}{↑}_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)$
10 7 9 eqeq12d ${⊢}{x}={y}\to \left(\left({A}{↑}_{𝑜}{B}\right){↑}_{𝑜}{x}={A}{↑}_{𝑜}\left({B}{\cdot }_{𝑜}{x}\right)↔\left({A}{↑}_{𝑜}{B}\right){↑}_{𝑜}{y}={A}{↑}_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\right)$
11 oveq2 ${⊢}{x}=\mathrm{suc}{y}\to \left({A}{↑}_{𝑜}{B}\right){↑}_{𝑜}{x}=\left({A}{↑}_{𝑜}{B}\right){↑}_{𝑜}\mathrm{suc}{y}$
12 oveq2 ${⊢}{x}=\mathrm{suc}{y}\to {B}{\cdot }_{𝑜}{x}={B}{\cdot }_{𝑜}\mathrm{suc}{y}$
13 12 oveq2d ${⊢}{x}=\mathrm{suc}{y}\to {A}{↑}_{𝑜}\left({B}{\cdot }_{𝑜}{x}\right)={A}{↑}_{𝑜}\left({B}{\cdot }_{𝑜}\mathrm{suc}{y}\right)$
14 11 13 eqeq12d ${⊢}{x}=\mathrm{suc}{y}\to \left(\left({A}{↑}_{𝑜}{B}\right){↑}_{𝑜}{x}={A}{↑}_{𝑜}\left({B}{\cdot }_{𝑜}{x}\right)↔\left({A}{↑}_{𝑜}{B}\right){↑}_{𝑜}\mathrm{suc}{y}={A}{↑}_{𝑜}\left({B}{\cdot }_{𝑜}\mathrm{suc}{y}\right)\right)$
15 oveq2 ${⊢}{x}={C}\to \left({A}{↑}_{𝑜}{B}\right){↑}_{𝑜}{x}=\left({A}{↑}_{𝑜}{B}\right){↑}_{𝑜}{C}$
16 oveq2 ${⊢}{x}={C}\to {B}{\cdot }_{𝑜}{x}={B}{\cdot }_{𝑜}{C}$
17 16 oveq2d ${⊢}{x}={C}\to {A}{↑}_{𝑜}\left({B}{\cdot }_{𝑜}{x}\right)={A}{↑}_{𝑜}\left({B}{\cdot }_{𝑜}{C}\right)$
18 15 17 eqeq12d ${⊢}{x}={C}\to \left(\left({A}{↑}_{𝑜}{B}\right){↑}_{𝑜}{x}={A}{↑}_{𝑜}\left({B}{\cdot }_{𝑜}{x}\right)↔\left({A}{↑}_{𝑜}{B}\right){↑}_{𝑜}{C}={A}{↑}_{𝑜}\left({B}{\cdot }_{𝑜}{C}\right)\right)$
19 oecl ${⊢}\left({A}\in \mathrm{On}\wedge {B}\in \mathrm{On}\right)\to {A}{↑}_{𝑜}{B}\in \mathrm{On}$
20 1 19 mpan ${⊢}{B}\in \mathrm{On}\to {A}{↑}_{𝑜}{B}\in \mathrm{On}$
21 oe0 ${⊢}{A}{↑}_{𝑜}{B}\in \mathrm{On}\to \left({A}{↑}_{𝑜}{B}\right){↑}_{𝑜}\varnothing ={1}_{𝑜}$
22 20 21 syl ${⊢}{B}\in \mathrm{On}\to \left({A}{↑}_{𝑜}{B}\right){↑}_{𝑜}\varnothing ={1}_{𝑜}$
23 om0 ${⊢}{B}\in \mathrm{On}\to {B}{\cdot }_{𝑜}\varnothing =\varnothing$
24 23 oveq2d ${⊢}{B}\in \mathrm{On}\to {A}{↑}_{𝑜}\left({B}{\cdot }_{𝑜}\varnothing \right)={A}{↑}_{𝑜}\varnothing$
25 oe0 ${⊢}{A}\in \mathrm{On}\to {A}{↑}_{𝑜}\varnothing ={1}_{𝑜}$
26 1 25 ax-mp ${⊢}{A}{↑}_{𝑜}\varnothing ={1}_{𝑜}$
27 24 26 syl6eq ${⊢}{B}\in \mathrm{On}\to {A}{↑}_{𝑜}\left({B}{\cdot }_{𝑜}\varnothing \right)={1}_{𝑜}$
28 22 27 eqtr4d ${⊢}{B}\in \mathrm{On}\to \left({A}{↑}_{𝑜}{B}\right){↑}_{𝑜}\varnothing ={A}{↑}_{𝑜}\left({B}{\cdot }_{𝑜}\varnothing \right)$
29 oveq1 ${⊢}\left({A}{↑}_{𝑜}{B}\right){↑}_{𝑜}{y}={A}{↑}_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\to \left(\left({A}{↑}_{𝑜}{B}\right){↑}_{𝑜}{y}\right){\cdot }_{𝑜}\left({A}{↑}_{𝑜}{B}\right)=\left({A}{↑}_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\right){\cdot }_{𝑜}\left({A}{↑}_{𝑜}{B}\right)$
30 oesuc ${⊢}\left({A}{↑}_{𝑜}{B}\in \mathrm{On}\wedge {y}\in \mathrm{On}\right)\to \left({A}{↑}_{𝑜}{B}\right){↑}_{𝑜}\mathrm{suc}{y}=\left(\left({A}{↑}_{𝑜}{B}\right){↑}_{𝑜}{y}\right){\cdot }_{𝑜}\left({A}{↑}_{𝑜}{B}\right)$
31 20 30 sylan ${⊢}\left({B}\in \mathrm{On}\wedge {y}\in \mathrm{On}\right)\to \left({A}{↑}_{𝑜}{B}\right){↑}_{𝑜}\mathrm{suc}{y}=\left(\left({A}{↑}_{𝑜}{B}\right){↑}_{𝑜}{y}\right){\cdot }_{𝑜}\left({A}{↑}_{𝑜}{B}\right)$
32 omsuc ${⊢}\left({B}\in \mathrm{On}\wedge {y}\in \mathrm{On}\right)\to {B}{\cdot }_{𝑜}\mathrm{suc}{y}=\left({B}{\cdot }_{𝑜}{y}\right){+}_{𝑜}{B}$
33 32 oveq2d ${⊢}\left({B}\in \mathrm{On}\wedge {y}\in \mathrm{On}\right)\to {A}{↑}_{𝑜}\left({B}{\cdot }_{𝑜}\mathrm{suc}{y}\right)={A}{↑}_{𝑜}\left(\left({B}{\cdot }_{𝑜}{y}\right){+}_{𝑜}{B}\right)$
34 omcl ${⊢}\left({B}\in \mathrm{On}\wedge {y}\in \mathrm{On}\right)\to {B}{\cdot }_{𝑜}{y}\in \mathrm{On}$
35 oeoa ${⊢}\left({A}\in \mathrm{On}\wedge {B}{\cdot }_{𝑜}{y}\in \mathrm{On}\wedge {B}\in \mathrm{On}\right)\to {A}{↑}_{𝑜}\left(\left({B}{\cdot }_{𝑜}{y}\right){+}_{𝑜}{B}\right)=\left({A}{↑}_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\right){\cdot }_{𝑜}\left({A}{↑}_{𝑜}{B}\right)$
36 1 35 mp3an1 ${⊢}\left({B}{\cdot }_{𝑜}{y}\in \mathrm{On}\wedge {B}\in \mathrm{On}\right)\to {A}{↑}_{𝑜}\left(\left({B}{\cdot }_{𝑜}{y}\right){+}_{𝑜}{B}\right)=\left({A}{↑}_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\right){\cdot }_{𝑜}\left({A}{↑}_{𝑜}{B}\right)$
37 34 36 sylan ${⊢}\left(\left({B}\in \mathrm{On}\wedge {y}\in \mathrm{On}\right)\wedge {B}\in \mathrm{On}\right)\to {A}{↑}_{𝑜}\left(\left({B}{\cdot }_{𝑜}{y}\right){+}_{𝑜}{B}\right)=\left({A}{↑}_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\right){\cdot }_{𝑜}\left({A}{↑}_{𝑜}{B}\right)$
38 37 anabss1 ${⊢}\left({B}\in \mathrm{On}\wedge {y}\in \mathrm{On}\right)\to {A}{↑}_{𝑜}\left(\left({B}{\cdot }_{𝑜}{y}\right){+}_{𝑜}{B}\right)=\left({A}{↑}_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\right){\cdot }_{𝑜}\left({A}{↑}_{𝑜}{B}\right)$
39 33 38 eqtrd ${⊢}\left({B}\in \mathrm{On}\wedge {y}\in \mathrm{On}\right)\to {A}{↑}_{𝑜}\left({B}{\cdot }_{𝑜}\mathrm{suc}{y}\right)=\left({A}{↑}_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\right){\cdot }_{𝑜}\left({A}{↑}_{𝑜}{B}\right)$
40 31 39 eqeq12d ${⊢}\left({B}\in \mathrm{On}\wedge {y}\in \mathrm{On}\right)\to \left(\left({A}{↑}_{𝑜}{B}\right){↑}_{𝑜}\mathrm{suc}{y}={A}{↑}_{𝑜}\left({B}{\cdot }_{𝑜}\mathrm{suc}{y}\right)↔\left(\left({A}{↑}_{𝑜}{B}\right){↑}_{𝑜}{y}\right){\cdot }_{𝑜}\left({A}{↑}_{𝑜}{B}\right)=\left({A}{↑}_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\right){\cdot }_{𝑜}\left({A}{↑}_{𝑜}{B}\right)\right)$
41 29 40 syl5ibr ${⊢}\left({B}\in \mathrm{On}\wedge {y}\in \mathrm{On}\right)\to \left(\left({A}{↑}_{𝑜}{B}\right){↑}_{𝑜}{y}={A}{↑}_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\to \left({A}{↑}_{𝑜}{B}\right){↑}_{𝑜}\mathrm{suc}{y}={A}{↑}_{𝑜}\left({B}{\cdot }_{𝑜}\mathrm{suc}{y}\right)\right)$
42 41 expcom ${⊢}{y}\in \mathrm{On}\to \left({B}\in \mathrm{On}\to \left(\left({A}{↑}_{𝑜}{B}\right){↑}_{𝑜}{y}={A}{↑}_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\to \left({A}{↑}_{𝑜}{B}\right){↑}_{𝑜}\mathrm{suc}{y}={A}{↑}_{𝑜}\left({B}{\cdot }_{𝑜}\mathrm{suc}{y}\right)\right)\right)$
43 iuneq2 ${⊢}\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\left({A}{↑}_{𝑜}{B}\right){↑}_{𝑜}{y}={A}{↑}_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\to \bigcup _{{y}\in {x}}\left(\left({A}{↑}_{𝑜}{B}\right){↑}_{𝑜}{y}\right)=\bigcup _{{y}\in {x}}\left({A}{↑}_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\right)$
44 vex ${⊢}{x}\in \mathrm{V}$
45 oen0 ${⊢}\left(\left({A}\in \mathrm{On}\wedge {B}\in \mathrm{On}\right)\wedge \varnothing \in {A}\right)\to \varnothing \in \left({A}{↑}_{𝑜}{B}\right)$
46 2 45 mpan2 ${⊢}\left({A}\in \mathrm{On}\wedge {B}\in \mathrm{On}\right)\to \varnothing \in \left({A}{↑}_{𝑜}{B}\right)$
47 oelim ${⊢}\left(\left({A}{↑}_{𝑜}{B}\in \mathrm{On}\wedge \left({x}\in \mathrm{V}\wedge \mathrm{Lim}{x}\right)\right)\wedge \varnothing \in \left({A}{↑}_{𝑜}{B}\right)\right)\to \left({A}{↑}_{𝑜}{B}\right){↑}_{𝑜}{x}=\bigcup _{{y}\in {x}}\left(\left({A}{↑}_{𝑜}{B}\right){↑}_{𝑜}{y}\right)$
48 19 47 sylanl1 ${⊢}\left(\left(\left({A}\in \mathrm{On}\wedge {B}\in \mathrm{On}\right)\wedge \left({x}\in \mathrm{V}\wedge \mathrm{Lim}{x}\right)\right)\wedge \varnothing \in \left({A}{↑}_{𝑜}{B}\right)\right)\to \left({A}{↑}_{𝑜}{B}\right){↑}_{𝑜}{x}=\bigcup _{{y}\in {x}}\left(\left({A}{↑}_{𝑜}{B}\right){↑}_{𝑜}{y}\right)$
49 46 48 mpidan ${⊢}\left(\left({A}\in \mathrm{On}\wedge {B}\in \mathrm{On}\right)\wedge \left({x}\in \mathrm{V}\wedge \mathrm{Lim}{x}\right)\right)\to \left({A}{↑}_{𝑜}{B}\right){↑}_{𝑜}{x}=\bigcup _{{y}\in {x}}\left(\left({A}{↑}_{𝑜}{B}\right){↑}_{𝑜}{y}\right)$
50 1 49 mpanl1 ${⊢}\left({B}\in \mathrm{On}\wedge \left({x}\in \mathrm{V}\wedge \mathrm{Lim}{x}\right)\right)\to \left({A}{↑}_{𝑜}{B}\right){↑}_{𝑜}{x}=\bigcup _{{y}\in {x}}\left(\left({A}{↑}_{𝑜}{B}\right){↑}_{𝑜}{y}\right)$
51 44 50 mpanr1 ${⊢}\left({B}\in \mathrm{On}\wedge \mathrm{Lim}{x}\right)\to \left({A}{↑}_{𝑜}{B}\right){↑}_{𝑜}{x}=\bigcup _{{y}\in {x}}\left(\left({A}{↑}_{𝑜}{B}\right){↑}_{𝑜}{y}\right)$
52 omlim ${⊢}\left({B}\in \mathrm{On}\wedge \left({x}\in \mathrm{V}\wedge \mathrm{Lim}{x}\right)\right)\to {B}{\cdot }_{𝑜}{x}=\bigcup _{{y}\in {x}}\left({B}{\cdot }_{𝑜}{y}\right)$
53 44 52 mpanr1 ${⊢}\left({B}\in \mathrm{On}\wedge \mathrm{Lim}{x}\right)\to {B}{\cdot }_{𝑜}{x}=\bigcup _{{y}\in {x}}\left({B}{\cdot }_{𝑜}{y}\right)$
54 53 oveq2d ${⊢}\left({B}\in \mathrm{On}\wedge \mathrm{Lim}{x}\right)\to {A}{↑}_{𝑜}\left({B}{\cdot }_{𝑜}{x}\right)={A}{↑}_{𝑜}\bigcup _{{y}\in {x}}\left({B}{\cdot }_{𝑜}{y}\right)$
55 limord ${⊢}\mathrm{Lim}{x}\to \mathrm{Ord}{x}$
56 ordelon ${⊢}\left(\mathrm{Ord}{x}\wedge {y}\in {x}\right)\to {y}\in \mathrm{On}$
57 55 56 sylan ${⊢}\left(\mathrm{Lim}{x}\wedge {y}\in {x}\right)\to {y}\in \mathrm{On}$
58 57 34 sylan2 ${⊢}\left({B}\in \mathrm{On}\wedge \left(\mathrm{Lim}{x}\wedge {y}\in {x}\right)\right)\to {B}{\cdot }_{𝑜}{y}\in \mathrm{On}$
59 58 anassrs ${⊢}\left(\left({B}\in \mathrm{On}\wedge \mathrm{Lim}{x}\right)\wedge {y}\in {x}\right)\to {B}{\cdot }_{𝑜}{y}\in \mathrm{On}$
60 59 ralrimiva ${⊢}\left({B}\in \mathrm{On}\wedge \mathrm{Lim}{x}\right)\to \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{B}{\cdot }_{𝑜}{y}\in \mathrm{On}$
61 0ellim ${⊢}\mathrm{Lim}{x}\to \varnothing \in {x}$
62 61 ne0d ${⊢}\mathrm{Lim}{x}\to {x}\ne \varnothing$
63 62 adantl ${⊢}\left({B}\in \mathrm{On}\wedge \mathrm{Lim}{x}\right)\to {x}\ne \varnothing$
64 vex ${⊢}{w}\in \mathrm{V}$
65 oelim ${⊢}\left(\left({A}\in \mathrm{On}\wedge \left({w}\in \mathrm{V}\wedge \mathrm{Lim}{w}\right)\right)\wedge \varnothing \in {A}\right)\to {A}{↑}_{𝑜}{w}=\bigcup _{{z}\in {w}}\left({A}{↑}_{𝑜}{z}\right)$
66 2 65 mpan2 ${⊢}\left({A}\in \mathrm{On}\wedge \left({w}\in \mathrm{V}\wedge \mathrm{Lim}{w}\right)\right)\to {A}{↑}_{𝑜}{w}=\bigcup _{{z}\in {w}}\left({A}{↑}_{𝑜}{z}\right)$
67 1 66 mpan ${⊢}\left({w}\in \mathrm{V}\wedge \mathrm{Lim}{w}\right)\to {A}{↑}_{𝑜}{w}=\bigcup _{{z}\in {w}}\left({A}{↑}_{𝑜}{z}\right)$
68 64 67 mpan ${⊢}\mathrm{Lim}{w}\to {A}{↑}_{𝑜}{w}=\bigcup _{{z}\in {w}}\left({A}{↑}_{𝑜}{z}\right)$
69 oewordi ${⊢}\left(\left({z}\in \mathrm{On}\wedge {w}\in \mathrm{On}\wedge {A}\in \mathrm{On}\right)\wedge \varnothing \in {A}\right)\to \left({z}\subseteq {w}\to {A}{↑}_{𝑜}{z}\subseteq {A}{↑}_{𝑜}{w}\right)$
70 2 69 mpan2 ${⊢}\left({z}\in \mathrm{On}\wedge {w}\in \mathrm{On}\wedge {A}\in \mathrm{On}\right)\to \left({z}\subseteq {w}\to {A}{↑}_{𝑜}{z}\subseteq {A}{↑}_{𝑜}{w}\right)$
71 1 70 mp3an3 ${⊢}\left({z}\in \mathrm{On}\wedge {w}\in \mathrm{On}\right)\to \left({z}\subseteq {w}\to {A}{↑}_{𝑜}{z}\subseteq {A}{↑}_{𝑜}{w}\right)$
72 71 3impia ${⊢}\left({z}\in \mathrm{On}\wedge {w}\in \mathrm{On}\wedge {z}\subseteq {w}\right)\to {A}{↑}_{𝑜}{z}\subseteq {A}{↑}_{𝑜}{w}$
73 68 72 onoviun ${⊢}\left({x}\in \mathrm{V}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{B}{\cdot }_{𝑜}{y}\in \mathrm{On}\wedge {x}\ne \varnothing \right)\to {A}{↑}_{𝑜}\bigcup _{{y}\in {x}}\left({B}{\cdot }_{𝑜}{y}\right)=\bigcup _{{y}\in {x}}\left({A}{↑}_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\right)$
74 44 60 63 73 mp3an2i ${⊢}\left({B}\in \mathrm{On}\wedge \mathrm{Lim}{x}\right)\to {A}{↑}_{𝑜}\bigcup _{{y}\in {x}}\left({B}{\cdot }_{𝑜}{y}\right)=\bigcup _{{y}\in {x}}\left({A}{↑}_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\right)$
75 54 74 eqtrd ${⊢}\left({B}\in \mathrm{On}\wedge \mathrm{Lim}{x}\right)\to {A}{↑}_{𝑜}\left({B}{\cdot }_{𝑜}{x}\right)=\bigcup _{{y}\in {x}}\left({A}{↑}_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\right)$
76 51 75 eqeq12d ${⊢}\left({B}\in \mathrm{On}\wedge \mathrm{Lim}{x}\right)\to \left(\left({A}{↑}_{𝑜}{B}\right){↑}_{𝑜}{x}={A}{↑}_{𝑜}\left({B}{\cdot }_{𝑜}{x}\right)↔\bigcup _{{y}\in {x}}\left(\left({A}{↑}_{𝑜}{B}\right){↑}_{𝑜}{y}\right)=\bigcup _{{y}\in {x}}\left({A}{↑}_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\right)\right)$
77 43 76 syl5ibr ${⊢}\left({B}\in \mathrm{On}\wedge \mathrm{Lim}{x}\right)\to \left(\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\left({A}{↑}_{𝑜}{B}\right){↑}_{𝑜}{y}={A}{↑}_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\to \left({A}{↑}_{𝑜}{B}\right){↑}_{𝑜}{x}={A}{↑}_{𝑜}\left({B}{\cdot }_{𝑜}{x}\right)\right)$
78 77 expcom ${⊢}\mathrm{Lim}{x}\to \left({B}\in \mathrm{On}\to \left(\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\left({A}{↑}_{𝑜}{B}\right){↑}_{𝑜}{y}={A}{↑}_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\to \left({A}{↑}_{𝑜}{B}\right){↑}_{𝑜}{x}={A}{↑}_{𝑜}\left({B}{\cdot }_{𝑜}{x}\right)\right)\right)$
79 6 10 14 18 28 42 78 tfinds3 ${⊢}{C}\in \mathrm{On}\to \left({B}\in \mathrm{On}\to \left({A}{↑}_{𝑜}{B}\right){↑}_{𝑜}{C}={A}{↑}_{𝑜}\left({B}{\cdot }_{𝑜}{C}\right)\right)$
80 79 impcom ${⊢}\left({B}\in \mathrm{On}\wedge {C}\in \mathrm{On}\right)\to \left({A}{↑}_{𝑜}{B}\right){↑}_{𝑜}{C}={A}{↑}_{𝑜}\left({B}{\cdot }_{𝑜}{C}\right)$