# Metamath Proof Explorer

## Theorem omass

Description: Multiplication of ordinal numbers is associative. Theorem 8.26 of TakeutiZaring p. 65. (Contributed by NM, 28-Dec-2004)

Ref Expression
Assertion omass ${⊢}\left({A}\in \mathrm{On}\wedge {B}\in \mathrm{On}\wedge {C}\in \mathrm{On}\right)\to \left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}{C}={A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{C}\right)$

### Proof

Step Hyp Ref Expression
1 oveq2 ${⊢}{x}=\varnothing \to \left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}{x}=\left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}\varnothing$
2 oveq2 ${⊢}{x}=\varnothing \to {B}{\cdot }_{𝑜}{x}={B}{\cdot }_{𝑜}\varnothing$
3 2 oveq2d ${⊢}{x}=\varnothing \to {A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{x}\right)={A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}\varnothing \right)$
4 1 3 eqeq12d ${⊢}{x}=\varnothing \to \left(\left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}{x}={A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{x}\right)↔\left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}\varnothing ={A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}\varnothing \right)\right)$
5 oveq2 ${⊢}{x}={y}\to \left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}{x}=\left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}{y}$
6 oveq2 ${⊢}{x}={y}\to {B}{\cdot }_{𝑜}{x}={B}{\cdot }_{𝑜}{y}$
7 6 oveq2d ${⊢}{x}={y}\to {A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{x}\right)={A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)$
8 5 7 eqeq12d ${⊢}{x}={y}\to \left(\left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}{x}={A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{x}\right)↔\left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}{y}={A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\right)$
9 oveq2 ${⊢}{x}=\mathrm{suc}{y}\to \left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}{x}=\left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}\mathrm{suc}{y}$
10 oveq2 ${⊢}{x}=\mathrm{suc}{y}\to {B}{\cdot }_{𝑜}{x}={B}{\cdot }_{𝑜}\mathrm{suc}{y}$
11 10 oveq2d ${⊢}{x}=\mathrm{suc}{y}\to {A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{x}\right)={A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}\mathrm{suc}{y}\right)$
12 9 11 eqeq12d ${⊢}{x}=\mathrm{suc}{y}\to \left(\left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}{x}={A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{x}\right)↔\left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}\mathrm{suc}{y}={A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}\mathrm{suc}{y}\right)\right)$
13 oveq2 ${⊢}{x}={C}\to \left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}{x}=\left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}{C}$
14 oveq2 ${⊢}{x}={C}\to {B}{\cdot }_{𝑜}{x}={B}{\cdot }_{𝑜}{C}$
15 14 oveq2d ${⊢}{x}={C}\to {A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{x}\right)={A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{C}\right)$
16 13 15 eqeq12d ${⊢}{x}={C}\to \left(\left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}{x}={A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{x}\right)↔\left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}{C}={A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{C}\right)\right)$
17 omcl ${⊢}\left({A}\in \mathrm{On}\wedge {B}\in \mathrm{On}\right)\to {A}{\cdot }_{𝑜}{B}\in \mathrm{On}$
18 om0 ${⊢}{A}{\cdot }_{𝑜}{B}\in \mathrm{On}\to \left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}\varnothing =\varnothing$
19 17 18 syl ${⊢}\left({A}\in \mathrm{On}\wedge {B}\in \mathrm{On}\right)\to \left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}\varnothing =\varnothing$
20 om0 ${⊢}{B}\in \mathrm{On}\to {B}{\cdot }_{𝑜}\varnothing =\varnothing$
21 20 oveq2d ${⊢}{B}\in \mathrm{On}\to {A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}\varnothing \right)={A}{\cdot }_{𝑜}\varnothing$
22 om0 ${⊢}{A}\in \mathrm{On}\to {A}{\cdot }_{𝑜}\varnothing =\varnothing$
23 21 22 sylan9eqr ${⊢}\left({A}\in \mathrm{On}\wedge {B}\in \mathrm{On}\right)\to {A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}\varnothing \right)=\varnothing$
24 19 23 eqtr4d ${⊢}\left({A}\in \mathrm{On}\wedge {B}\in \mathrm{On}\right)\to \left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}\varnothing ={A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}\varnothing \right)$
25 oveq1 ${⊢}\left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}{y}={A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\to \left(\left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}{y}\right){+}_{𝑜}\left({A}{\cdot }_{𝑜}{B}\right)=\left({A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\right){+}_{𝑜}\left({A}{\cdot }_{𝑜}{B}\right)$
26 omsuc ${⊢}\left({A}{\cdot }_{𝑜}{B}\in \mathrm{On}\wedge {y}\in \mathrm{On}\right)\to \left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}\mathrm{suc}{y}=\left(\left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}{y}\right){+}_{𝑜}\left({A}{\cdot }_{𝑜}{B}\right)$
27 17 26 stoic3 ${⊢}\left({A}\in \mathrm{On}\wedge {B}\in \mathrm{On}\wedge {y}\in \mathrm{On}\right)\to \left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}\mathrm{suc}{y}=\left(\left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}{y}\right){+}_{𝑜}\left({A}{\cdot }_{𝑜}{B}\right)$
28 omsuc ${⊢}\left({B}\in \mathrm{On}\wedge {y}\in \mathrm{On}\right)\to {B}{\cdot }_{𝑜}\mathrm{suc}{y}=\left({B}{\cdot }_{𝑜}{y}\right){+}_{𝑜}{B}$
29 28 3adant1 ${⊢}\left({A}\in \mathrm{On}\wedge {B}\in \mathrm{On}\wedge {y}\in \mathrm{On}\right)\to {B}{\cdot }_{𝑜}\mathrm{suc}{y}=\left({B}{\cdot }_{𝑜}{y}\right){+}_{𝑜}{B}$
30 29 oveq2d ${⊢}\left({A}\in \mathrm{On}\wedge {B}\in \mathrm{On}\wedge {y}\in \mathrm{On}\right)\to {A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}\mathrm{suc}{y}\right)={A}{\cdot }_{𝑜}\left(\left({B}{\cdot }_{𝑜}{y}\right){+}_{𝑜}{B}\right)$
31 omcl ${⊢}\left({B}\in \mathrm{On}\wedge {y}\in \mathrm{On}\right)\to {B}{\cdot }_{𝑜}{y}\in \mathrm{On}$
32 odi ${⊢}\left({A}\in \mathrm{On}\wedge {B}{\cdot }_{𝑜}{y}\in \mathrm{On}\wedge {B}\in \mathrm{On}\right)\to {A}{\cdot }_{𝑜}\left(\left({B}{\cdot }_{𝑜}{y}\right){+}_{𝑜}{B}\right)=\left({A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\right){+}_{𝑜}\left({A}{\cdot }_{𝑜}{B}\right)$
33 31 32 syl3an2 ${⊢}\left({A}\in \mathrm{On}\wedge \left({B}\in \mathrm{On}\wedge {y}\in \mathrm{On}\right)\wedge {B}\in \mathrm{On}\right)\to {A}{\cdot }_{𝑜}\left(\left({B}{\cdot }_{𝑜}{y}\right){+}_{𝑜}{B}\right)=\left({A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\right){+}_{𝑜}\left({A}{\cdot }_{𝑜}{B}\right)$
34 33 3exp ${⊢}{A}\in \mathrm{On}\to \left(\left({B}\in \mathrm{On}\wedge {y}\in \mathrm{On}\right)\to \left({B}\in \mathrm{On}\to {A}{\cdot }_{𝑜}\left(\left({B}{\cdot }_{𝑜}{y}\right){+}_{𝑜}{B}\right)=\left({A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\right){+}_{𝑜}\left({A}{\cdot }_{𝑜}{B}\right)\right)\right)$
35 34 expd ${⊢}{A}\in \mathrm{On}\to \left({B}\in \mathrm{On}\to \left({y}\in \mathrm{On}\to \left({B}\in \mathrm{On}\to {A}{\cdot }_{𝑜}\left(\left({B}{\cdot }_{𝑜}{y}\right){+}_{𝑜}{B}\right)=\left({A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\right){+}_{𝑜}\left({A}{\cdot }_{𝑜}{B}\right)\right)\right)\right)$
36 35 com34 ${⊢}{A}\in \mathrm{On}\to \left({B}\in \mathrm{On}\to \left({B}\in \mathrm{On}\to \left({y}\in \mathrm{On}\to {A}{\cdot }_{𝑜}\left(\left({B}{\cdot }_{𝑜}{y}\right){+}_{𝑜}{B}\right)=\left({A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\right){+}_{𝑜}\left({A}{\cdot }_{𝑜}{B}\right)\right)\right)\right)$
37 36 pm2.43d ${⊢}{A}\in \mathrm{On}\to \left({B}\in \mathrm{On}\to \left({y}\in \mathrm{On}\to {A}{\cdot }_{𝑜}\left(\left({B}{\cdot }_{𝑜}{y}\right){+}_{𝑜}{B}\right)=\left({A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\right){+}_{𝑜}\left({A}{\cdot }_{𝑜}{B}\right)\right)\right)$
38 37 3imp ${⊢}\left({A}\in \mathrm{On}\wedge {B}\in \mathrm{On}\wedge {y}\in \mathrm{On}\right)\to {A}{\cdot }_{𝑜}\left(\left({B}{\cdot }_{𝑜}{y}\right){+}_{𝑜}{B}\right)=\left({A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\right){+}_{𝑜}\left({A}{\cdot }_{𝑜}{B}\right)$
39 30 38 eqtrd ${⊢}\left({A}\in \mathrm{On}\wedge {B}\in \mathrm{On}\wedge {y}\in \mathrm{On}\right)\to {A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}\mathrm{suc}{y}\right)=\left({A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\right){+}_{𝑜}\left({A}{\cdot }_{𝑜}{B}\right)$
40 27 39 eqeq12d ${⊢}\left({A}\in \mathrm{On}\wedge {B}\in \mathrm{On}\wedge {y}\in \mathrm{On}\right)\to \left(\left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}\mathrm{suc}{y}={A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}\mathrm{suc}{y}\right)↔\left(\left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}{y}\right){+}_{𝑜}\left({A}{\cdot }_{𝑜}{B}\right)=\left({A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\right){+}_{𝑜}\left({A}{\cdot }_{𝑜}{B}\right)\right)$
41 25 40 syl5ibr ${⊢}\left({A}\in \mathrm{On}\wedge {B}\in \mathrm{On}\wedge {y}\in \mathrm{On}\right)\to \left(\left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}{y}={A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\to \left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}\mathrm{suc}{y}={A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}\mathrm{suc}{y}\right)\right)$
42 41 3exp ${⊢}{A}\in \mathrm{On}\to \left({B}\in \mathrm{On}\to \left({y}\in \mathrm{On}\to \left(\left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}{y}={A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\to \left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}\mathrm{suc}{y}={A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}\mathrm{suc}{y}\right)\right)\right)\right)$
43 42 com3r ${⊢}{y}\in \mathrm{On}\to \left({A}\in \mathrm{On}\to \left({B}\in \mathrm{On}\to \left(\left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}{y}={A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\to \left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}\mathrm{suc}{y}={A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}\mathrm{suc}{y}\right)\right)\right)\right)$
44 43 impd ${⊢}{y}\in \mathrm{On}\to \left(\left({A}\in \mathrm{On}\wedge {B}\in \mathrm{On}\right)\to \left(\left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}{y}={A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\to \left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}\mathrm{suc}{y}={A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}\mathrm{suc}{y}\right)\right)\right)$
45 17 ancoms ${⊢}\left({B}\in \mathrm{On}\wedge {A}\in \mathrm{On}\right)\to {A}{\cdot }_{𝑜}{B}\in \mathrm{On}$
46 vex ${⊢}{x}\in \mathrm{V}$
47 omlim ${⊢}\left({A}{\cdot }_{𝑜}{B}\in \mathrm{On}\wedge \left({x}\in \mathrm{V}\wedge \mathrm{Lim}{x}\right)\right)\to \left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}{x}=\bigcup _{{y}\in {x}}\left(\left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}{y}\right)$
48 46 47 mpanr1 ${⊢}\left({A}{\cdot }_{𝑜}{B}\in \mathrm{On}\wedge \mathrm{Lim}{x}\right)\to \left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}{x}=\bigcup _{{y}\in {x}}\left(\left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}{y}\right)$
49 45 48 sylan ${⊢}\left(\left({B}\in \mathrm{On}\wedge {A}\in \mathrm{On}\right)\wedge \mathrm{Lim}{x}\right)\to \left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}{x}=\bigcup _{{y}\in {x}}\left(\left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}{y}\right)$
50 49 an32s ${⊢}\left(\left({B}\in \mathrm{On}\wedge \mathrm{Lim}{x}\right)\wedge {A}\in \mathrm{On}\right)\to \left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}{x}=\bigcup _{{y}\in {x}}\left(\left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}{y}\right)$
51 50 ad2antrr ${⊢}\left(\left(\left(\left({B}\in \mathrm{On}\wedge \mathrm{Lim}{x}\right)\wedge {A}\in \mathrm{On}\right)\wedge \varnothing \in {B}\right)\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}{y}={A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\right)\to \left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}{x}=\bigcup _{{y}\in {x}}\left(\left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}{y}\right)$
52 iuneq2 ${⊢}\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}{y}={A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\to \bigcup _{{y}\in {x}}\left(\left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}{y}\right)=\bigcup _{{y}\in {x}}\left({A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\right)$
53 limelon ${⊢}\left({x}\in \mathrm{V}\wedge \mathrm{Lim}{x}\right)\to {x}\in \mathrm{On}$
54 46 53 mpan ${⊢}\mathrm{Lim}{x}\to {x}\in \mathrm{On}$
55 54 anim1i ${⊢}\left(\mathrm{Lim}{x}\wedge {B}\in \mathrm{On}\right)\to \left({x}\in \mathrm{On}\wedge {B}\in \mathrm{On}\right)$
56 55 ancoms ${⊢}\left({B}\in \mathrm{On}\wedge \mathrm{Lim}{x}\right)\to \left({x}\in \mathrm{On}\wedge {B}\in \mathrm{On}\right)$
57 omordi ${⊢}\left(\left({x}\in \mathrm{On}\wedge {B}\in \mathrm{On}\right)\wedge \varnothing \in {B}\right)\to \left({y}\in {x}\to {B}{\cdot }_{𝑜}{y}\in \left({B}{\cdot }_{𝑜}{x}\right)\right)$
58 56 57 sylan ${⊢}\left(\left({B}\in \mathrm{On}\wedge \mathrm{Lim}{x}\right)\wedge \varnothing \in {B}\right)\to \left({y}\in {x}\to {B}{\cdot }_{𝑜}{y}\in \left({B}{\cdot }_{𝑜}{x}\right)\right)$
59 ssid ${⊢}{A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\subseteq {A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)$
60 oveq2 ${⊢}{z}={B}{\cdot }_{𝑜}{y}\to {A}{\cdot }_{𝑜}{z}={A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)$
61 60 sseq2d ${⊢}{z}={B}{\cdot }_{𝑜}{y}\to \left({A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\subseteq {A}{\cdot }_{𝑜}{z}↔{A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\subseteq {A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\right)$
62 61 rspcev ${⊢}\left({B}{\cdot }_{𝑜}{y}\in \left({B}{\cdot }_{𝑜}{x}\right)\wedge {A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\subseteq {A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\right)\to \exists {z}\in \left({B}{\cdot }_{𝑜}{x}\right)\phantom{\rule{.4em}{0ex}}{A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\subseteq {A}{\cdot }_{𝑜}{z}$
63 59 62 mpan2 ${⊢}{B}{\cdot }_{𝑜}{y}\in \left({B}{\cdot }_{𝑜}{x}\right)\to \exists {z}\in \left({B}{\cdot }_{𝑜}{x}\right)\phantom{\rule{.4em}{0ex}}{A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\subseteq {A}{\cdot }_{𝑜}{z}$
64 58 63 syl6 ${⊢}\left(\left({B}\in \mathrm{On}\wedge \mathrm{Lim}{x}\right)\wedge \varnothing \in {B}\right)\to \left({y}\in {x}\to \exists {z}\in \left({B}{\cdot }_{𝑜}{x}\right)\phantom{\rule{.4em}{0ex}}{A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\subseteq {A}{\cdot }_{𝑜}{z}\right)$
65 64 ralrimiv ${⊢}\left(\left({B}\in \mathrm{On}\wedge \mathrm{Lim}{x}\right)\wedge \varnothing \in {B}\right)\to \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {z}\in \left({B}{\cdot }_{𝑜}{x}\right)\phantom{\rule{.4em}{0ex}}{A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\subseteq {A}{\cdot }_{𝑜}{z}$
66 iunss2 ${⊢}\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {z}\in \left({B}{\cdot }_{𝑜}{x}\right)\phantom{\rule{.4em}{0ex}}{A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\subseteq {A}{\cdot }_{𝑜}{z}\to \bigcup _{{y}\in {x}}\left({A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\right)\subseteq \bigcup _{{z}\in {B}{\cdot }_{𝑜}{x}}\left({A}{\cdot }_{𝑜}{z}\right)$
67 65 66 syl ${⊢}\left(\left({B}\in \mathrm{On}\wedge \mathrm{Lim}{x}\right)\wedge \varnothing \in {B}\right)\to \bigcup _{{y}\in {x}}\left({A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\right)\subseteq \bigcup _{{z}\in {B}{\cdot }_{𝑜}{x}}\left({A}{\cdot }_{𝑜}{z}\right)$
68 67 adantlr ${⊢}\left(\left(\left({B}\in \mathrm{On}\wedge \mathrm{Lim}{x}\right)\wedge {A}\in \mathrm{On}\right)\wedge \varnothing \in {B}\right)\to \bigcup _{{y}\in {x}}\left({A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\right)\subseteq \bigcup _{{z}\in {B}{\cdot }_{𝑜}{x}}\left({A}{\cdot }_{𝑜}{z}\right)$
69 omcl ${⊢}\left({B}\in \mathrm{On}\wedge {x}\in \mathrm{On}\right)\to {B}{\cdot }_{𝑜}{x}\in \mathrm{On}$
70 54 69 sylan2 ${⊢}\left({B}\in \mathrm{On}\wedge \mathrm{Lim}{x}\right)\to {B}{\cdot }_{𝑜}{x}\in \mathrm{On}$
71 onelon ${⊢}\left({B}{\cdot }_{𝑜}{x}\in \mathrm{On}\wedge {z}\in \left({B}{\cdot }_{𝑜}{x}\right)\right)\to {z}\in \mathrm{On}$
72 70 71 sylan ${⊢}\left(\left({B}\in \mathrm{On}\wedge \mathrm{Lim}{x}\right)\wedge {z}\in \left({B}{\cdot }_{𝑜}{x}\right)\right)\to {z}\in \mathrm{On}$
73 72 adantlr ${⊢}\left(\left(\left({B}\in \mathrm{On}\wedge \mathrm{Lim}{x}\right)\wedge {A}\in \mathrm{On}\right)\wedge {z}\in \left({B}{\cdot }_{𝑜}{x}\right)\right)\to {z}\in \mathrm{On}$
74 omordlim ${⊢}\left(\left({B}\in \mathrm{On}\wedge \left({x}\in \mathrm{V}\wedge \mathrm{Lim}{x}\right)\right)\wedge {z}\in \left({B}{\cdot }_{𝑜}{x}\right)\right)\to \exists {y}\in {x}\phantom{\rule{.4em}{0ex}}{z}\in \left({B}{\cdot }_{𝑜}{y}\right)$
75 74 ex ${⊢}\left({B}\in \mathrm{On}\wedge \left({x}\in \mathrm{V}\wedge \mathrm{Lim}{x}\right)\right)\to \left({z}\in \left({B}{\cdot }_{𝑜}{x}\right)\to \exists {y}\in {x}\phantom{\rule{.4em}{0ex}}{z}\in \left({B}{\cdot }_{𝑜}{y}\right)\right)$
76 46 75 mpanr1 ${⊢}\left({B}\in \mathrm{On}\wedge \mathrm{Lim}{x}\right)\to \left({z}\in \left({B}{\cdot }_{𝑜}{x}\right)\to \exists {y}\in {x}\phantom{\rule{.4em}{0ex}}{z}\in \left({B}{\cdot }_{𝑜}{y}\right)\right)$
77 76 ad2antlr ${⊢}\left(\left({z}\in \mathrm{On}\wedge \left({B}\in \mathrm{On}\wedge \mathrm{Lim}{x}\right)\right)\wedge {A}\in \mathrm{On}\right)\to \left({z}\in \left({B}{\cdot }_{𝑜}{x}\right)\to \exists {y}\in {x}\phantom{\rule{.4em}{0ex}}{z}\in \left({B}{\cdot }_{𝑜}{y}\right)\right)$
78 onelon ${⊢}\left({x}\in \mathrm{On}\wedge {y}\in {x}\right)\to {y}\in \mathrm{On}$
79 54 78 sylan ${⊢}\left(\mathrm{Lim}{x}\wedge {y}\in {x}\right)\to {y}\in \mathrm{On}$
80 79 31 sylan2 ${⊢}\left({B}\in \mathrm{On}\wedge \left(\mathrm{Lim}{x}\wedge {y}\in {x}\right)\right)\to {B}{\cdot }_{𝑜}{y}\in \mathrm{On}$
81 onelss ${⊢}{B}{\cdot }_{𝑜}{y}\in \mathrm{On}\to \left({z}\in \left({B}{\cdot }_{𝑜}{y}\right)\to {z}\subseteq {B}{\cdot }_{𝑜}{y}\right)$
82 81 3ad2ant2 ${⊢}\left({z}\in \mathrm{On}\wedge {B}{\cdot }_{𝑜}{y}\in \mathrm{On}\wedge {A}\in \mathrm{On}\right)\to \left({z}\in \left({B}{\cdot }_{𝑜}{y}\right)\to {z}\subseteq {B}{\cdot }_{𝑜}{y}\right)$
83 omwordi ${⊢}\left({z}\in \mathrm{On}\wedge {B}{\cdot }_{𝑜}{y}\in \mathrm{On}\wedge {A}\in \mathrm{On}\right)\to \left({z}\subseteq {B}{\cdot }_{𝑜}{y}\to {A}{\cdot }_{𝑜}{z}\subseteq {A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\right)$
84 82 83 syld ${⊢}\left({z}\in \mathrm{On}\wedge {B}{\cdot }_{𝑜}{y}\in \mathrm{On}\wedge {A}\in \mathrm{On}\right)\to \left({z}\in \left({B}{\cdot }_{𝑜}{y}\right)\to {A}{\cdot }_{𝑜}{z}\subseteq {A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\right)$
85 84 3exp ${⊢}{z}\in \mathrm{On}\to \left({B}{\cdot }_{𝑜}{y}\in \mathrm{On}\to \left({A}\in \mathrm{On}\to \left({z}\in \left({B}{\cdot }_{𝑜}{y}\right)\to {A}{\cdot }_{𝑜}{z}\subseteq {A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\right)\right)\right)$
86 80 85 syl5 ${⊢}{z}\in \mathrm{On}\to \left(\left({B}\in \mathrm{On}\wedge \left(\mathrm{Lim}{x}\wedge {y}\in {x}\right)\right)\to \left({A}\in \mathrm{On}\to \left({z}\in \left({B}{\cdot }_{𝑜}{y}\right)\to {A}{\cdot }_{𝑜}{z}\subseteq {A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\right)\right)\right)$
87 86 exp4d ${⊢}{z}\in \mathrm{On}\to \left({B}\in \mathrm{On}\to \left(\mathrm{Lim}{x}\to \left({y}\in {x}\to \left({A}\in \mathrm{On}\to \left({z}\in \left({B}{\cdot }_{𝑜}{y}\right)\to {A}{\cdot }_{𝑜}{z}\subseteq {A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\right)\right)\right)\right)\right)$
88 87 imp32 ${⊢}\left({z}\in \mathrm{On}\wedge \left({B}\in \mathrm{On}\wedge \mathrm{Lim}{x}\right)\right)\to \left({y}\in {x}\to \left({A}\in \mathrm{On}\to \left({z}\in \left({B}{\cdot }_{𝑜}{y}\right)\to {A}{\cdot }_{𝑜}{z}\subseteq {A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\right)\right)\right)$
89 88 com23 ${⊢}\left({z}\in \mathrm{On}\wedge \left({B}\in \mathrm{On}\wedge \mathrm{Lim}{x}\right)\right)\to \left({A}\in \mathrm{On}\to \left({y}\in {x}\to \left({z}\in \left({B}{\cdot }_{𝑜}{y}\right)\to {A}{\cdot }_{𝑜}{z}\subseteq {A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\right)\right)\right)$
90 89 imp ${⊢}\left(\left({z}\in \mathrm{On}\wedge \left({B}\in \mathrm{On}\wedge \mathrm{Lim}{x}\right)\right)\wedge {A}\in \mathrm{On}\right)\to \left({y}\in {x}\to \left({z}\in \left({B}{\cdot }_{𝑜}{y}\right)\to {A}{\cdot }_{𝑜}{z}\subseteq {A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\right)\right)$
91 90 reximdvai ${⊢}\left(\left({z}\in \mathrm{On}\wedge \left({B}\in \mathrm{On}\wedge \mathrm{Lim}{x}\right)\right)\wedge {A}\in \mathrm{On}\right)\to \left(\exists {y}\in {x}\phantom{\rule{.4em}{0ex}}{z}\in \left({B}{\cdot }_{𝑜}{y}\right)\to \exists {y}\in {x}\phantom{\rule{.4em}{0ex}}{A}{\cdot }_{𝑜}{z}\subseteq {A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\right)$
92 77 91 syld ${⊢}\left(\left({z}\in \mathrm{On}\wedge \left({B}\in \mathrm{On}\wedge \mathrm{Lim}{x}\right)\right)\wedge {A}\in \mathrm{On}\right)\to \left({z}\in \left({B}{\cdot }_{𝑜}{x}\right)\to \exists {y}\in {x}\phantom{\rule{.4em}{0ex}}{A}{\cdot }_{𝑜}{z}\subseteq {A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\right)$
93 92 exp31 ${⊢}{z}\in \mathrm{On}\to \left(\left({B}\in \mathrm{On}\wedge \mathrm{Lim}{x}\right)\to \left({A}\in \mathrm{On}\to \left({z}\in \left({B}{\cdot }_{𝑜}{x}\right)\to \exists {y}\in {x}\phantom{\rule{.4em}{0ex}}{A}{\cdot }_{𝑜}{z}\subseteq {A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\right)\right)\right)$
94 93 imp4c ${⊢}{z}\in \mathrm{On}\to \left(\left(\left(\left({B}\in \mathrm{On}\wedge \mathrm{Lim}{x}\right)\wedge {A}\in \mathrm{On}\right)\wedge {z}\in \left({B}{\cdot }_{𝑜}{x}\right)\right)\to \exists {y}\in {x}\phantom{\rule{.4em}{0ex}}{A}{\cdot }_{𝑜}{z}\subseteq {A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\right)$
95 73 94 mpcom ${⊢}\left(\left(\left({B}\in \mathrm{On}\wedge \mathrm{Lim}{x}\right)\wedge {A}\in \mathrm{On}\right)\wedge {z}\in \left({B}{\cdot }_{𝑜}{x}\right)\right)\to \exists {y}\in {x}\phantom{\rule{.4em}{0ex}}{A}{\cdot }_{𝑜}{z}\subseteq {A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)$
96 95 ralrimiva ${⊢}\left(\left({B}\in \mathrm{On}\wedge \mathrm{Lim}{x}\right)\wedge {A}\in \mathrm{On}\right)\to \forall {z}\in \left({B}{\cdot }_{𝑜}{x}\right)\phantom{\rule{.4em}{0ex}}\exists {y}\in {x}\phantom{\rule{.4em}{0ex}}{A}{\cdot }_{𝑜}{z}\subseteq {A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)$
97 iunss2 ${⊢}\forall {z}\in \left({B}{\cdot }_{𝑜}{x}\right)\phantom{\rule{.4em}{0ex}}\exists {y}\in {x}\phantom{\rule{.4em}{0ex}}{A}{\cdot }_{𝑜}{z}\subseteq {A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\to \bigcup _{{z}\in {B}{\cdot }_{𝑜}{x}}\left({A}{\cdot }_{𝑜}{z}\right)\subseteq \bigcup _{{y}\in {x}}\left({A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\right)$
98 96 97 syl ${⊢}\left(\left({B}\in \mathrm{On}\wedge \mathrm{Lim}{x}\right)\wedge {A}\in \mathrm{On}\right)\to \bigcup _{{z}\in {B}{\cdot }_{𝑜}{x}}\left({A}{\cdot }_{𝑜}{z}\right)\subseteq \bigcup _{{y}\in {x}}\left({A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\right)$
99 98 adantr ${⊢}\left(\left(\left({B}\in \mathrm{On}\wedge \mathrm{Lim}{x}\right)\wedge {A}\in \mathrm{On}\right)\wedge \varnothing \in {B}\right)\to \bigcup _{{z}\in {B}{\cdot }_{𝑜}{x}}\left({A}{\cdot }_{𝑜}{z}\right)\subseteq \bigcup _{{y}\in {x}}\left({A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\right)$
100 68 99 eqssd ${⊢}\left(\left(\left({B}\in \mathrm{On}\wedge \mathrm{Lim}{x}\right)\wedge {A}\in \mathrm{On}\right)\wedge \varnothing \in {B}\right)\to \bigcup _{{y}\in {x}}\left({A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\right)=\bigcup _{{z}\in {B}{\cdot }_{𝑜}{x}}\left({A}{\cdot }_{𝑜}{z}\right)$
101 omlimcl ${⊢}\left(\left({B}\in \mathrm{On}\wedge \left({x}\in \mathrm{V}\wedge \mathrm{Lim}{x}\right)\right)\wedge \varnothing \in {B}\right)\to \mathrm{Lim}\left({B}{\cdot }_{𝑜}{x}\right)$
102 46 101 mpanlr1 ${⊢}\left(\left({B}\in \mathrm{On}\wedge \mathrm{Lim}{x}\right)\wedge \varnothing \in {B}\right)\to \mathrm{Lim}\left({B}{\cdot }_{𝑜}{x}\right)$
103 ovex ${⊢}{B}{\cdot }_{𝑜}{x}\in \mathrm{V}$
104 omlim ${⊢}\left({A}\in \mathrm{On}\wedge \left({B}{\cdot }_{𝑜}{x}\in \mathrm{V}\wedge \mathrm{Lim}\left({B}{\cdot }_{𝑜}{x}\right)\right)\right)\to {A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{x}\right)=\bigcup _{{z}\in {B}{\cdot }_{𝑜}{x}}\left({A}{\cdot }_{𝑜}{z}\right)$
105 103 104 mpanr1 ${⊢}\left({A}\in \mathrm{On}\wedge \mathrm{Lim}\left({B}{\cdot }_{𝑜}{x}\right)\right)\to {A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{x}\right)=\bigcup _{{z}\in {B}{\cdot }_{𝑜}{x}}\left({A}{\cdot }_{𝑜}{z}\right)$
106 102 105 sylan2 ${⊢}\left({A}\in \mathrm{On}\wedge \left(\left({B}\in \mathrm{On}\wedge \mathrm{Lim}{x}\right)\wedge \varnothing \in {B}\right)\right)\to {A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{x}\right)=\bigcup _{{z}\in {B}{\cdot }_{𝑜}{x}}\left({A}{\cdot }_{𝑜}{z}\right)$
107 106 ancoms ${⊢}\left(\left(\left({B}\in \mathrm{On}\wedge \mathrm{Lim}{x}\right)\wedge \varnothing \in {B}\right)\wedge {A}\in \mathrm{On}\right)\to {A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{x}\right)=\bigcup _{{z}\in {B}{\cdot }_{𝑜}{x}}\left({A}{\cdot }_{𝑜}{z}\right)$
108 107 an32s ${⊢}\left(\left(\left({B}\in \mathrm{On}\wedge \mathrm{Lim}{x}\right)\wedge {A}\in \mathrm{On}\right)\wedge \varnothing \in {B}\right)\to {A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{x}\right)=\bigcup _{{z}\in {B}{\cdot }_{𝑜}{x}}\left({A}{\cdot }_{𝑜}{z}\right)$
109 100 108 eqtr4d ${⊢}\left(\left(\left({B}\in \mathrm{On}\wedge \mathrm{Lim}{x}\right)\wedge {A}\in \mathrm{On}\right)\wedge \varnothing \in {B}\right)\to \bigcup _{{y}\in {x}}\left({A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\right)={A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{x}\right)$
110 52 109 sylan9eqr ${⊢}\left(\left(\left(\left({B}\in \mathrm{On}\wedge \mathrm{Lim}{x}\right)\wedge {A}\in \mathrm{On}\right)\wedge \varnothing \in {B}\right)\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}{y}={A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\right)\to \bigcup _{{y}\in {x}}\left(\left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}{y}\right)={A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{x}\right)$
111 51 110 eqtrd ${⊢}\left(\left(\left(\left({B}\in \mathrm{On}\wedge \mathrm{Lim}{x}\right)\wedge {A}\in \mathrm{On}\right)\wedge \varnothing \in {B}\right)\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}{y}={A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\right)\to \left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}{x}={A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{x}\right)$
112 111 exp31 ${⊢}\left(\left({B}\in \mathrm{On}\wedge \mathrm{Lim}{x}\right)\wedge {A}\in \mathrm{On}\right)\to \left(\varnothing \in {B}\to \left(\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}{y}={A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\to \left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}{x}={A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{x}\right)\right)\right)$
113 eloni ${⊢}{B}\in \mathrm{On}\to \mathrm{Ord}{B}$
114 ord0eln0 ${⊢}\mathrm{Ord}{B}\to \left(\varnothing \in {B}↔{B}\ne \varnothing \right)$
115 114 necon2bbid ${⊢}\mathrm{Ord}{B}\to \left({B}=\varnothing ↔¬\varnothing \in {B}\right)$
116 113 115 syl ${⊢}{B}\in \mathrm{On}\to \left({B}=\varnothing ↔¬\varnothing \in {B}\right)$
117 116 ad2antrr ${⊢}\left(\left({B}\in \mathrm{On}\wedge \mathrm{Lim}{x}\right)\wedge {A}\in \mathrm{On}\right)\to \left({B}=\varnothing ↔¬\varnothing \in {B}\right)$
118 oveq2 ${⊢}{B}=\varnothing \to {A}{\cdot }_{𝑜}{B}={A}{\cdot }_{𝑜}\varnothing$
119 118 22 sylan9eqr ${⊢}\left({A}\in \mathrm{On}\wedge {B}=\varnothing \right)\to {A}{\cdot }_{𝑜}{B}=\varnothing$
120 119 oveq1d ${⊢}\left({A}\in \mathrm{On}\wedge {B}=\varnothing \right)\to \left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}{x}=\varnothing {\cdot }_{𝑜}{x}$
121 om0r ${⊢}{x}\in \mathrm{On}\to \varnothing {\cdot }_{𝑜}{x}=\varnothing$
122 120 121 sylan9eqr ${⊢}\left({x}\in \mathrm{On}\wedge \left({A}\in \mathrm{On}\wedge {B}=\varnothing \right)\right)\to \left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}{x}=\varnothing$
123 122 anassrs ${⊢}\left(\left({x}\in \mathrm{On}\wedge {A}\in \mathrm{On}\right)\wedge {B}=\varnothing \right)\to \left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}{x}=\varnothing$
124 oveq1 ${⊢}{B}=\varnothing \to {B}{\cdot }_{𝑜}{x}=\varnothing {\cdot }_{𝑜}{x}$
125 124 121 sylan9eqr ${⊢}\left({x}\in \mathrm{On}\wedge {B}=\varnothing \right)\to {B}{\cdot }_{𝑜}{x}=\varnothing$
126 125 oveq2d ${⊢}\left({x}\in \mathrm{On}\wedge {B}=\varnothing \right)\to {A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{x}\right)={A}{\cdot }_{𝑜}\varnothing$
127 126 22 sylan9eq ${⊢}\left(\left({x}\in \mathrm{On}\wedge {B}=\varnothing \right)\wedge {A}\in \mathrm{On}\right)\to {A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{x}\right)=\varnothing$
128 127 an32s ${⊢}\left(\left({x}\in \mathrm{On}\wedge {A}\in \mathrm{On}\right)\wedge {B}=\varnothing \right)\to {A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{x}\right)=\varnothing$
129 123 128 eqtr4d ${⊢}\left(\left({x}\in \mathrm{On}\wedge {A}\in \mathrm{On}\right)\wedge {B}=\varnothing \right)\to \left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}{x}={A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{x}\right)$
130 129 ex ${⊢}\left({x}\in \mathrm{On}\wedge {A}\in \mathrm{On}\right)\to \left({B}=\varnothing \to \left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}{x}={A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{x}\right)\right)$
131 54 130 sylan ${⊢}\left(\mathrm{Lim}{x}\wedge {A}\in \mathrm{On}\right)\to \left({B}=\varnothing \to \left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}{x}={A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{x}\right)\right)$
132 131 adantll ${⊢}\left(\left({B}\in \mathrm{On}\wedge \mathrm{Lim}{x}\right)\wedge {A}\in \mathrm{On}\right)\to \left({B}=\varnothing \to \left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}{x}={A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{x}\right)\right)$
133 117 132 sylbird ${⊢}\left(\left({B}\in \mathrm{On}\wedge \mathrm{Lim}{x}\right)\wedge {A}\in \mathrm{On}\right)\to \left(¬\varnothing \in {B}\to \left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}{x}={A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{x}\right)\right)$
134 133 a1dd ${⊢}\left(\left({B}\in \mathrm{On}\wedge \mathrm{Lim}{x}\right)\wedge {A}\in \mathrm{On}\right)\to \left(¬\varnothing \in {B}\to \left(\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}{y}={A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\to \left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}{x}={A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{x}\right)\right)\right)$
135 112 134 pm2.61d ${⊢}\left(\left({B}\in \mathrm{On}\wedge \mathrm{Lim}{x}\right)\wedge {A}\in \mathrm{On}\right)\to \left(\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}{y}={A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\to \left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}{x}={A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{x}\right)\right)$
136 135 exp31 ${⊢}{B}\in \mathrm{On}\to \left(\mathrm{Lim}{x}\to \left({A}\in \mathrm{On}\to \left(\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}{y}={A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\to \left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}{x}={A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{x}\right)\right)\right)\right)$
137 136 com3l ${⊢}\mathrm{Lim}{x}\to \left({A}\in \mathrm{On}\to \left({B}\in \mathrm{On}\to \left(\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}{y}={A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\to \left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}{x}={A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{x}\right)\right)\right)\right)$
138 137 impd ${⊢}\mathrm{Lim}{x}\to \left(\left({A}\in \mathrm{On}\wedge {B}\in \mathrm{On}\right)\to \left(\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}{y}={A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{y}\right)\to \left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}{x}={A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{x}\right)\right)\right)$
139 4 8 12 16 24 44 138 tfinds3 ${⊢}{C}\in \mathrm{On}\to \left(\left({A}\in \mathrm{On}\wedge {B}\in \mathrm{On}\right)\to \left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}{C}={A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{C}\right)\right)$
140 139 expd ${⊢}{C}\in \mathrm{On}\to \left({A}\in \mathrm{On}\to \left({B}\in \mathrm{On}\to \left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}{C}={A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{C}\right)\right)\right)$
141 140 com3l ${⊢}{A}\in \mathrm{On}\to \left({B}\in \mathrm{On}\to \left({C}\in \mathrm{On}\to \left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}{C}={A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{C}\right)\right)\right)$
142 141 3imp ${⊢}\left({A}\in \mathrm{On}\wedge {B}\in \mathrm{On}\wedge {C}\in \mathrm{On}\right)\to \left({A}{\cdot }_{𝑜}{B}\right){\cdot }_{𝑜}{C}={A}{\cdot }_{𝑜}\left({B}{\cdot }_{𝑜}{C}\right)$