Metamath Proof Explorer

Theorem oeoalem

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

Ref Expression
Hypotheses oeoalem.1 ⊢ 𝐴 ∈ On
oeoalem.2 ⊢ ∅ ∈ 𝐴
oeoalem.3 ⊢ 𝐵 ∈ On
Assertion oeoalem ( 𝐶 ∈ On → ( 𝐴 ↑o ( 𝐵 +o 𝐶 ) ) = ( ( 𝐴 ↑o 𝐵 ) ·o ( 𝐴 ↑o 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 oeoalem.1 ⊢ 𝐴 ∈ On
2 oeoalem.2 ⊢ ∅ ∈ 𝐴
3 oeoalem.3 ⊢ 𝐵 ∈ On
4 oveq2 ⊢ ( 𝑥 = ∅ → ( 𝐵 +o 𝑥 ) = ( 𝐵 +o ∅ ) )
5 4 oveq2d ⊢ ( 𝑥 = ∅ → ( 𝐴 ↑o ( 𝐵 +o 𝑥 ) ) = ( 𝐴 ↑o ( 𝐵 +o ∅ ) ) )
6 oveq2 ⊢ ( 𝑥 = ∅ → ( 𝐴 ↑o 𝑥 ) = ( 𝐴 ↑o ∅ ) )
7 6 oveq2d ⊢ ( 𝑥 = ∅ → ( ( 𝐴 ↑o 𝐵 ) ·o ( 𝐴 ↑o 𝑥 ) ) = ( ( 𝐴 ↑o 𝐵 ) ·o ( 𝐴 ↑o ∅ ) ) )
8 5 7 eqeq12d ⊢ ( 𝑥 = ∅ → ( ( 𝐴 ↑o ( 𝐵 +o 𝑥 ) ) = ( ( 𝐴 ↑o 𝐵 ) ·o ( 𝐴 ↑o 𝑥 ) ) ↔ ( 𝐴 ↑o ( 𝐵 +o ∅ ) ) = ( ( 𝐴 ↑o 𝐵 ) ·o ( 𝐴 ↑o ∅ ) ) ) )
9 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐵 +o 𝑥 ) = ( 𝐵 +o 𝑦 ) )
10 9 oveq2d ⊢ ( 𝑥 = 𝑦 → ( 𝐴 ↑o ( 𝐵 +o 𝑥 ) ) = ( 𝐴 ↑o ( 𝐵 +o 𝑦 ) ) )
11 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐴 ↑o 𝑥 ) = ( 𝐴 ↑o 𝑦 ) )
12 11 oveq2d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐴 ↑o 𝐵 ) ·o ( 𝐴 ↑o 𝑥 ) ) = ( ( 𝐴 ↑o 𝐵 ) ·o ( 𝐴 ↑o 𝑦 ) ) )
13 10 12 eqeq12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐴 ↑o ( 𝐵 +o 𝑥 ) ) = ( ( 𝐴 ↑o 𝐵 ) ·o ( 𝐴 ↑o 𝑥 ) ) ↔ ( 𝐴 ↑o ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ↑o 𝐵 ) ·o ( 𝐴 ↑o 𝑦 ) ) ) )
14 oveq2 ⊢ ( 𝑥 = suc 𝑦 → ( 𝐵 +o 𝑥 ) = ( 𝐵 +o suc 𝑦 ) )
15 14 oveq2d ⊢ ( 𝑥 = suc 𝑦 → ( 𝐴 ↑o ( 𝐵 +o 𝑥 ) ) = ( 𝐴 ↑o ( 𝐵 +o suc 𝑦 ) ) )
16 oveq2 ⊢ ( 𝑥 = suc 𝑦 → ( 𝐴 ↑o 𝑥 ) = ( 𝐴 ↑o suc 𝑦 ) )
17 16 oveq2d ⊢ ( 𝑥 = suc 𝑦 → ( ( 𝐴 ↑o 𝐵 ) ·o ( 𝐴 ↑o 𝑥 ) ) = ( ( 𝐴 ↑o 𝐵 ) ·o ( 𝐴 ↑o suc 𝑦 ) ) )
18 15 17 eqeq12d ⊢ ( 𝑥 = suc 𝑦 → ( ( 𝐴 ↑o ( 𝐵 +o 𝑥 ) ) = ( ( 𝐴 ↑o 𝐵 ) ·o ( 𝐴 ↑o 𝑥 ) ) ↔ ( 𝐴 ↑o ( 𝐵 +o suc 𝑦 ) ) = ( ( 𝐴 ↑o 𝐵 ) ·o ( 𝐴 ↑o suc 𝑦 ) ) ) )
19 oveq2 ⊢ ( 𝑥 = 𝐶 → ( 𝐵 +o 𝑥 ) = ( 𝐵 +o 𝐶 ) )
20 19 oveq2d ⊢ ( 𝑥 = 𝐶 → ( 𝐴 ↑o ( 𝐵 +o 𝑥 ) ) = ( 𝐴 ↑o ( 𝐵 +o 𝐶 ) ) )
21 oveq2 ⊢ ( 𝑥 = 𝐶 → ( 𝐴 ↑o 𝑥 ) = ( 𝐴 ↑o 𝐶 ) )
22 21 oveq2d ⊢ ( 𝑥 = 𝐶 → ( ( 𝐴 ↑o 𝐵 ) ·o ( 𝐴 ↑o 𝑥 ) ) = ( ( 𝐴 ↑o 𝐵 ) ·o ( 𝐴 ↑o 𝐶 ) ) )
23 20 22 eqeq12d ⊢ ( 𝑥 = 𝐶 → ( ( 𝐴 ↑o ( 𝐵 +o 𝑥 ) ) = ( ( 𝐴 ↑o 𝐵 ) ·o ( 𝐴 ↑o 𝑥 ) ) ↔ ( 𝐴 ↑o ( 𝐵 +o 𝐶 ) ) = ( ( 𝐴 ↑o 𝐵 ) ·o ( 𝐴 ↑o 𝐶 ) ) ) )
24 oecl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ↑o 𝐵 ) ∈ On )
25 1 3 24 mp2an ⊢ ( 𝐴 ↑o 𝐵 ) ∈ On
26 om1 ⊢ ( ( 𝐴 ↑o 𝐵 ) ∈ On → ( ( 𝐴 ↑o 𝐵 ) ·o 1o ) = ( 𝐴 ↑o 𝐵 ) )
27 25 26 ax-mp ⊢ ( ( 𝐴 ↑o 𝐵 ) ·o 1o ) = ( 𝐴 ↑o 𝐵 )
28 oe0 ⊢ ( 𝐴 ∈ On → ( 𝐴 ↑o ∅ ) = 1o )
29 1 28 ax-mp ⊢ ( 𝐴 ↑o ∅ ) = 1o
30 29 oveq2i ⊢ ( ( 𝐴 ↑o 𝐵 ) ·o ( 𝐴 ↑o ∅ ) ) = ( ( 𝐴 ↑o 𝐵 ) ·o 1o )
31 oa0 ⊢ ( 𝐵 ∈ On → ( 𝐵 +o ∅ ) = 𝐵 )
32 3 31 ax-mp ⊢ ( 𝐵 +o ∅ ) = 𝐵
33 32 oveq2i ⊢ ( 𝐴 ↑o ( 𝐵 +o ∅ ) ) = ( 𝐴 ↑o 𝐵 )
34 27 30 33 3eqtr4ri ⊢ ( 𝐴 ↑o ( 𝐵 +o ∅ ) ) = ( ( 𝐴 ↑o 𝐵 ) ·o ( 𝐴 ↑o ∅ ) )
35 oasuc ⊢ ( ( 𝐵 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐵 +o suc 𝑦 ) = suc ( 𝐵 +o 𝑦 ) )
36 35 oveq2d ⊢ ( ( 𝐵 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐴 ↑o ( 𝐵 +o suc 𝑦 ) ) = ( 𝐴 ↑o suc ( 𝐵 +o 𝑦 ) ) )
37 oacl ⊢ ( ( 𝐵 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐵 +o 𝑦 ) ∈ On )
38 oesuc ⊢ ( ( 𝐴 ∈ On ∧ ( 𝐵 +o 𝑦 ) ∈ On ) → ( 𝐴 ↑o suc ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ↑o ( 𝐵 +o 𝑦 ) ) ·o 𝐴 ) )
39 1 37 38 sylancr ⊢ ( ( 𝐵 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐴 ↑o suc ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ↑o ( 𝐵 +o 𝑦 ) ) ·o 𝐴 ) )
40 36 39 eqtrd ⊢ ( ( 𝐵 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐴 ↑o ( 𝐵 +o suc 𝑦 ) ) = ( ( 𝐴 ↑o ( 𝐵 +o 𝑦 ) ) ·o 𝐴 ) )
41 3 40 mpan ⊢ ( 𝑦 ∈ On → ( 𝐴 ↑o ( 𝐵 +o suc 𝑦 ) ) = ( ( 𝐴 ↑o ( 𝐵 +o 𝑦 ) ) ·o 𝐴 ) )
42 oveq1 ⊢ ( ( 𝐴 ↑o ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ↑o 𝐵 ) ·o ( 𝐴 ↑o 𝑦 ) ) → ( ( 𝐴 ↑o ( 𝐵 +o 𝑦 ) ) ·o 𝐴 ) = ( ( ( 𝐴 ↑o 𝐵 ) ·o ( 𝐴 ↑o 𝑦 ) ) ·o 𝐴 ) )
43 41 42 sylan9eq ⊢ ( ( 𝑦 ∈ On ∧ ( 𝐴 ↑o ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ↑o 𝐵 ) ·o ( 𝐴 ↑o 𝑦 ) ) ) → ( 𝐴 ↑o ( 𝐵 +o suc 𝑦 ) ) = ( ( ( 𝐴 ↑o 𝐵 ) ·o ( 𝐴 ↑o 𝑦 ) ) ·o 𝐴 ) )
44 oecl ⊢ ( ( 𝐴 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐴 ↑o 𝑦 ) ∈ On )
45 omass ⊢ ( ( ( 𝐴 ↑o 𝐵 ) ∈ On ∧ ( 𝐴 ↑o 𝑦 ) ∈ On ∧ 𝐴 ∈ On ) → ( ( ( 𝐴 ↑o 𝐵 ) ·o ( 𝐴 ↑o 𝑦 ) ) ·o 𝐴 ) = ( ( 𝐴 ↑o 𝐵 ) ·o ( ( 𝐴 ↑o 𝑦 ) ·o 𝐴 ) ) )
46 25 1 45 mp3an13 ⊢ ( ( 𝐴 ↑o 𝑦 ) ∈ On → ( ( ( 𝐴 ↑o 𝐵 ) ·o ( 𝐴 ↑o 𝑦 ) ) ·o 𝐴 ) = ( ( 𝐴 ↑o 𝐵 ) ·o ( ( 𝐴 ↑o 𝑦 ) ·o 𝐴 ) ) )
47 44 46 syl ⊢ ( ( 𝐴 ∈ On ∧ 𝑦 ∈ On ) → ( ( ( 𝐴 ↑o 𝐵 ) ·o ( 𝐴 ↑o 𝑦 ) ) ·o 𝐴 ) = ( ( 𝐴 ↑o 𝐵 ) ·o ( ( 𝐴 ↑o 𝑦 ) ·o 𝐴 ) ) )
48 oesuc ⊢ ( ( 𝐴 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐴 ↑o suc 𝑦 ) = ( ( 𝐴 ↑o 𝑦 ) ·o 𝐴 ) )
49 48 oveq2d ⊢ ( ( 𝐴 ∈ On ∧ 𝑦 ∈ On ) → ( ( 𝐴 ↑o 𝐵 ) ·o ( 𝐴 ↑o suc 𝑦 ) ) = ( ( 𝐴 ↑o 𝐵 ) ·o ( ( 𝐴 ↑o 𝑦 ) ·o 𝐴 ) ) )
50 47 49 eqtr4d ⊢ ( ( 𝐴 ∈ On ∧ 𝑦 ∈ On ) → ( ( ( 𝐴 ↑o 𝐵 ) ·o ( 𝐴 ↑o 𝑦 ) ) ·o 𝐴 ) = ( ( 𝐴 ↑o 𝐵 ) ·o ( 𝐴 ↑o suc 𝑦 ) ) )
51 1 50 mpan ⊢ ( 𝑦 ∈ On → ( ( ( 𝐴 ↑o 𝐵 ) ·o ( 𝐴 ↑o 𝑦 ) ) ·o 𝐴 ) = ( ( 𝐴 ↑o 𝐵 ) ·o ( 𝐴 ↑o suc 𝑦 ) ) )
52 51 adantr ⊢ ( ( 𝑦 ∈ On ∧ ( 𝐴 ↑o ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ↑o 𝐵 ) ·o ( 𝐴 ↑o 𝑦 ) ) ) → ( ( ( 𝐴 ↑o 𝐵 ) ·o ( 𝐴 ↑o 𝑦 ) ) ·o 𝐴 ) = ( ( 𝐴 ↑o 𝐵 ) ·o ( 𝐴 ↑o suc 𝑦 ) ) )
53 43 52 eqtrd ⊢ ( ( 𝑦 ∈ On ∧ ( 𝐴 ↑o ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ↑o 𝐵 ) ·o ( 𝐴 ↑o 𝑦 ) ) ) → ( 𝐴 ↑o ( 𝐵 +o suc 𝑦 ) ) = ( ( 𝐴 ↑o 𝐵 ) ·o ( 𝐴 ↑o suc 𝑦 ) ) )
54 53 ex ⊢ ( 𝑦 ∈ On → ( ( 𝐴 ↑o ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ↑o 𝐵 ) ·o ( 𝐴 ↑o 𝑦 ) ) → ( 𝐴 ↑o ( 𝐵 +o suc 𝑦 ) ) = ( ( 𝐴 ↑o 𝐵 ) ·o ( 𝐴 ↑o suc 𝑦 ) ) ) )
55 vex ⊢ 𝑥 ∈ V
56 oalim ⊢ ( ( 𝐵 ∈ On ∧ ( 𝑥 ∈ V ∧ Lim 𝑥 ) ) → ( 𝐵 +o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝐵 +o 𝑦 ) )
57 3 56 mpan ⊢ ( ( 𝑥 ∈ V ∧ Lim 𝑥 ) → ( 𝐵 +o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝐵 +o 𝑦 ) )
58 55 57 mpan ⊢ ( Lim 𝑥 → ( 𝐵 +o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝐵 +o 𝑦 ) )
59 58 oveq2d ⊢ ( Lim 𝑥 → ( 𝐴 ↑o ( 𝐵 +o 𝑥 ) ) = ( 𝐴 ↑o ∪ 𝑦 ∈ 𝑥 ( 𝐵 +o 𝑦 ) ) )
60 limord ⊢ ( Lim 𝑥 → Ord 𝑥 )
61 ordelon ⊢ ( ( Ord 𝑥 ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ On )
62 60 61 sylan ⊢ ( ( Lim 𝑥 ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ On )
63 3 62 37 sylancr ⊢ ( ( Lim 𝑥 ∧ 𝑦 ∈ 𝑥 ) → ( 𝐵 +o 𝑦 ) ∈ On )
64 63 ralrimiva ⊢ ( Lim 𝑥 → ∀ 𝑦 ∈ 𝑥 ( 𝐵 +o 𝑦 ) ∈ On )
65 0ellim ⊢ ( Lim 𝑥 → ∅ ∈ 𝑥 )
66 65 ne0d ⊢ ( Lim 𝑥 → 𝑥 ≠ ∅ )
67 vex ⊢ 𝑤 ∈ V
68 oelim ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝑤 ∈ V ∧ Lim 𝑤 ) ) ∧ ∅ ∈ 𝐴 ) → ( 𝐴 ↑o 𝑤 ) = ∪ 𝑧 ∈ 𝑤 ( 𝐴 ↑o 𝑧 ) )
69 2 68 mpan2 ⊢ ( ( 𝐴 ∈ On ∧ ( 𝑤 ∈ V ∧ Lim 𝑤 ) ) → ( 𝐴 ↑o 𝑤 ) = ∪ 𝑧 ∈ 𝑤 ( 𝐴 ↑o 𝑧 ) )
70 1 69 mpan ⊢ ( ( 𝑤 ∈ V ∧ Lim 𝑤 ) → ( 𝐴 ↑o 𝑤 ) = ∪ 𝑧 ∈ 𝑤 ( 𝐴 ↑o 𝑧 ) )
71 67 70 mpan ⊢ ( Lim 𝑤 → ( 𝐴 ↑o 𝑤 ) = ∪ 𝑧 ∈ 𝑤 ( 𝐴 ↑o 𝑧 ) )
72 oewordi ⊢ ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ∧ 𝐴 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ( 𝑧 ⊆ 𝑤 → ( 𝐴 ↑o 𝑧 ) ⊆ ( 𝐴 ↑o 𝑤 ) ) )
73 2 72 mpan2 ⊢ ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ∧ 𝐴 ∈ On ) → ( 𝑧 ⊆ 𝑤 → ( 𝐴 ↑o 𝑧 ) ⊆ ( 𝐴 ↑o 𝑤 ) ) )
74 1 73 mp3an3 ⊢ ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) → ( 𝑧 ⊆ 𝑤 → ( 𝐴 ↑o 𝑧 ) ⊆ ( 𝐴 ↑o 𝑤 ) ) )
75 74 3impia ⊢ ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ∧ 𝑧 ⊆ 𝑤 ) → ( 𝐴 ↑o 𝑧 ) ⊆ ( 𝐴 ↑o 𝑤 ) )
76 71 75 onoviun ⊢ ( ( 𝑥 ∈ V ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐵 +o 𝑦 ) ∈ On ∧ 𝑥 ≠ ∅ ) → ( 𝐴 ↑o ∪ 𝑦 ∈ 𝑥 ( 𝐵 +o 𝑦 ) ) = ∪ 𝑦 ∈ 𝑥 ( 𝐴 ↑o ( 𝐵 +o 𝑦 ) ) )
77 55 64 66 76 mp3an2i ⊢ ( Lim 𝑥 → ( 𝐴 ↑o ∪ 𝑦 ∈ 𝑥 ( 𝐵 +o 𝑦 ) ) = ∪ 𝑦 ∈ 𝑥 ( 𝐴 ↑o ( 𝐵 +o 𝑦 ) ) )
78 59 77 eqtrd ⊢ ( Lim 𝑥 → ( 𝐴 ↑o ( 𝐵 +o 𝑥 ) ) = ∪ 𝑦 ∈ 𝑥 ( 𝐴 ↑o ( 𝐵 +o 𝑦 ) ) )
79 iuneq2 ⊢ ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ↑o ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ↑o 𝐵 ) ·o ( 𝐴 ↑o 𝑦 ) ) → ∪ 𝑦 ∈ 𝑥 ( 𝐴 ↑o ( 𝐵 +o 𝑦 ) ) = ∪ 𝑦 ∈ 𝑥 ( ( 𝐴 ↑o 𝐵 ) ·o ( 𝐴 ↑o 𝑦 ) ) )
80 78 79 sylan9eq ⊢ ( ( Lim 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ↑o ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ↑o 𝐵 ) ·o ( 𝐴 ↑o 𝑦 ) ) ) → ( 𝐴 ↑o ( 𝐵 +o 𝑥 ) ) = ∪ 𝑦 ∈ 𝑥 ( ( 𝐴 ↑o 𝐵 ) ·o ( 𝐴 ↑o 𝑦 ) ) )
81 oelim ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝑥 ∈ V ∧ Lim 𝑥 ) ) ∧ ∅ ∈ 𝐴 ) → ( 𝐴 ↑o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝐴 ↑o 𝑦 ) )
82 2 81 mpan2 ⊢ ( ( 𝐴 ∈ On ∧ ( 𝑥 ∈ V ∧ Lim 𝑥 ) ) → ( 𝐴 ↑o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝐴 ↑o 𝑦 ) )
83 1 82 mpan ⊢ ( ( 𝑥 ∈ V ∧ Lim 𝑥 ) → ( 𝐴 ↑o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝐴 ↑o 𝑦 ) )
84 55 83 mpan ⊢ ( Lim 𝑥 → ( 𝐴 ↑o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝐴 ↑o 𝑦 ) )
85 84 oveq2d ⊢ ( Lim 𝑥 → ( ( 𝐴 ↑o 𝐵 ) ·o ( 𝐴 ↑o 𝑥 ) ) = ( ( 𝐴 ↑o 𝐵 ) ·o ∪ 𝑦 ∈ 𝑥 ( 𝐴 ↑o 𝑦 ) ) )
86 1 62 44 sylancr ⊢ ( ( Lim 𝑥 ∧ 𝑦 ∈ 𝑥 ) → ( 𝐴 ↑o 𝑦 ) ∈ On )
87 86 ralrimiva ⊢ ( Lim 𝑥 → ∀ 𝑦 ∈ 𝑥 ( 𝐴 ↑o 𝑦 ) ∈ On )
88 omlim ⊢ ( ( ( 𝐴 ↑o 𝐵 ) ∈ On ∧ ( 𝑤 ∈ V ∧ Lim 𝑤 ) ) → ( ( 𝐴 ↑o 𝐵 ) ·o 𝑤 ) = ∪ 𝑧 ∈ 𝑤 ( ( 𝐴 ↑o 𝐵 ) ·o 𝑧 ) )
89 25 88 mpan ⊢ ( ( 𝑤 ∈ V ∧ Lim 𝑤 ) → ( ( 𝐴 ↑o 𝐵 ) ·o 𝑤 ) = ∪ 𝑧 ∈ 𝑤 ( ( 𝐴 ↑o 𝐵 ) ·o 𝑧 ) )
90 67 89 mpan ⊢ ( Lim 𝑤 → ( ( 𝐴 ↑o 𝐵 ) ·o 𝑤 ) = ∪ 𝑧 ∈ 𝑤 ( ( 𝐴 ↑o 𝐵 ) ·o 𝑧 ) )
91 omwordi ⊢ ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ∧ ( 𝐴 ↑o 𝐵 ) ∈ On ) → ( 𝑧 ⊆ 𝑤 → ( ( 𝐴 ↑o 𝐵 ) ·o 𝑧 ) ⊆ ( ( 𝐴 ↑o 𝐵 ) ·o 𝑤 ) ) )
92 25 91 mp3an3 ⊢ ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) → ( 𝑧 ⊆ 𝑤 → ( ( 𝐴 ↑o 𝐵 ) ·o 𝑧 ) ⊆ ( ( 𝐴 ↑o 𝐵 ) ·o 𝑤 ) ) )
93 92 3impia ⊢ ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ∧ 𝑧 ⊆ 𝑤 ) → ( ( 𝐴 ↑o 𝐵 ) ·o 𝑧 ) ⊆ ( ( 𝐴 ↑o 𝐵 ) ·o 𝑤 ) )
94 90 93 onoviun ⊢ ( ( 𝑥 ∈ V ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ↑o 𝑦 ) ∈ On ∧ 𝑥 ≠ ∅ ) → ( ( 𝐴 ↑o 𝐵 ) ·o ∪ 𝑦 ∈ 𝑥 ( 𝐴 ↑o 𝑦 ) ) = ∪ 𝑦 ∈ 𝑥 ( ( 𝐴 ↑o 𝐵 ) ·o ( 𝐴 ↑o 𝑦 ) ) )
95 55 87 66 94 mp3an2i ⊢ ( Lim 𝑥 → ( ( 𝐴 ↑o 𝐵 ) ·o ∪ 𝑦 ∈ 𝑥 ( 𝐴 ↑o 𝑦 ) ) = ∪ 𝑦 ∈ 𝑥 ( ( 𝐴 ↑o 𝐵 ) ·o ( 𝐴 ↑o 𝑦 ) ) )
96 85 95 eqtrd ⊢ ( Lim 𝑥 → ( ( 𝐴 ↑o 𝐵 ) ·o ( 𝐴 ↑o 𝑥 ) ) = ∪ 𝑦 ∈ 𝑥 ( ( 𝐴 ↑o 𝐵 ) ·o ( 𝐴 ↑o 𝑦 ) ) )
97 96 adantr ⊢ ( ( Lim 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ↑o ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ↑o 𝐵 ) ·o ( 𝐴 ↑o 𝑦 ) ) ) → ( ( 𝐴 ↑o 𝐵 ) ·o ( 𝐴 ↑o 𝑥 ) ) = ∪ 𝑦 ∈ 𝑥 ( ( 𝐴 ↑o 𝐵 ) ·o ( 𝐴 ↑o 𝑦 ) ) )
98 80 97 eqtr4d ⊢ ( ( Lim 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ↑o ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ↑o 𝐵 ) ·o ( 𝐴 ↑o 𝑦 ) ) ) → ( 𝐴 ↑o ( 𝐵 +o 𝑥 ) ) = ( ( 𝐴 ↑o 𝐵 ) ·o ( 𝐴 ↑o 𝑥 ) ) )
99 98 ex ⊢ ( Lim 𝑥 → ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ↑o ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ↑o 𝐵 ) ·o ( 𝐴 ↑o 𝑦 ) ) → ( 𝐴 ↑o ( 𝐵 +o 𝑥 ) ) = ( ( 𝐴 ↑o 𝐵 ) ·o ( 𝐴 ↑o 𝑥 ) ) ) )
100 8 13 18 23 34 54 99 tfinds ⊢ ( 𝐶 ∈ On → ( 𝐴 ↑o ( 𝐵 +o 𝐶 ) ) = ( ( 𝐴 ↑o 𝐵 ) ·o ( 𝐴 ↑o 𝐶 ) ) )