Metamath Proof Explorer

Theorem oacl

Description: Closure law for ordinal addition. Proposition 8.2 of TakeutiZaring p. 57. Remark 2.8 of Schloeder p. 5. (Contributed by NM, 5-May-1995)

Ref Expression
Assertion oacl ⊢ 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 oa0 ⊢ A ∈ On → A + 𝑜 ∅ = A
10 9 eleq1d ⊢ A ∈ On → A + 𝑜 ∅ ∈ On ↔ A ∈ On
11 10 ibir ⊢ A ∈ On → A + 𝑜 ∅ ∈ On
12 onsuc ⊢ A + 𝑜 y ∈ On → suc ⁡ A + 𝑜 y ∈ On
13 oasuc ⊢ A ∈ On ∧ y ∈ On → A + 𝑜 suc ⁡ y = suc ⁡ A + 𝑜 y
14 13 eleq1d ⊢ A ∈ On ∧ y ∈ On → A + 𝑜 suc ⁡ y ∈ On ↔ suc ⁡ A + 𝑜 y ∈ On
15 12 14 imbitrrid ⊢ A ∈ On ∧ y ∈ On → A + 𝑜 y ∈ On → A + 𝑜 suc ⁡ y ∈ On
16 15 expcom ⊢ y ∈ On → A ∈ On → A + 𝑜 y ∈ On → A + 𝑜 suc ⁡ y ∈ On
17 vex ⊢ x ∈ V
18 iunon ⊢ x ∈ V ∧ ∀ y ∈ x A + 𝑜 y ∈ On → ⋃ y ∈ x A + 𝑜 y ∈ On
19 17 18 mpan ⊢ ∀ y ∈ x A + 𝑜 y ∈ On → ⋃ y ∈ x A + 𝑜 y ∈ On
20 oalim ⊢ A ∈ On ∧ x ∈ V ∧ Lim ⁡ x → A + 𝑜 x = ⋃ y ∈ x A + 𝑜 y
21 17 20 mpanr1 ⊢ A ∈ On ∧ Lim ⁡ x → A + 𝑜 x = ⋃ y ∈ x A + 𝑜 y
22 21 eleq1d ⊢ A ∈ On ∧ Lim ⁡ x → A + 𝑜 x ∈ On ↔ ⋃ y ∈ x A + 𝑜 y ∈ On
23 19 22 imbitrrid ⊢ A ∈ On ∧ Lim ⁡ x → ∀ y ∈ x A + 𝑜 y ∈ On → A + 𝑜 x ∈ On
24 23 expcom ⊢ Lim ⁡ x → A ∈ On → ∀ y ∈ x A + 𝑜 y ∈ On → A + 𝑜 x ∈ On
25 2 4 6 8 11 16 24 tfinds3 ⊢ B ∈ On → A ∈ On → A + 𝑜 B ∈ On
26 25 impcom ⊢ A ∈ On ∧ B ∈ On → A + 𝑜 B ∈ On