Metamath Proof Explorer

Theorem omcl

Description: Closure law for ordinal multiplication. Proposition 8.16 of TakeutiZaring p. 57. Remark 2.8 of Schloeder p. 5. (Contributed by NM, 3-Aug-2004) (Proof shortened by Andrew Salmon, 22-Oct-2011)

Ref Expression
Assertion omcl ⊢ A ∈ On ∧ B ∈ On → A ⋅ 𝑜 B ∈ On

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ x = ∅ → A ⋅ 𝑜 x = A ⋅ 𝑜 ∅
2 1 eleq1d ⊢ x = ∅ → A ⋅ 𝑜 x ∈ On ↔ A ⋅ 𝑜 ∅ ∈ On
3 oveq2 ⊢ x = y → A ⋅ 𝑜 x = A ⋅ 𝑜 y
4 3 eleq1d ⊢ x = y → A ⋅ 𝑜 x ∈ On ↔ A ⋅ 𝑜 y ∈ On
5 oveq2 ⊢ x = suc ⁡ y → A ⋅ 𝑜 x = A ⋅ 𝑜 suc ⁡ y
6 5 eleq1d ⊢ x = suc ⁡ y → A ⋅ 𝑜 x ∈ On ↔ A ⋅ 𝑜 suc ⁡ y ∈ On
7 oveq2 ⊢ x = B → A ⋅ 𝑜 x = A ⋅ 𝑜 B
8 7 eleq1d ⊢ x = B → A ⋅ 𝑜 x ∈ On ↔ A ⋅ 𝑜 B ∈ On
9 om0 ⊢ A ∈ On → A ⋅ 𝑜 ∅ = ∅
10 0elon ⊢ ∅ ∈ On
11 9 10 eqeltrdi ⊢ A ∈ On → A ⋅ 𝑜 ∅ ∈ On
12 oacl ⊢ A ⋅ 𝑜 y ∈ On ∧ A ∈ On → A ⋅ 𝑜 y + 𝑜 A ∈ On
13 12 expcom ⊢ A ∈ On → A ⋅ 𝑜 y ∈ On → A ⋅ 𝑜 y + 𝑜 A ∈ On
14 13 adantr ⊢ A ∈ On ∧ y ∈ On → A ⋅ 𝑜 y ∈ On → A ⋅ 𝑜 y + 𝑜 A ∈ On
15 omsuc ⊢ A ∈ On ∧ y ∈ On → A ⋅ 𝑜 suc ⁡ y = A ⋅ 𝑜 y + 𝑜 A
16 15 eleq1d ⊢ A ∈ On ∧ y ∈ On → A ⋅ 𝑜 suc ⁡ y ∈ On ↔ A ⋅ 𝑜 y + 𝑜 A ∈ On
17 14 16 sylibrd ⊢ A ∈ On ∧ y ∈ On → A ⋅ 𝑜 y ∈ On → A ⋅ 𝑜 suc ⁡ y ∈ On
18 17 expcom ⊢ y ∈ On → A ∈ On → A ⋅ 𝑜 y ∈ On → A ⋅ 𝑜 suc ⁡ y ∈ On
19 vex ⊢ x ∈ V
20 iunon ⊢ x ∈ V ∧ ∀ y ∈ x A ⋅ 𝑜 y ∈ On → ⋃ y ∈ x A ⋅ 𝑜 y ∈ On
21 19 20 mpan ⊢ ∀ y ∈ x A ⋅ 𝑜 y ∈ On → ⋃ y ∈ x A ⋅ 𝑜 y ∈ On
22 omlim ⊢ A ∈ On ∧ x ∈ V ∧ Lim ⁡ x → A ⋅ 𝑜 x = ⋃ y ∈ x A ⋅ 𝑜 y
23 19 22 mpanr1 ⊢ A ∈ On ∧ Lim ⁡ x → A ⋅ 𝑜 x = ⋃ y ∈ x A ⋅ 𝑜 y
24 23 eleq1d ⊢ A ∈ On ∧ Lim ⁡ x → A ⋅ 𝑜 x ∈ On ↔ ⋃ y ∈ x A ⋅ 𝑜 y ∈ On
25 21 24 imbitrrid ⊢ A ∈ On ∧ Lim ⁡ x → ∀ y ∈ x A ⋅ 𝑜 y ∈ On → A ⋅ 𝑜 x ∈ On
26 25 expcom ⊢ Lim ⁡ x → A ∈ On → ∀ y ∈ x A ⋅ 𝑜 y ∈ On → A ⋅ 𝑜 x ∈ On
27 2 4 6 8 11 18 26 tfinds3 ⊢ B ∈ On → A ∈ On → A ⋅ 𝑜 B ∈ On
28 27 impcom ⊢ A ∈ On ∧ B ∈ On → A ⋅ 𝑜 B ∈ On