Metamath Proof Explorer

Theorem omcl3g

Description: Closure law for ordinal multiplication. (Contributed by RP, 14-Jan-2025)

Ref Expression
Assertion omcl3g ⊢ A ∈ C ∧ B ∈ C ∧ C ∈ 3 𝑜 ∨ C = ω ↑ 𝑜 ω ↑ 𝑜 D ∧ D ∈ On → A ⋅ 𝑜 B ∈ C

Proof

Step Hyp Ref Expression
1 eltpi ⊢ C ∈ ∅ 1 𝑜 2 𝑜 → C = ∅ ∨ C = 1 𝑜 ∨ C = 2 𝑜
2 df-3o ⊢ 3 𝑜 = suc ⁡ 2 𝑜
3 df2o3 ⊢ 2 𝑜 = ∅ 1 𝑜
4 3 uneq1i ⊢ 2 𝑜 ∪ 2 𝑜 = ∅ 1 𝑜 ∪ 2 𝑜
5 df-suc ⊢ suc ⁡ 2 𝑜 = 2 𝑜 ∪ 2 𝑜
6 df-tp ⊢ ∅ 1 𝑜 2 𝑜 = ∅ 1 𝑜 ∪ 2 𝑜
7 4 5 6 3eqtr4i ⊢ suc ⁡ 2 𝑜 = ∅ 1 𝑜 2 𝑜
8 2 7 eqtri ⊢ 3 𝑜 = ∅ 1 𝑜 2 𝑜
9 1 8 eleq2s ⊢ C ∈ 3 𝑜 → C = ∅ ∨ C = 1 𝑜 ∨ C = 2 𝑜
10 orc ⊢ C = ∅ → C = ∅ ∨ C = ω ↑ 𝑜 ω ↑ 𝑜 C ∧ C ∈ On
11 omcl2 ⊢ A ∈ C ∧ B ∈ C ∧ C = ∅ ∨ C = ω ↑ 𝑜 ω ↑ 𝑜 C ∧ C ∈ On → A ⋅ 𝑜 B ∈ C
12 10 11 sylan2 ⊢ A ∈ C ∧ B ∈ C ∧ C = ∅ → A ⋅ 𝑜 B ∈ C
13 12 ex ⊢ A ∈ C ∧ B ∈ C → C = ∅ → A ⋅ 𝑜 B ∈ C
14 el1o ⊢ A ∈ 1 𝑜 ↔ A = ∅
15 el1o ⊢ B ∈ 1 𝑜 ↔ B = ∅
16 oveq12 ⊢ A = ∅ ∧ B = ∅ → A ⋅ 𝑜 B = ∅ ⋅ 𝑜 ∅
17 0elon ⊢ ∅ ∈ On
18 om0 ⊢ ∅ ∈ On → ∅ ⋅ 𝑜 ∅ = ∅
19 17 18 ax-mp ⊢ ∅ ⋅ 𝑜 ∅ = ∅
20 0lt1o ⊢ ∅ ∈ 1 𝑜
21 19 20 eqeltri ⊢ ∅ ⋅ 𝑜 ∅ ∈ 1 𝑜
22 16 21 eqeltrdi ⊢ A = ∅ ∧ B = ∅ → A ⋅ 𝑜 B ∈ 1 𝑜
23 14 15 22 syl2anb ⊢ A ∈ 1 𝑜 ∧ B ∈ 1 𝑜 → A ⋅ 𝑜 B ∈ 1 𝑜
24 23 a1i ⊢ C = 1 𝑜 → A ∈ 1 𝑜 ∧ B ∈ 1 𝑜 → A ⋅ 𝑜 B ∈ 1 𝑜
25 eleq2 ⊢ C = 1 𝑜 → A ∈ C ↔ A ∈ 1 𝑜
26 eleq2 ⊢ C = 1 𝑜 → B ∈ C ↔ B ∈ 1 𝑜
27 25 26 anbi12d ⊢ C = 1 𝑜 → A ∈ C ∧ B ∈ C ↔ A ∈ 1 𝑜 ∧ B ∈ 1 𝑜
28 eleq2 ⊢ C = 1 𝑜 → A ⋅ 𝑜 B ∈ C ↔ A ⋅ 𝑜 B ∈ 1 𝑜
29 24 27 28 3imtr4d ⊢ C = 1 𝑜 → A ∈ C ∧ B ∈ C → A ⋅ 𝑜 B ∈ C
30 29 com12 ⊢ A ∈ C ∧ B ∈ C → C = 1 𝑜 → A ⋅ 𝑜 B ∈ C
31 elpri ⊢ A ∈ ∅ 1 𝑜 → A = ∅ ∨ A = 1 𝑜
32 31 3 eleq2s ⊢ A ∈ 2 𝑜 → A = ∅ ∨ A = 1 𝑜
33 elpri ⊢ B ∈ ∅ 1 𝑜 → B = ∅ ∨ B = 1 𝑜
34 33 3 eleq2s ⊢ B ∈ 2 𝑜 → B = ∅ ∨ B = 1 𝑜
35 0ex ⊢ ∅ ∈ V
36 35 prid1 ⊢ ∅ ∈ ∅ 1 𝑜
37 36 19 3 3eltr4i ⊢ ∅ ⋅ 𝑜 ∅ ∈ 2 𝑜
38 16 37 eqeltrdi ⊢ A = ∅ ∧ B = ∅ → A ⋅ 𝑜 B ∈ 2 𝑜
39 oveq12 ⊢ A = 1 𝑜 ∧ B = ∅ → A ⋅ 𝑜 B = 1 𝑜 ⋅ 𝑜 ∅
40 1on ⊢ 1 𝑜 ∈ On
41 om0 ⊢ 1 𝑜 ∈ On → 1 𝑜 ⋅ 𝑜 ∅ = ∅
42 40 41 ax-mp ⊢ 1 𝑜 ⋅ 𝑜 ∅ = ∅
43 36 42 3 3eltr4i ⊢ 1 𝑜 ⋅ 𝑜 ∅ ∈ 2 𝑜
44 39 43 eqeltrdi ⊢ A = 1 𝑜 ∧ B = ∅ → A ⋅ 𝑜 B ∈ 2 𝑜
45 oveq12 ⊢ A = ∅ ∧ B = 1 𝑜 → A ⋅ 𝑜 B = ∅ ⋅ 𝑜 1 𝑜
46 om0r ⊢ 1 𝑜 ∈ On → ∅ ⋅ 𝑜 1 𝑜 = ∅
47 40 46 ax-mp ⊢ ∅ ⋅ 𝑜 1 𝑜 = ∅
48 36 47 3 3eltr4i ⊢ ∅ ⋅ 𝑜 1 𝑜 ∈ 2 𝑜
49 45 48 eqeltrdi ⊢ A = ∅ ∧ B = 1 𝑜 → A ⋅ 𝑜 B ∈ 2 𝑜
50 oveq12 ⊢ A = 1 𝑜 ∧ B = 1 𝑜 → A ⋅ 𝑜 B = 1 𝑜 ⋅ 𝑜 1 𝑜
51 1oelpr ⊢ 1 𝑜 ∈ ∅ 1 𝑜
52 om1 ⊢ 1 𝑜 ∈ On → 1 𝑜 ⋅ 𝑜 1 𝑜 = 1 𝑜
53 40 52 ax-mp ⊢ 1 𝑜 ⋅ 𝑜 1 𝑜 = 1 𝑜
54 51 53 3 3eltr4i ⊢ 1 𝑜 ⋅ 𝑜 1 𝑜 ∈ 2 𝑜
55 50 54 eqeltrdi ⊢ A = 1 𝑜 ∧ B = 1 𝑜 → A ⋅ 𝑜 B ∈ 2 𝑜
56 38 44 49 55 ccase ⊢ A = ∅ ∨ A = 1 𝑜 ∧ B = ∅ ∨ B = 1 𝑜 → A ⋅ 𝑜 B ∈ 2 𝑜
57 32 34 56 syl2an ⊢ A ∈ 2 𝑜 ∧ B ∈ 2 𝑜 → A ⋅ 𝑜 B ∈ 2 𝑜
58 57 a1i ⊢ C = 2 𝑜 → A ∈ 2 𝑜 ∧ B ∈ 2 𝑜 → A ⋅ 𝑜 B ∈ 2 𝑜
59 eleq2 ⊢ C = 2 𝑜 → A ∈ C ↔ A ∈ 2 𝑜
60 eleq2 ⊢ C = 2 𝑜 → B ∈ C ↔ B ∈ 2 𝑜
61 59 60 anbi12d ⊢ C = 2 𝑜 → A ∈ C ∧ B ∈ C ↔ A ∈ 2 𝑜 ∧ B ∈ 2 𝑜
62 eleq2 ⊢ C = 2 𝑜 → A ⋅ 𝑜 B ∈ C ↔ A ⋅ 𝑜 B ∈ 2 𝑜
63 58 61 62 3imtr4d ⊢ C = 2 𝑜 → A ∈ C ∧ B ∈ C → A ⋅ 𝑜 B ∈ C
64 63 com12 ⊢ A ∈ C ∧ B ∈ C → C = 2 𝑜 → A ⋅ 𝑜 B ∈ C
65 13 30 64 3jaod ⊢ A ∈ C ∧ B ∈ C → C = ∅ ∨ C = 1 𝑜 ∨ C = 2 𝑜 → A ⋅ 𝑜 B ∈ C
66 9 65 syl5 ⊢ A ∈ C ∧ B ∈ C → C ∈ 3 𝑜 → A ⋅ 𝑜 B ∈ C
67 olc ⊢ C = ω ↑ 𝑜 ω ↑ 𝑜 D ∧ D ∈ On → C = ∅ ∨ C = ω ↑ 𝑜 ω ↑ 𝑜 D ∧ D ∈ On
68 omcl2 ⊢ A ∈ C ∧ B ∈ C ∧ C = ∅ ∨ C = ω ↑ 𝑜 ω ↑ 𝑜 D ∧ D ∈ On → A ⋅ 𝑜 B ∈ C
69 67 68 sylan2 ⊢ A ∈ C ∧ B ∈ C ∧ C = ω ↑ 𝑜 ω ↑ 𝑜 D ∧ D ∈ On → A ⋅ 𝑜 B ∈ C
70 69 ex ⊢ A ∈ C ∧ B ∈ C → C = ω ↑ 𝑜 ω ↑ 𝑜 D ∧ D ∈ On → A ⋅ 𝑜 B ∈ C
71 66 70 jaod ⊢ A ∈ C ∧ B ∈ C → C ∈ 3 𝑜 ∨ C = ω ↑ 𝑜 ω ↑ 𝑜 D ∧ D ∈ On → A ⋅ 𝑜 B ∈ C
72 71 imp ⊢ A ∈ C ∧ B ∈ C ∧ C ∈ 3 𝑜 ∨ C = ω ↑ 𝑜 ω ↑ 𝑜 D ∧ D ∈ On → A ⋅ 𝑜 B ∈ C