Metamath Proof Explorer

Theorem omass

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

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

Proof

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