This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem odi

Description: Distributive law for ordinal arithmetic (left-distributivity). Proposition 8.25 of TakeutiZaring p. 64. Theorem 4.3 of Schloeder p. 12. (Contributed by NM, 26-Dec-2004)

Ref Expression
Assertion odi ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ·o ( 𝐵 +o 𝐶 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ ( 𝑥 = ∅ → ( 𝐵 +o 𝑥 ) = ( 𝐵 +o ∅ ) )
2 1 oveq2d ⊢ ( 𝑥 = ∅ → ( 𝐴 ·o ( 𝐵 +o 𝑥 ) ) = ( 𝐴 ·o ( 𝐵 +o ∅ ) ) )
3 oveq2 ⊢ ( 𝑥 = ∅ → ( 𝐴 ·o 𝑥 ) = ( 𝐴 ·o ∅ ) )
4 3 oveq2d ⊢ ( 𝑥 = ∅ → ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑥 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o ∅ ) ) )
5 2 4 eqeq12d ⊢ ( 𝑥 = ∅ → ( ( 𝐴 ·o ( 𝐵 +o 𝑥 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑥 ) ) ↔ ( 𝐴 ·o ( 𝐵 +o ∅ ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o ∅ ) ) ) )
6 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐵 +o 𝑥 ) = ( 𝐵 +o 𝑦 ) )
7 6 oveq2d ⊢ ( 𝑥 = 𝑦 → ( 𝐴 ·o ( 𝐵 +o 𝑥 ) ) = ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) )
8 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐴 ·o 𝑥 ) = ( 𝐴 ·o 𝑦 ) )
9 8 oveq2d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑥 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) )
10 7 9 eqeq12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐴 ·o ( 𝐵 +o 𝑥 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑥 ) ) ↔ ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) ) )
11 oveq2 ⊢ ( 𝑥 = suc 𝑦 → ( 𝐵 +o 𝑥 ) = ( 𝐵 +o suc 𝑦 ) )
12 11 oveq2d ⊢ ( 𝑥 = suc 𝑦 → ( 𝐴 ·o ( 𝐵 +o 𝑥 ) ) = ( 𝐴 ·o ( 𝐵 +o suc 𝑦 ) ) )
13 oveq2 ⊢ ( 𝑥 = suc 𝑦 → ( 𝐴 ·o 𝑥 ) = ( 𝐴 ·o suc 𝑦 ) )
14 13 oveq2d ⊢ ( 𝑥 = suc 𝑦 → ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑥 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o suc 𝑦 ) ) )
15 12 14 eqeq12d ⊢ ( 𝑥 = suc 𝑦 → ( ( 𝐴 ·o ( 𝐵 +o 𝑥 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑥 ) ) ↔ ( 𝐴 ·o ( 𝐵 +o suc 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o suc 𝑦 ) ) ) )
16 oveq2 ⊢ ( 𝑥 = 𝐶 → ( 𝐵 +o 𝑥 ) = ( 𝐵 +o 𝐶 ) )
17 16 oveq2d ⊢ ( 𝑥 = 𝐶 → ( 𝐴 ·o ( 𝐵 +o 𝑥 ) ) = ( 𝐴 ·o ( 𝐵 +o 𝐶 ) ) )
18 oveq2 ⊢ ( 𝑥 = 𝐶 → ( 𝐴 ·o 𝑥 ) = ( 𝐴 ·o 𝐶 ) )
19 18 oveq2d ⊢ ( 𝑥 = 𝐶 → ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑥 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝐶 ) ) )
20 17 19 eqeq12d ⊢ ( 𝑥 = 𝐶 → ( ( 𝐴 ·o ( 𝐵 +o 𝑥 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑥 ) ) ↔ ( 𝐴 ·o ( 𝐵 +o 𝐶 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝐶 ) ) ) )
21 omcl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ·o 𝐵 ) ∈ On )
22 oa0 ⊢ ( ( 𝐴 ·o 𝐵 ) ∈ On → ( ( 𝐴 ·o 𝐵 ) +o ∅ ) = ( 𝐴 ·o 𝐵 ) )
23 21 22 syl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐴 ·o 𝐵 ) +o ∅ ) = ( 𝐴 ·o 𝐵 ) )
24 om0 ⊢ ( 𝐴 ∈ On → ( 𝐴 ·o ∅ ) = ∅ )
25 24 adantr ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ·o ∅ ) = ∅ )
26 25 oveq2d ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o ∅ ) ) = ( ( 𝐴 ·o 𝐵 ) +o ∅ ) )
27 oa0 ⊢ ( 𝐵 ∈ On → ( 𝐵 +o ∅ ) = 𝐵 )
28 27 adantl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐵 +o ∅ ) = 𝐵 )
29 28 oveq2d ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ·o ( 𝐵 +o ∅ ) ) = ( 𝐴 ·o 𝐵 ) )
30 23 26 29 3eqtr4rd ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ·o ( 𝐵 +o ∅ ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o ∅ ) ) )
31 oveq1 ⊢ ( ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) → ( ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) +o 𝐴 ) = ( ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) +o 𝐴 ) )
32 oasuc ⊢ ( ( 𝐵 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐵 +o suc 𝑦 ) = suc ( 𝐵 +o 𝑦 ) )
33 32 3adant1 ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐵 +o suc 𝑦 ) = suc ( 𝐵 +o 𝑦 ) )
34 33 oveq2d ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐴 ·o ( 𝐵 +o suc 𝑦 ) ) = ( 𝐴 ·o suc ( 𝐵 +o 𝑦 ) ) )
35 oacl ⊢ ( ( 𝐵 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐵 +o 𝑦 ) ∈ On )
36 omsuc ⊢ ( ( 𝐴 ∈ On ∧ ( 𝐵 +o 𝑦 ) ∈ On ) → ( 𝐴 ·o suc ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) +o 𝐴 ) )
37 35 36 sylan2 ⊢ ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ On ∧ 𝑦 ∈ On ) ) → ( 𝐴 ·o suc ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) +o 𝐴 ) )
38 37 3impb ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐴 ·o suc ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) +o 𝐴 ) )
39 34 38 eqtrd ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐴 ·o ( 𝐵 +o suc 𝑦 ) ) = ( ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) +o 𝐴 ) )
40 omsuc ⊢ ( ( 𝐴 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐴 ·o suc 𝑦 ) = ( ( 𝐴 ·o 𝑦 ) +o 𝐴 ) )
41 40 3adant2 ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐴 ·o suc 𝑦 ) = ( ( 𝐴 ·o 𝑦 ) +o 𝐴 ) )
42 41 oveq2d ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On ) → ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o suc 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( ( 𝐴 ·o 𝑦 ) +o 𝐴 ) ) )
43 omcl ⊢ ( ( 𝐴 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐴 ·o 𝑦 ) ∈ On )
44 oaass ⊢ ( ( ( 𝐴 ·o 𝐵 ) ∈ On ∧ ( 𝐴 ·o 𝑦 ) ∈ On ∧ 𝐴 ∈ On ) → ( ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) +o 𝐴 ) = ( ( 𝐴 ·o 𝐵 ) +o ( ( 𝐴 ·o 𝑦 ) +o 𝐴 ) ) )
45 21 44 syl3an1 ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐴 ·o 𝑦 ) ∈ On ∧ 𝐴 ∈ On ) → ( ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) +o 𝐴 ) = ( ( 𝐴 ·o 𝐵 ) +o ( ( 𝐴 ·o 𝑦 ) +o 𝐴 ) ) )
46 43 45 syl3an2 ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐴 ∈ On ∧ 𝑦 ∈ On ) ∧ 𝐴 ∈ On ) → ( ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) +o 𝐴 ) = ( ( 𝐴 ·o 𝐵 ) +o ( ( 𝐴 ·o 𝑦 ) +o 𝐴 ) ) )
47 46 3exp ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐴 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐴 ∈ On → ( ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) +o 𝐴 ) = ( ( 𝐴 ·o 𝐵 ) +o ( ( 𝐴 ·o 𝑦 ) +o 𝐴 ) ) ) ) )
48 47 exp4b ⊢ ( 𝐴 ∈ On → ( 𝐵 ∈ On → ( 𝐴 ∈ On → ( 𝑦 ∈ On → ( 𝐴 ∈ On → ( ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) +o 𝐴 ) = ( ( 𝐴 ·o 𝐵 ) +o ( ( 𝐴 ·o 𝑦 ) +o 𝐴 ) ) ) ) ) ) )
49 48 pm2.43a ⊢ ( 𝐴 ∈ On → ( 𝐵 ∈ On → ( 𝑦 ∈ On → ( 𝐴 ∈ On → ( ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) +o 𝐴 ) = ( ( 𝐴 ·o 𝐵 ) +o ( ( 𝐴 ·o 𝑦 ) +o 𝐴 ) ) ) ) ) )
50 49 com4r ⊢ ( 𝐴 ∈ On → ( 𝐴 ∈ On → ( 𝐵 ∈ On → ( 𝑦 ∈ On → ( ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) +o 𝐴 ) = ( ( 𝐴 ·o 𝐵 ) +o ( ( 𝐴 ·o 𝑦 ) +o 𝐴 ) ) ) ) ) )
51 50 pm2.43i ⊢ ( 𝐴 ∈ On → ( 𝐵 ∈ On → ( 𝑦 ∈ On → ( ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) +o 𝐴 ) = ( ( 𝐴 ·o 𝐵 ) +o ( ( 𝐴 ·o 𝑦 ) +o 𝐴 ) ) ) ) )
52 51 3imp ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On ) → ( ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) +o 𝐴 ) = ( ( 𝐴 ·o 𝐵 ) +o ( ( 𝐴 ·o 𝑦 ) +o 𝐴 ) ) )
53 42 52 eqtr4d ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On ) → ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o suc 𝑦 ) ) = ( ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) +o 𝐴 ) )
54 39 53 eqeq12d ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On ) → ( ( 𝐴 ·o ( 𝐵 +o suc 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o suc 𝑦 ) ) ↔ ( ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) +o 𝐴 ) = ( ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) +o 𝐴 ) ) )
55 31 54 imbitrrid ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On ) → ( ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) → ( 𝐴 ·o ( 𝐵 +o suc 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o suc 𝑦 ) ) ) )
56 55 3exp ⊢ ( 𝐴 ∈ On → ( 𝐵 ∈ On → ( 𝑦 ∈ On → ( ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) → ( 𝐴 ·o ( 𝐵 +o suc 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o suc 𝑦 ) ) ) ) ) )
57 56 com3r ⊢ ( 𝑦 ∈ On → ( 𝐴 ∈ On → ( 𝐵 ∈ On → ( ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) → ( 𝐴 ·o ( 𝐵 +o suc 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o suc 𝑦 ) ) ) ) ) )
58 57 impd ⊢ ( 𝑦 ∈ On → ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) → ( 𝐴 ·o ( 𝐵 +o suc 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o suc 𝑦 ) ) ) ) )
59 vex ⊢ 𝑥 ∈ V
60 limelon ⊢ ( ( 𝑥 ∈ V ∧ Lim 𝑥 ) → 𝑥 ∈ On )
61 59 60 mpan ⊢ ( Lim 𝑥 → 𝑥 ∈ On )
62 oacl ⊢ ( ( 𝐵 ∈ On ∧ 𝑥 ∈ On ) → ( 𝐵 +o 𝑥 ) ∈ On )
63 om0r ⊢ ( ( 𝐵 +o 𝑥 ) ∈ On → ( ∅ ·o ( 𝐵 +o 𝑥 ) ) = ∅ )
64 62 63 syl ⊢ ( ( 𝐵 ∈ On ∧ 𝑥 ∈ On ) → ( ∅ ·o ( 𝐵 +o 𝑥 ) ) = ∅ )
65 om0r ⊢ ( 𝐵 ∈ On → ( ∅ ·o 𝐵 ) = ∅ )
66 om0r ⊢ ( 𝑥 ∈ On → ( ∅ ·o 𝑥 ) = ∅ )
67 65 66 oveqan12d ⊢ ( ( 𝐵 ∈ On ∧ 𝑥 ∈ On ) → ( ( ∅ ·o 𝐵 ) +o ( ∅ ·o 𝑥 ) ) = ( ∅ +o ∅ ) )
68 0elon ⊢ ∅ ∈ On
69 oa0 ⊢ ( ∅ ∈ On → ( ∅ +o ∅ ) = ∅ )
70 68 69 ax-mp ⊢ ( ∅ +o ∅ ) = ∅
71 67 70 eqtr2di ⊢ ( ( 𝐵 ∈ On ∧ 𝑥 ∈ On ) → ∅ = ( ( ∅ ·o 𝐵 ) +o ( ∅ ·o 𝑥 ) ) )
72 64 71 eqtrd ⊢ ( ( 𝐵 ∈ On ∧ 𝑥 ∈ On ) → ( ∅ ·o ( 𝐵 +o 𝑥 ) ) = ( ( ∅ ·o 𝐵 ) +o ( ∅ ·o 𝑥 ) ) )
73 61 72 sylan2 ⊢ ( ( 𝐵 ∈ On ∧ Lim 𝑥 ) → ( ∅ ·o ( 𝐵 +o 𝑥 ) ) = ( ( ∅ ·o 𝐵 ) +o ( ∅ ·o 𝑥 ) ) )
74 73 ancoms ⊢ ( ( Lim 𝑥 ∧ 𝐵 ∈ On ) → ( ∅ ·o ( 𝐵 +o 𝑥 ) ) = ( ( ∅ ·o 𝐵 ) +o ( ∅ ·o 𝑥 ) ) )
75 oveq1 ⊢ ( 𝐴 = ∅ → ( 𝐴 ·o ( 𝐵 +o 𝑥 ) ) = ( ∅ ·o ( 𝐵 +o 𝑥 ) ) )
76 oveq1 ⊢ ( 𝐴 = ∅ → ( 𝐴 ·o 𝐵 ) = ( ∅ ·o 𝐵 ) )
77 oveq1 ⊢ ( 𝐴 = ∅ → ( 𝐴 ·o 𝑥 ) = ( ∅ ·o 𝑥 ) )
78 76 77 oveq12d ⊢ ( 𝐴 = ∅ → ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑥 ) ) = ( ( ∅ ·o 𝐵 ) +o ( ∅ ·o 𝑥 ) ) )
79 75 78 eqeq12d ⊢ ( 𝐴 = ∅ → ( ( 𝐴 ·o ( 𝐵 +o 𝑥 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑥 ) ) ↔ ( ∅ ·o ( 𝐵 +o 𝑥 ) ) = ( ( ∅ ·o 𝐵 ) +o ( ∅ ·o 𝑥 ) ) ) )
80 74 79 imbitrrid ⊢ ( 𝐴 = ∅ → ( ( Lim 𝑥 ∧ 𝐵 ∈ On ) → ( 𝐴 ·o ( 𝐵 +o 𝑥 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑥 ) ) ) )
81 80 expd ⊢ ( 𝐴 = ∅ → ( Lim 𝑥 → ( 𝐵 ∈ On → ( 𝐴 ·o ( 𝐵 +o 𝑥 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑥 ) ) ) ) )
82 81 com3r ⊢ ( 𝐵 ∈ On → ( 𝐴 = ∅ → ( Lim 𝑥 → ( 𝐴 ·o ( 𝐵 +o 𝑥 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑥 ) ) ) ) )
83 82 imp ⊢ ( ( 𝐵 ∈ On ∧ 𝐴 = ∅ ) → ( Lim 𝑥 → ( 𝐴 ·o ( 𝐵 +o 𝑥 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑥 ) ) ) )
84 83 a1dd ⊢ ( ( 𝐵 ∈ On ∧ 𝐴 = ∅ ) → ( Lim 𝑥 → ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) → ( 𝐴 ·o ( 𝐵 +o 𝑥 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑥 ) ) ) ) )
85 simplr ⊢ ( ( ( 𝑥 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝑧 ∈ ( 𝐵 +o 𝑥 ) ) → 𝐵 ∈ On )
86 62 ancoms ⊢ ( ( 𝑥 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐵 +o 𝑥 ) ∈ On )
87 onelon ⊢ ( ( ( 𝐵 +o 𝑥 ) ∈ On ∧ 𝑧 ∈ ( 𝐵 +o 𝑥 ) ) → 𝑧 ∈ On )
88 86 87 sylan ⊢ ( ( ( 𝑥 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝑧 ∈ ( 𝐵 +o 𝑥 ) ) → 𝑧 ∈ On )
89 ontri1 ⊢ ( ( 𝐵 ∈ On ∧ 𝑧 ∈ On ) → ( 𝐵 ⊆ 𝑧 ↔ ¬ 𝑧 ∈ 𝐵 ) )
90 oawordex ⊢ ( ( 𝐵 ∈ On ∧ 𝑧 ∈ On ) → ( 𝐵 ⊆ 𝑧 ↔ ∃ 𝑣 ∈ On ( 𝐵 +o 𝑣 ) = 𝑧 ) )
91 89 90 bitr3d ⊢ ( ( 𝐵 ∈ On ∧ 𝑧 ∈ On ) → ( ¬ 𝑧 ∈ 𝐵 ↔ ∃ 𝑣 ∈ On ( 𝐵 +o 𝑣 ) = 𝑧 ) )
92 85 88 91 syl2anc ⊢ ( ( ( 𝑥 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝑧 ∈ ( 𝐵 +o 𝑥 ) ) → ( ¬ 𝑧 ∈ 𝐵 ↔ ∃ 𝑣 ∈ On ( 𝐵 +o 𝑣 ) = 𝑧 ) )
93 oaord ⊢ ( ( 𝑣 ∈ On ∧ 𝑥 ∈ On ∧ 𝐵 ∈ On ) → ( 𝑣 ∈ 𝑥 ↔ ( 𝐵 +o 𝑣 ) ∈ ( 𝐵 +o 𝑥 ) ) )
94 93 3expb ⊢ ( ( 𝑣 ∈ On ∧ ( 𝑥 ∈ On ∧ 𝐵 ∈ On ) ) → ( 𝑣 ∈ 𝑥 ↔ ( 𝐵 +o 𝑣 ) ∈ ( 𝐵 +o 𝑥 ) ) )
95 eleq1 ⊢ ( ( 𝐵 +o 𝑣 ) = 𝑧 → ( ( 𝐵 +o 𝑣 ) ∈ ( 𝐵 +o 𝑥 ) ↔ 𝑧 ∈ ( 𝐵 +o 𝑥 ) ) )
96 94 95 sylan9bb ⊢ ( ( ( 𝑣 ∈ On ∧ ( 𝑥 ∈ On ∧ 𝐵 ∈ On ) ) ∧ ( 𝐵 +o 𝑣 ) = 𝑧 ) → ( 𝑣 ∈ 𝑥 ↔ 𝑧 ∈ ( 𝐵 +o 𝑥 ) ) )
97 iba ⊢ ( ( 𝐵 +o 𝑣 ) = 𝑧 → ( 𝑣 ∈ 𝑥 ↔ ( 𝑣 ∈ 𝑥 ∧ ( 𝐵 +o 𝑣 ) = 𝑧 ) ) )
98 97 adantl ⊢ ( ( ( 𝑣 ∈ On ∧ ( 𝑥 ∈ On ∧ 𝐵 ∈ On ) ) ∧ ( 𝐵 +o 𝑣 ) = 𝑧 ) → ( 𝑣 ∈ 𝑥 ↔ ( 𝑣 ∈ 𝑥 ∧ ( 𝐵 +o 𝑣 ) = 𝑧 ) ) )
99 96 98 bitr3d ⊢ ( ( ( 𝑣 ∈ On ∧ ( 𝑥 ∈ On ∧ 𝐵 ∈ On ) ) ∧ ( 𝐵 +o 𝑣 ) = 𝑧 ) → ( 𝑧 ∈ ( 𝐵 +o 𝑥 ) ↔ ( 𝑣 ∈ 𝑥 ∧ ( 𝐵 +o 𝑣 ) = 𝑧 ) ) )
100 99 an32s ⊢ ( ( ( 𝑣 ∈ On ∧ ( 𝐵 +o 𝑣 ) = 𝑧 ) ∧ ( 𝑥 ∈ On ∧ 𝐵 ∈ On ) ) → ( 𝑧 ∈ ( 𝐵 +o 𝑥 ) ↔ ( 𝑣 ∈ 𝑥 ∧ ( 𝐵 +o 𝑣 ) = 𝑧 ) ) )
101 100 biimpcd ⊢ ( 𝑧 ∈ ( 𝐵 +o 𝑥 ) → ( ( ( 𝑣 ∈ On ∧ ( 𝐵 +o 𝑣 ) = 𝑧 ) ∧ ( 𝑥 ∈ On ∧ 𝐵 ∈ On ) ) → ( 𝑣 ∈ 𝑥 ∧ ( 𝐵 +o 𝑣 ) = 𝑧 ) ) )
102 101 exp4c ⊢ ( 𝑧 ∈ ( 𝐵 +o 𝑥 ) → ( 𝑣 ∈ On → ( ( 𝐵 +o 𝑣 ) = 𝑧 → ( ( 𝑥 ∈ On ∧ 𝐵 ∈ On ) → ( 𝑣 ∈ 𝑥 ∧ ( 𝐵 +o 𝑣 ) = 𝑧 ) ) ) ) )
103 102 com4r ⊢ ( ( 𝑥 ∈ On ∧ 𝐵 ∈ On ) → ( 𝑧 ∈ ( 𝐵 +o 𝑥 ) → ( 𝑣 ∈ On → ( ( 𝐵 +o 𝑣 ) = 𝑧 → ( 𝑣 ∈ 𝑥 ∧ ( 𝐵 +o 𝑣 ) = 𝑧 ) ) ) ) )
104 103 imp ⊢ ( ( ( 𝑥 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝑧 ∈ ( 𝐵 +o 𝑥 ) ) → ( 𝑣 ∈ On → ( ( 𝐵 +o 𝑣 ) = 𝑧 → ( 𝑣 ∈ 𝑥 ∧ ( 𝐵 +o 𝑣 ) = 𝑧 ) ) ) )
105 104 reximdvai ⊢ ( ( ( 𝑥 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝑧 ∈ ( 𝐵 +o 𝑥 ) ) → ( ∃ 𝑣 ∈ On ( 𝐵 +o 𝑣 ) = 𝑧 → ∃ 𝑣 ∈ On ( 𝑣 ∈ 𝑥 ∧ ( 𝐵 +o 𝑣 ) = 𝑧 ) ) )
106 92 105 sylbid ⊢ ( ( ( 𝑥 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝑧 ∈ ( 𝐵 +o 𝑥 ) ) → ( ¬ 𝑧 ∈ 𝐵 → ∃ 𝑣 ∈ On ( 𝑣 ∈ 𝑥 ∧ ( 𝐵 +o 𝑣 ) = 𝑧 ) ) )
107 106 orrd ⊢ ( ( ( 𝑥 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝑧 ∈ ( 𝐵 +o 𝑥 ) ) → ( 𝑧 ∈ 𝐵 ∨ ∃ 𝑣 ∈ On ( 𝑣 ∈ 𝑥 ∧ ( 𝐵 +o 𝑣 ) = 𝑧 ) ) )
108 61 107 sylanl1 ⊢ ( ( ( Lim 𝑥 ∧ 𝐵 ∈ On ) ∧ 𝑧 ∈ ( 𝐵 +o 𝑥 ) ) → ( 𝑧 ∈ 𝐵 ∨ ∃ 𝑣 ∈ On ( 𝑣 ∈ 𝑥 ∧ ( 𝐵 +o 𝑣 ) = 𝑧 ) ) )
109 108 adantlrl ⊢ ( ( ( Lim 𝑥 ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ 𝑧 ∈ ( 𝐵 +o 𝑥 ) ) → ( 𝑧 ∈ 𝐵 ∨ ∃ 𝑣 ∈ On ( 𝑣 ∈ 𝑥 ∧ ( 𝐵 +o 𝑣 ) = 𝑧 ) ) )
110 109 adantlr ⊢ ( ( ( ( Lim 𝑥 ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ ( ∅ ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) ) ) ∧ 𝑧 ∈ ( 𝐵 +o 𝑥 ) ) → ( 𝑧 ∈ 𝐵 ∨ ∃ 𝑣 ∈ On ( 𝑣 ∈ 𝑥 ∧ ( 𝐵 +o 𝑣 ) = 𝑧 ) ) )
111 0ellim ⊢ ( Lim 𝑥 → ∅ ∈ 𝑥 )
112 om00el ⊢ ( ( 𝐴 ∈ On ∧ 𝑥 ∈ On ) → ( ∅ ∈ ( 𝐴 ·o 𝑥 ) ↔ ( ∅ ∈ 𝐴 ∧ ∅ ∈ 𝑥 ) ) )
113 112 biimprd ⊢ ( ( 𝐴 ∈ On ∧ 𝑥 ∈ On ) → ( ( ∅ ∈ 𝐴 ∧ ∅ ∈ 𝑥 ) → ∅ ∈ ( 𝐴 ·o 𝑥 ) ) )
114 111 113 sylan2i ⊢ ( ( 𝐴 ∈ On ∧ 𝑥 ∈ On ) → ( ( ∅ ∈ 𝐴 ∧ Lim 𝑥 ) → ∅ ∈ ( 𝐴 ·o 𝑥 ) ) )
115 61 114 sylan2 ⊢ ( ( 𝐴 ∈ On ∧ Lim 𝑥 ) → ( ( ∅ ∈ 𝐴 ∧ Lim 𝑥 ) → ∅ ∈ ( 𝐴 ·o 𝑥 ) ) )
116 115 exp4b ⊢ ( 𝐴 ∈ On → ( Lim 𝑥 → ( ∅ ∈ 𝐴 → ( Lim 𝑥 → ∅ ∈ ( 𝐴 ·o 𝑥 ) ) ) ) )
117 116 com4r ⊢ ( Lim 𝑥 → ( 𝐴 ∈ On → ( Lim 𝑥 → ( ∅ ∈ 𝐴 → ∅ ∈ ( 𝐴 ·o 𝑥 ) ) ) ) )
118 117 pm2.43a ⊢ ( Lim 𝑥 → ( 𝐴 ∈ On → ( ∅ ∈ 𝐴 → ∅ ∈ ( 𝐴 ·o 𝑥 ) ) ) )
119 118 imp31 ⊢ ( ( ( Lim 𝑥 ∧ 𝐴 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ∅ ∈ ( 𝐴 ·o 𝑥 ) )
120 119 a1d ⊢ ( ( ( Lim 𝑥 ∧ 𝐴 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ( 𝑧 ∈ 𝐵 → ∅ ∈ ( 𝐴 ·o 𝑥 ) ) )
121 120 adantlrr ⊢ ( ( ( Lim 𝑥 ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ ∅ ∈ 𝐴 ) → ( 𝑧 ∈ 𝐵 → ∅ ∈ ( 𝐴 ·o 𝑥 ) ) )
122 omordi ⊢ ( ( ( 𝐵 ∈ On ∧ 𝐴 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ( 𝑧 ∈ 𝐵 → ( 𝐴 ·o 𝑧 ) ∈ ( 𝐴 ·o 𝐵 ) ) )
123 122 ancom1s ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ( 𝑧 ∈ 𝐵 → ( 𝐴 ·o 𝑧 ) ∈ ( 𝐴 ·o 𝐵 ) ) )
124 onelss ⊢ ( ( 𝐴 ·o 𝐵 ) ∈ On → ( ( 𝐴 ·o 𝑧 ) ∈ ( 𝐴 ·o 𝐵 ) → ( 𝐴 ·o 𝑧 ) ⊆ ( 𝐴 ·o 𝐵 ) ) )
125 22 sseq2d ⊢ ( ( 𝐴 ·o 𝐵 ) ∈ On → ( ( 𝐴 ·o 𝑧 ) ⊆ ( ( 𝐴 ·o 𝐵 ) +o ∅ ) ↔ ( 𝐴 ·o 𝑧 ) ⊆ ( 𝐴 ·o 𝐵 ) ) )
126 124 125 sylibrd ⊢ ( ( 𝐴 ·o 𝐵 ) ∈ On → ( ( 𝐴 ·o 𝑧 ) ∈ ( 𝐴 ·o 𝐵 ) → ( 𝐴 ·o 𝑧 ) ⊆ ( ( 𝐴 ·o 𝐵 ) +o ∅ ) ) )
127 21 126 syl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐴 ·o 𝑧 ) ∈ ( 𝐴 ·o 𝐵 ) → ( 𝐴 ·o 𝑧 ) ⊆ ( ( 𝐴 ·o 𝐵 ) +o ∅ ) ) )
128 127 adantr ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ( ( 𝐴 ·o 𝑧 ) ∈ ( 𝐴 ·o 𝐵 ) → ( 𝐴 ·o 𝑧 ) ⊆ ( ( 𝐴 ·o 𝐵 ) +o ∅ ) ) )
129 123 128 syld ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ( 𝑧 ∈ 𝐵 → ( 𝐴 ·o 𝑧 ) ⊆ ( ( 𝐴 ·o 𝐵 ) +o ∅ ) ) )
130 129 adantll ⊢ ( ( ( Lim 𝑥 ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ ∅ ∈ 𝐴 ) → ( 𝑧 ∈ 𝐵 → ( 𝐴 ·o 𝑧 ) ⊆ ( ( 𝐴 ·o 𝐵 ) +o ∅ ) ) )
131 121 130 jcad ⊢ ( ( ( Lim 𝑥 ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ ∅ ∈ 𝐴 ) → ( 𝑧 ∈ 𝐵 → ( ∅ ∈ ( 𝐴 ·o 𝑥 ) ∧ ( 𝐴 ·o 𝑧 ) ⊆ ( ( 𝐴 ·o 𝐵 ) +o ∅ ) ) ) )
132 oveq2 ⊢ ( 𝑤 = ∅ → ( ( 𝐴 ·o 𝐵 ) +o 𝑤 ) = ( ( 𝐴 ·o 𝐵 ) +o ∅ ) )
133 132 sseq2d ⊢ ( 𝑤 = ∅ → ( ( 𝐴 ·o 𝑧 ) ⊆ ( ( 𝐴 ·o 𝐵 ) +o 𝑤 ) ↔ ( 𝐴 ·o 𝑧 ) ⊆ ( ( 𝐴 ·o 𝐵 ) +o ∅ ) ) )
134 133 rspcev ⊢ ( ( ∅ ∈ ( 𝐴 ·o 𝑥 ) ∧ ( 𝐴 ·o 𝑧 ) ⊆ ( ( 𝐴 ·o 𝐵 ) +o ∅ ) ) → ∃ 𝑤 ∈ ( 𝐴 ·o 𝑥 ) ( 𝐴 ·o 𝑧 ) ⊆ ( ( 𝐴 ·o 𝐵 ) +o 𝑤 ) )
135 131 134 syl6 ⊢ ( ( ( Lim 𝑥 ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ ∅ ∈ 𝐴 ) → ( 𝑧 ∈ 𝐵 → ∃ 𝑤 ∈ ( 𝐴 ·o 𝑥 ) ( 𝐴 ·o 𝑧 ) ⊆ ( ( 𝐴 ·o 𝐵 ) +o 𝑤 ) ) )
136 135 adantrr ⊢ ( ( ( Lim 𝑥 ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ ( ∅ ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) ) ) → ( 𝑧 ∈ 𝐵 → ∃ 𝑤 ∈ ( 𝐴 ·o 𝑥 ) ( 𝐴 ·o 𝑧 ) ⊆ ( ( 𝐴 ·o 𝐵 ) +o 𝑤 ) ) )
137 omordi ⊢ ( ( ( 𝑥 ∈ On ∧ 𝐴 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ( 𝑣 ∈ 𝑥 → ( 𝐴 ·o 𝑣 ) ∈ ( 𝐴 ·o 𝑥 ) ) )
138 61 137 sylanl1 ⊢ ( ( ( Lim 𝑥 ∧ 𝐴 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ( 𝑣 ∈ 𝑥 → ( 𝐴 ·o 𝑣 ) ∈ ( 𝐴 ·o 𝑥 ) ) )
139 138 adantrd ⊢ ( ( ( Lim 𝑥 ∧ 𝐴 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ( ( 𝑣 ∈ 𝑥 ∧ ( 𝐵 +o 𝑣 ) = 𝑧 ) → ( 𝐴 ·o 𝑣 ) ∈ ( 𝐴 ·o 𝑥 ) ) )
140 139 adantrr ⊢ ( ( ( Lim 𝑥 ∧ 𝐴 ∈ On ) ∧ ( ∅ ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) ) ) → ( ( 𝑣 ∈ 𝑥 ∧ ( 𝐵 +o 𝑣 ) = 𝑧 ) → ( 𝐴 ·o 𝑣 ) ∈ ( 𝐴 ·o 𝑥 ) ) )
141 oveq2 ⊢ ( 𝑦 = 𝑣 → ( 𝐵 +o 𝑦 ) = ( 𝐵 +o 𝑣 ) )
142 141 oveq2d ⊢ ( 𝑦 = 𝑣 → ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) = ( 𝐴 ·o ( 𝐵 +o 𝑣 ) ) )
143 oveq2 ⊢ ( 𝑦 = 𝑣 → ( 𝐴 ·o 𝑦 ) = ( 𝐴 ·o 𝑣 ) )
144 143 oveq2d ⊢ ( 𝑦 = 𝑣 → ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑣 ) ) )
145 142 144 eqeq12d ⊢ ( 𝑦 = 𝑣 → ( ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) ↔ ( 𝐴 ·o ( 𝐵 +o 𝑣 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑣 ) ) ) )
146 145 rspccv ⊢ ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) → ( 𝑣 ∈ 𝑥 → ( 𝐴 ·o ( 𝐵 +o 𝑣 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑣 ) ) ) )
147 oveq2 ⊢ ( ( 𝐵 +o 𝑣 ) = 𝑧 → ( 𝐴 ·o ( 𝐵 +o 𝑣 ) ) = ( 𝐴 ·o 𝑧 ) )
148 eqeq1 ⊢ ( ( 𝐴 ·o ( 𝐵 +o 𝑣 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑣 ) ) → ( ( 𝐴 ·o ( 𝐵 +o 𝑣 ) ) = ( 𝐴 ·o 𝑧 ) ↔ ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑣 ) ) = ( 𝐴 ·o 𝑧 ) ) )
149 147 148 imbitrid ⊢ ( ( 𝐴 ·o ( 𝐵 +o 𝑣 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑣 ) ) → ( ( 𝐵 +o 𝑣 ) = 𝑧 → ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑣 ) ) = ( 𝐴 ·o 𝑧 ) ) )
150 eqimss2 ⊢ ( ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑣 ) ) = ( 𝐴 ·o 𝑧 ) → ( 𝐴 ·o 𝑧 ) ⊆ ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑣 ) ) )
151 149 150 syl6 ⊢ ( ( 𝐴 ·o ( 𝐵 +o 𝑣 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑣 ) ) → ( ( 𝐵 +o 𝑣 ) = 𝑧 → ( 𝐴 ·o 𝑧 ) ⊆ ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑣 ) ) ) )
152 151 imim2i ⊢ ( ( 𝑣 ∈ 𝑥 → ( 𝐴 ·o ( 𝐵 +o 𝑣 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑣 ) ) ) → ( 𝑣 ∈ 𝑥 → ( ( 𝐵 +o 𝑣 ) = 𝑧 → ( 𝐴 ·o 𝑧 ) ⊆ ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑣 ) ) ) ) )
153 152 impd ⊢ ( ( 𝑣 ∈ 𝑥 → ( 𝐴 ·o ( 𝐵 +o 𝑣 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑣 ) ) ) → ( ( 𝑣 ∈ 𝑥 ∧ ( 𝐵 +o 𝑣 ) = 𝑧 ) → ( 𝐴 ·o 𝑧 ) ⊆ ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑣 ) ) ) )
154 146 153 syl ⊢ ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) → ( ( 𝑣 ∈ 𝑥 ∧ ( 𝐵 +o 𝑣 ) = 𝑧 ) → ( 𝐴 ·o 𝑧 ) ⊆ ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑣 ) ) ) )
155 154 ad2antll ⊢ ( ( ( Lim 𝑥 ∧ 𝐴 ∈ On ) ∧ ( ∅ ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) ) ) → ( ( 𝑣 ∈ 𝑥 ∧ ( 𝐵 +o 𝑣 ) = 𝑧 ) → ( 𝐴 ·o 𝑧 ) ⊆ ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑣 ) ) ) )
156 140 155 jcad ⊢ ( ( ( Lim 𝑥 ∧ 𝐴 ∈ On ) ∧ ( ∅ ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) ) ) → ( ( 𝑣 ∈ 𝑥 ∧ ( 𝐵 +o 𝑣 ) = 𝑧 ) → ( ( 𝐴 ·o 𝑣 ) ∈ ( 𝐴 ·o 𝑥 ) ∧ ( 𝐴 ·o 𝑧 ) ⊆ ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑣 ) ) ) ) )
157 oveq2 ⊢ ( 𝑤 = ( 𝐴 ·o 𝑣 ) → ( ( 𝐴 ·o 𝐵 ) +o 𝑤 ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑣 ) ) )
158 157 sseq2d ⊢ ( 𝑤 = ( 𝐴 ·o 𝑣 ) → ( ( 𝐴 ·o 𝑧 ) ⊆ ( ( 𝐴 ·o 𝐵 ) +o 𝑤 ) ↔ ( 𝐴 ·o 𝑧 ) ⊆ ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑣 ) ) ) )
159 158 rspcev ⊢ ( ( ( 𝐴 ·o 𝑣 ) ∈ ( 𝐴 ·o 𝑥 ) ∧ ( 𝐴 ·o 𝑧 ) ⊆ ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑣 ) ) ) → ∃ 𝑤 ∈ ( 𝐴 ·o 𝑥 ) ( 𝐴 ·o 𝑧 ) ⊆ ( ( 𝐴 ·o 𝐵 ) +o 𝑤 ) )
160 156 159 syl6 ⊢ ( ( ( Lim 𝑥 ∧ 𝐴 ∈ On ) ∧ ( ∅ ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) ) ) → ( ( 𝑣 ∈ 𝑥 ∧ ( 𝐵 +o 𝑣 ) = 𝑧 ) → ∃ 𝑤 ∈ ( 𝐴 ·o 𝑥 ) ( 𝐴 ·o 𝑧 ) ⊆ ( ( 𝐴 ·o 𝐵 ) +o 𝑤 ) ) )
161 160 rexlimdvw ⊢ ( ( ( Lim 𝑥 ∧ 𝐴 ∈ On ) ∧ ( ∅ ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) ) ) → ( ∃ 𝑣 ∈ On ( 𝑣 ∈ 𝑥 ∧ ( 𝐵 +o 𝑣 ) = 𝑧 ) → ∃ 𝑤 ∈ ( 𝐴 ·o 𝑥 ) ( 𝐴 ·o 𝑧 ) ⊆ ( ( 𝐴 ·o 𝐵 ) +o 𝑤 ) ) )
162 161 adantlrr ⊢ ( ( ( Lim 𝑥 ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ ( ∅ ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) ) ) → ( ∃ 𝑣 ∈ On ( 𝑣 ∈ 𝑥 ∧ ( 𝐵 +o 𝑣 ) = 𝑧 ) → ∃ 𝑤 ∈ ( 𝐴 ·o 𝑥 ) ( 𝐴 ·o 𝑧 ) ⊆ ( ( 𝐴 ·o 𝐵 ) +o 𝑤 ) ) )
163 136 162 jaod ⊢ ( ( ( Lim 𝑥 ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ ( ∅ ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) ) ) → ( ( 𝑧 ∈ 𝐵 ∨ ∃ 𝑣 ∈ On ( 𝑣 ∈ 𝑥 ∧ ( 𝐵 +o 𝑣 ) = 𝑧 ) ) → ∃ 𝑤 ∈ ( 𝐴 ·o 𝑥 ) ( 𝐴 ·o 𝑧 ) ⊆ ( ( 𝐴 ·o 𝐵 ) +o 𝑤 ) ) )
164 163 adantr ⊢ ( ( ( ( Lim 𝑥 ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ ( ∅ ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) ) ) ∧ 𝑧 ∈ ( 𝐵 +o 𝑥 ) ) → ( ( 𝑧 ∈ 𝐵 ∨ ∃ 𝑣 ∈ On ( 𝑣 ∈ 𝑥 ∧ ( 𝐵 +o 𝑣 ) = 𝑧 ) ) → ∃ 𝑤 ∈ ( 𝐴 ·o 𝑥 ) ( 𝐴 ·o 𝑧 ) ⊆ ( ( 𝐴 ·o 𝐵 ) +o 𝑤 ) ) )
165 110 164 mpd ⊢ ( ( ( ( Lim 𝑥 ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ ( ∅ ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) ) ) ∧ 𝑧 ∈ ( 𝐵 +o 𝑥 ) ) → ∃ 𝑤 ∈ ( 𝐴 ·o 𝑥 ) ( 𝐴 ·o 𝑧 ) ⊆ ( ( 𝐴 ·o 𝐵 ) +o 𝑤 ) )
166 165 ralrimiva ⊢ ( ( ( Lim 𝑥 ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ ( ∅ ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) ) ) → ∀ 𝑧 ∈ ( 𝐵 +o 𝑥 ) ∃ 𝑤 ∈ ( 𝐴 ·o 𝑥 ) ( 𝐴 ·o 𝑧 ) ⊆ ( ( 𝐴 ·o 𝐵 ) +o 𝑤 ) )
167 iunss2 ⊢ ( ∀ 𝑧 ∈ ( 𝐵 +o 𝑥 ) ∃ 𝑤 ∈ ( 𝐴 ·o 𝑥 ) ( 𝐴 ·o 𝑧 ) ⊆ ( ( 𝐴 ·o 𝐵 ) +o 𝑤 ) → ∪ 𝑧 ∈ ( 𝐵 +o 𝑥 ) ( 𝐴 ·o 𝑧 ) ⊆ ∪ 𝑤 ∈ ( 𝐴 ·o 𝑥 ) ( ( 𝐴 ·o 𝐵 ) +o 𝑤 ) )
168 166 167 syl ⊢ ( ( ( Lim 𝑥 ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ ( ∅ ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) ) ) → ∪ 𝑧 ∈ ( 𝐵 +o 𝑥 ) ( 𝐴 ·o 𝑧 ) ⊆ ∪ 𝑤 ∈ ( 𝐴 ·o 𝑥 ) ( ( 𝐴 ·o 𝐵 ) +o 𝑤 ) )
169 omordlim ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝑥 ∈ V ∧ Lim 𝑥 ) ) ∧ 𝑤 ∈ ( 𝐴 ·o 𝑥 ) ) → ∃ 𝑣 ∈ 𝑥 𝑤 ∈ ( 𝐴 ·o 𝑣 ) )
170 169 ex ⊢ ( ( 𝐴 ∈ On ∧ ( 𝑥 ∈ V ∧ Lim 𝑥 ) ) → ( 𝑤 ∈ ( 𝐴 ·o 𝑥 ) → ∃ 𝑣 ∈ 𝑥 𝑤 ∈ ( 𝐴 ·o 𝑣 ) ) )
171 59 170 mpanr1 ⊢ ( ( 𝐴 ∈ On ∧ Lim 𝑥 ) → ( 𝑤 ∈ ( 𝐴 ·o 𝑥 ) → ∃ 𝑣 ∈ 𝑥 𝑤 ∈ ( 𝐴 ·o 𝑣 ) ) )
172 171 ancoms ⊢ ( ( Lim 𝑥 ∧ 𝐴 ∈ On ) → ( 𝑤 ∈ ( 𝐴 ·o 𝑥 ) → ∃ 𝑣 ∈ 𝑥 𝑤 ∈ ( 𝐴 ·o 𝑣 ) ) )
173 172 imp ⊢ ( ( ( Lim 𝑥 ∧ 𝐴 ∈ On ) ∧ 𝑤 ∈ ( 𝐴 ·o 𝑥 ) ) → ∃ 𝑣 ∈ 𝑥 𝑤 ∈ ( 𝐴 ·o 𝑣 ) )
174 173 adantlrr ⊢ ( ( ( Lim 𝑥 ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ 𝑤 ∈ ( 𝐴 ·o 𝑥 ) ) → ∃ 𝑣 ∈ 𝑥 𝑤 ∈ ( 𝐴 ·o 𝑣 ) )
175 174 adantlr ⊢ ( ( ( ( Lim 𝑥 ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) ) ∧ 𝑤 ∈ ( 𝐴 ·o 𝑥 ) ) → ∃ 𝑣 ∈ 𝑥 𝑤 ∈ ( 𝐴 ·o 𝑣 ) )
176 oaordi ⊢ ( ( 𝑥 ∈ On ∧ 𝐵 ∈ On ) → ( 𝑣 ∈ 𝑥 → ( 𝐵 +o 𝑣 ) ∈ ( 𝐵 +o 𝑥 ) ) )
177 61 176 sylan ⊢ ( ( Lim 𝑥 ∧ 𝐵 ∈ On ) → ( 𝑣 ∈ 𝑥 → ( 𝐵 +o 𝑣 ) ∈ ( 𝐵 +o 𝑥 ) ) )
178 177 imp ⊢ ( ( ( Lim 𝑥 ∧ 𝐵 ∈ On ) ∧ 𝑣 ∈ 𝑥 ) → ( 𝐵 +o 𝑣 ) ∈ ( 𝐵 +o 𝑥 ) )
179 178 adantlrl ⊢ ( ( ( Lim 𝑥 ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ 𝑣 ∈ 𝑥 ) → ( 𝐵 +o 𝑣 ) ∈ ( 𝐵 +o 𝑥 ) )
180 179 a1d ⊢ ( ( ( Lim 𝑥 ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ 𝑣 ∈ 𝑥 ) → ( 𝑤 ∈ ( 𝐴 ·o 𝑣 ) → ( 𝐵 +o 𝑣 ) ∈ ( 𝐵 +o 𝑥 ) ) )
181 180 adantlr ⊢ ( ( ( ( Lim 𝑥 ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) ) ∧ 𝑣 ∈ 𝑥 ) → ( 𝑤 ∈ ( 𝐴 ·o 𝑣 ) → ( 𝐵 +o 𝑣 ) ∈ ( 𝐵 +o 𝑥 ) ) )
182 limord ⊢ ( Lim 𝑥 → Ord 𝑥 )
183 ordelon ⊢ ( ( Ord 𝑥 ∧ 𝑣 ∈ 𝑥 ) → 𝑣 ∈ On )
184 182 183 sylan ⊢ ( ( Lim 𝑥 ∧ 𝑣 ∈ 𝑥 ) → 𝑣 ∈ On )
185 omcl ⊢ ( ( 𝐴 ∈ On ∧ 𝑣 ∈ On ) → ( 𝐴 ·o 𝑣 ) ∈ On )
186 185 ancoms ⊢ ( ( 𝑣 ∈ On ∧ 𝐴 ∈ On ) → ( 𝐴 ·o 𝑣 ) ∈ On )
187 186 adantrr ⊢ ( ( 𝑣 ∈ On ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) → ( 𝐴 ·o 𝑣 ) ∈ On )
188 21 adantl ⊢ ( ( 𝑣 ∈ On ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) → ( 𝐴 ·o 𝐵 ) ∈ On )
189 oaordi ⊢ ( ( ( 𝐴 ·o 𝑣 ) ∈ On ∧ ( 𝐴 ·o 𝐵 ) ∈ On ) → ( 𝑤 ∈ ( 𝐴 ·o 𝑣 ) → ( ( 𝐴 ·o 𝐵 ) +o 𝑤 ) ∈ ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑣 ) ) ) )
190 187 188 189 syl2anc ⊢ ( ( 𝑣 ∈ On ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) → ( 𝑤 ∈ ( 𝐴 ·o 𝑣 ) → ( ( 𝐴 ·o 𝐵 ) +o 𝑤 ) ∈ ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑣 ) ) ) )
191 184 190 sylan ⊢ ( ( ( Lim 𝑥 ∧ 𝑣 ∈ 𝑥 ) ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) → ( 𝑤 ∈ ( 𝐴 ·o 𝑣 ) → ( ( 𝐴 ·o 𝐵 ) +o 𝑤 ) ∈ ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑣 ) ) ) )
192 191 an32s ⊢ ( ( ( Lim 𝑥 ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ 𝑣 ∈ 𝑥 ) → ( 𝑤 ∈ ( 𝐴 ·o 𝑣 ) → ( ( 𝐴 ·o 𝐵 ) +o 𝑤 ) ∈ ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑣 ) ) ) )
193 192 adantlr ⊢ ( ( ( ( Lim 𝑥 ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) ) ∧ 𝑣 ∈ 𝑥 ) → ( 𝑤 ∈ ( 𝐴 ·o 𝑣 ) → ( ( 𝐴 ·o 𝐵 ) +o 𝑤 ) ∈ ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑣 ) ) ) )
194 145 rspccva ⊢ ( ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) ∧ 𝑣 ∈ 𝑥 ) → ( 𝐴 ·o ( 𝐵 +o 𝑣 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑣 ) ) )
195 194 eleq2d ⊢ ( ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) ∧ 𝑣 ∈ 𝑥 ) → ( ( ( 𝐴 ·o 𝐵 ) +o 𝑤 ) ∈ ( 𝐴 ·o ( 𝐵 +o 𝑣 ) ) ↔ ( ( 𝐴 ·o 𝐵 ) +o 𝑤 ) ∈ ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑣 ) ) ) )
196 195 adantll ⊢ ( ( ( ( Lim 𝑥 ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) ) ∧ 𝑣 ∈ 𝑥 ) → ( ( ( 𝐴 ·o 𝐵 ) +o 𝑤 ) ∈ ( 𝐴 ·o ( 𝐵 +o 𝑣 ) ) ↔ ( ( 𝐴 ·o 𝐵 ) +o 𝑤 ) ∈ ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑣 ) ) ) )
197 193 196 sylibrd ⊢ ( ( ( ( Lim 𝑥 ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) ) ∧ 𝑣 ∈ 𝑥 ) → ( 𝑤 ∈ ( 𝐴 ·o 𝑣 ) → ( ( 𝐴 ·o 𝐵 ) +o 𝑤 ) ∈ ( 𝐴 ·o ( 𝐵 +o 𝑣 ) ) ) )
198 oacl ⊢ ( ( 𝐵 ∈ On ∧ 𝑣 ∈ On ) → ( 𝐵 +o 𝑣 ) ∈ On )
199 198 ancoms ⊢ ( ( 𝑣 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐵 +o 𝑣 ) ∈ On )
200 omcl ⊢ ( ( 𝐴 ∈ On ∧ ( 𝐵 +o 𝑣 ) ∈ On ) → ( 𝐴 ·o ( 𝐵 +o 𝑣 ) ) ∈ On )
201 199 200 sylan2 ⊢ ( ( 𝐴 ∈ On ∧ ( 𝑣 ∈ On ∧ 𝐵 ∈ On ) ) → ( 𝐴 ·o ( 𝐵 +o 𝑣 ) ) ∈ On )
202 201 an12s ⊢ ( ( 𝑣 ∈ On ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) → ( 𝐴 ·o ( 𝐵 +o 𝑣 ) ) ∈ On )
203 184 202 sylan ⊢ ( ( ( Lim 𝑥 ∧ 𝑣 ∈ 𝑥 ) ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) → ( 𝐴 ·o ( 𝐵 +o 𝑣 ) ) ∈ On )
204 203 an32s ⊢ ( ( ( Lim 𝑥 ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ 𝑣 ∈ 𝑥 ) → ( 𝐴 ·o ( 𝐵 +o 𝑣 ) ) ∈ On )
205 onelss ⊢ ( ( 𝐴 ·o ( 𝐵 +o 𝑣 ) ) ∈ On → ( ( ( 𝐴 ·o 𝐵 ) +o 𝑤 ) ∈ ( 𝐴 ·o ( 𝐵 +o 𝑣 ) ) → ( ( 𝐴 ·o 𝐵 ) +o 𝑤 ) ⊆ ( 𝐴 ·o ( 𝐵 +o 𝑣 ) ) ) )
206 204 205 syl ⊢ ( ( ( Lim 𝑥 ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ 𝑣 ∈ 𝑥 ) → ( ( ( 𝐴 ·o 𝐵 ) +o 𝑤 ) ∈ ( 𝐴 ·o ( 𝐵 +o 𝑣 ) ) → ( ( 𝐴 ·o 𝐵 ) +o 𝑤 ) ⊆ ( 𝐴 ·o ( 𝐵 +o 𝑣 ) ) ) )
207 206 adantlr ⊢ ( ( ( ( Lim 𝑥 ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) ) ∧ 𝑣 ∈ 𝑥 ) → ( ( ( 𝐴 ·o 𝐵 ) +o 𝑤 ) ∈ ( 𝐴 ·o ( 𝐵 +o 𝑣 ) ) → ( ( 𝐴 ·o 𝐵 ) +o 𝑤 ) ⊆ ( 𝐴 ·o ( 𝐵 +o 𝑣 ) ) ) )
208 197 207 syld ⊢ ( ( ( ( Lim 𝑥 ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) ) ∧ 𝑣 ∈ 𝑥 ) → ( 𝑤 ∈ ( 𝐴 ·o 𝑣 ) → ( ( 𝐴 ·o 𝐵 ) +o 𝑤 ) ⊆ ( 𝐴 ·o ( 𝐵 +o 𝑣 ) ) ) )
209 181 208 jcad ⊢ ( ( ( ( Lim 𝑥 ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) ) ∧ 𝑣 ∈ 𝑥 ) → ( 𝑤 ∈ ( 𝐴 ·o 𝑣 ) → ( ( 𝐵 +o 𝑣 ) ∈ ( 𝐵 +o 𝑥 ) ∧ ( ( 𝐴 ·o 𝐵 ) +o 𝑤 ) ⊆ ( 𝐴 ·o ( 𝐵 +o 𝑣 ) ) ) ) )
210 oveq2 ⊢ ( 𝑧 = ( 𝐵 +o 𝑣 ) → ( 𝐴 ·o 𝑧 ) = ( 𝐴 ·o ( 𝐵 +o 𝑣 ) ) )
211 210 sseq2d ⊢ ( 𝑧 = ( 𝐵 +o 𝑣 ) → ( ( ( 𝐴 ·o 𝐵 ) +o 𝑤 ) ⊆ ( 𝐴 ·o 𝑧 ) ↔ ( ( 𝐴 ·o 𝐵 ) +o 𝑤 ) ⊆ ( 𝐴 ·o ( 𝐵 +o 𝑣 ) ) ) )
212 211 rspcev ⊢ ( ( ( 𝐵 +o 𝑣 ) ∈ ( 𝐵 +o 𝑥 ) ∧ ( ( 𝐴 ·o 𝐵 ) +o 𝑤 ) ⊆ ( 𝐴 ·o ( 𝐵 +o 𝑣 ) ) ) → ∃ 𝑧 ∈ ( 𝐵 +o 𝑥 ) ( ( 𝐴 ·o 𝐵 ) +o 𝑤 ) ⊆ ( 𝐴 ·o 𝑧 ) )
213 209 212 syl6 ⊢ ( ( ( ( Lim 𝑥 ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) ) ∧ 𝑣 ∈ 𝑥 ) → ( 𝑤 ∈ ( 𝐴 ·o 𝑣 ) → ∃ 𝑧 ∈ ( 𝐵 +o 𝑥 ) ( ( 𝐴 ·o 𝐵 ) +o 𝑤 ) ⊆ ( 𝐴 ·o 𝑧 ) ) )
214 213 rexlimdva ⊢ ( ( ( Lim 𝑥 ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) ) → ( ∃ 𝑣 ∈ 𝑥 𝑤 ∈ ( 𝐴 ·o 𝑣 ) → ∃ 𝑧 ∈ ( 𝐵 +o 𝑥 ) ( ( 𝐴 ·o 𝐵 ) +o 𝑤 ) ⊆ ( 𝐴 ·o 𝑧 ) ) )
215 214 adantr ⊢ ( ( ( ( Lim 𝑥 ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) ) ∧ 𝑤 ∈ ( 𝐴 ·o 𝑥 ) ) → ( ∃ 𝑣 ∈ 𝑥 𝑤 ∈ ( 𝐴 ·o 𝑣 ) → ∃ 𝑧 ∈ ( 𝐵 +o 𝑥 ) ( ( 𝐴 ·o 𝐵 ) +o 𝑤 ) ⊆ ( 𝐴 ·o 𝑧 ) ) )
216 175 215 mpd ⊢ ( ( ( ( Lim 𝑥 ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) ) ∧ 𝑤 ∈ ( 𝐴 ·o 𝑥 ) ) → ∃ 𝑧 ∈ ( 𝐵 +o 𝑥 ) ( ( 𝐴 ·o 𝐵 ) +o 𝑤 ) ⊆ ( 𝐴 ·o 𝑧 ) )
217 216 ralrimiva ⊢ ( ( ( Lim 𝑥 ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) ) → ∀ 𝑤 ∈ ( 𝐴 ·o 𝑥 ) ∃ 𝑧 ∈ ( 𝐵 +o 𝑥 ) ( ( 𝐴 ·o 𝐵 ) +o 𝑤 ) ⊆ ( 𝐴 ·o 𝑧 ) )
218 iunss2 ⊢ ( ∀ 𝑤 ∈ ( 𝐴 ·o 𝑥 ) ∃ 𝑧 ∈ ( 𝐵 +o 𝑥 ) ( ( 𝐴 ·o 𝐵 ) +o 𝑤 ) ⊆ ( 𝐴 ·o 𝑧 ) → ∪ 𝑤 ∈ ( 𝐴 ·o 𝑥 ) ( ( 𝐴 ·o 𝐵 ) +o 𝑤 ) ⊆ ∪ 𝑧 ∈ ( 𝐵 +o 𝑥 ) ( 𝐴 ·o 𝑧 ) )
219 217 218 syl ⊢ ( ( ( Lim 𝑥 ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) ) → ∪ 𝑤 ∈ ( 𝐴 ·o 𝑥 ) ( ( 𝐴 ·o 𝐵 ) +o 𝑤 ) ⊆ ∪ 𝑧 ∈ ( 𝐵 +o 𝑥 ) ( 𝐴 ·o 𝑧 ) )
220 219 adantrl ⊢ ( ( ( Lim 𝑥 ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ ( ∅ ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) ) ) → ∪ 𝑤 ∈ ( 𝐴 ·o 𝑥 ) ( ( 𝐴 ·o 𝐵 ) +o 𝑤 ) ⊆ ∪ 𝑧 ∈ ( 𝐵 +o 𝑥 ) ( 𝐴 ·o 𝑧 ) )
221 168 220 eqssd ⊢ ( ( ( Lim 𝑥 ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ ( ∅ ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) ) ) → ∪ 𝑧 ∈ ( 𝐵 +o 𝑥 ) ( 𝐴 ·o 𝑧 ) = ∪ 𝑤 ∈ ( 𝐴 ·o 𝑥 ) ( ( 𝐴 ·o 𝐵 ) +o 𝑤 ) )
222 oalimcl ⊢ ( ( 𝐵 ∈ On ∧ ( 𝑥 ∈ V ∧ Lim 𝑥 ) ) → Lim ( 𝐵 +o 𝑥 ) )
223 59 222 mpanr1 ⊢ ( ( 𝐵 ∈ On ∧ Lim 𝑥 ) → Lim ( 𝐵 +o 𝑥 ) )
224 223 ancoms ⊢ ( ( Lim 𝑥 ∧ 𝐵 ∈ On ) → Lim ( 𝐵 +o 𝑥 ) )
225 224 anim2i ⊢ ( ( 𝐴 ∈ On ∧ ( Lim 𝑥 ∧ 𝐵 ∈ On ) ) → ( 𝐴 ∈ On ∧ Lim ( 𝐵 +o 𝑥 ) ) )
226 225 an12s ⊢ ( ( Lim 𝑥 ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) → ( 𝐴 ∈ On ∧ Lim ( 𝐵 +o 𝑥 ) ) )
227 ovex ⊢ ( 𝐵 +o 𝑥 ) ∈ V
228 omlim ⊢ ( ( 𝐴 ∈ On ∧ ( ( 𝐵 +o 𝑥 ) ∈ V ∧ Lim ( 𝐵 +o 𝑥 ) ) ) → ( 𝐴 ·o ( 𝐵 +o 𝑥 ) ) = ∪ 𝑧 ∈ ( 𝐵 +o 𝑥 ) ( 𝐴 ·o 𝑧 ) )
229 227 228 mpanr1 ⊢ ( ( 𝐴 ∈ On ∧ Lim ( 𝐵 +o 𝑥 ) ) → ( 𝐴 ·o ( 𝐵 +o 𝑥 ) ) = ∪ 𝑧 ∈ ( 𝐵 +o 𝑥 ) ( 𝐴 ·o 𝑧 ) )
230 226 229 syl ⊢ ( ( Lim 𝑥 ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) → ( 𝐴 ·o ( 𝐵 +o 𝑥 ) ) = ∪ 𝑧 ∈ ( 𝐵 +o 𝑥 ) ( 𝐴 ·o 𝑧 ) )
231 230 adantr ⊢ ( ( ( Lim 𝑥 ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ ( ∅ ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) ) ) → ( 𝐴 ·o ( 𝐵 +o 𝑥 ) ) = ∪ 𝑧 ∈ ( 𝐵 +o 𝑥 ) ( 𝐴 ·o 𝑧 ) )
232 21 ad2antlr ⊢ ( ( ( Lim 𝑥 ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ ∅ ∈ 𝐴 ) → ( 𝐴 ·o 𝐵 ) ∈ On )
233 59 jctl ⊢ ( Lim 𝑥 → ( 𝑥 ∈ V ∧ Lim 𝑥 ) )
234 233 anim1ci ⊢ ( ( Lim 𝑥 ∧ 𝐴 ∈ On ) → ( 𝐴 ∈ On ∧ ( 𝑥 ∈ V ∧ Lim 𝑥 ) ) )
235 omlimcl ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝑥 ∈ V ∧ Lim 𝑥 ) ) ∧ ∅ ∈ 𝐴 ) → Lim ( 𝐴 ·o 𝑥 ) )
236 234 235 sylan ⊢ ( ( ( Lim 𝑥 ∧ 𝐴 ∈ On ) ∧ ∅ ∈ 𝐴 ) → Lim ( 𝐴 ·o 𝑥 ) )
237 236 adantlrr ⊢ ( ( ( Lim 𝑥 ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ ∅ ∈ 𝐴 ) → Lim ( 𝐴 ·o 𝑥 ) )
238 ovex ⊢ ( 𝐴 ·o 𝑥 ) ∈ V
239 237 238 jctil ⊢ ( ( ( Lim 𝑥 ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ ∅ ∈ 𝐴 ) → ( ( 𝐴 ·o 𝑥 ) ∈ V ∧ Lim ( 𝐴 ·o 𝑥 ) ) )
240 oalim ⊢ ( ( ( 𝐴 ·o 𝐵 ) ∈ On ∧ ( ( 𝐴 ·o 𝑥 ) ∈ V ∧ Lim ( 𝐴 ·o 𝑥 ) ) ) → ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑥 ) ) = ∪ 𝑤 ∈ ( 𝐴 ·o 𝑥 ) ( ( 𝐴 ·o 𝐵 ) +o 𝑤 ) )
241 232 239 240 syl2anc ⊢ ( ( ( Lim 𝑥 ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ ∅ ∈ 𝐴 ) → ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑥 ) ) = ∪ 𝑤 ∈ ( 𝐴 ·o 𝑥 ) ( ( 𝐴 ·o 𝐵 ) +o 𝑤 ) )
242 241 adantrr ⊢ ( ( ( Lim 𝑥 ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ ( ∅ ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) ) ) → ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑥 ) ) = ∪ 𝑤 ∈ ( 𝐴 ·o 𝑥 ) ( ( 𝐴 ·o 𝐵 ) +o 𝑤 ) )
243 221 231 242 3eqtr4d ⊢ ( ( ( Lim 𝑥 ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ ( ∅ ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) ) ) → ( 𝐴 ·o ( 𝐵 +o 𝑥 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑥 ) ) )
244 243 exp43 ⊢ ( Lim 𝑥 → ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ∅ ∈ 𝐴 → ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) → ( 𝐴 ·o ( 𝐵 +o 𝑥 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑥 ) ) ) ) ) )
245 244 com3l ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ∅ ∈ 𝐴 → ( Lim 𝑥 → ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) → ( 𝐴 ·o ( 𝐵 +o 𝑥 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑥 ) ) ) ) ) )
246 245 imp ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ( Lim 𝑥 → ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) → ( 𝐴 ·o ( 𝐵 +o 𝑥 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑥 ) ) ) ) )
247 84 246 oe0lem ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( Lim 𝑥 → ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) → ( 𝐴 ·o ( 𝐵 +o 𝑥 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑥 ) ) ) ) )
248 247 com12 ⊢ ( Lim 𝑥 → ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) → ( 𝐴 ·o ( 𝐵 +o 𝑥 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑥 ) ) ) ) )
249 5 10 15 20 30 58 248 tfinds3 ⊢ ( 𝐶 ∈ On → ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ·o ( 𝐵 +o 𝐶 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝐶 ) ) ) )
250 249 expdcom ⊢ ( 𝐴 ∈ On → ( 𝐵 ∈ On → ( 𝐶 ∈ On → ( 𝐴 ·o ( 𝐵 +o 𝐶 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝐶 ) ) ) ) )
251 250 3imp ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ·o ( 𝐵 +o 𝐶 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝐶 ) ) )