Metamath Proof Explorer

Theorem omlim

Description: Ordinal multiplication with a limit ordinal. Definition 8.15 of TakeutiZaring p. 62. Definition 2.5 of Schloeder p. 4. (Contributed by NM, 3-Aug-2004) (Revised by Mario Carneiro, 8-Sep-2013)

Ref Expression
Assertion omlim ⊢ A ∈ On ∧ B ∈ C ∧ Lim ⁡ B → A ⋅ 𝑜 B = ⋃ x ∈ B A ⋅ 𝑜 x

Proof

Step Hyp Ref Expression
1 limelon ⊢ B ∈ C ∧ Lim ⁡ B → B ∈ On
2 simpr ⊢ B ∈ C ∧ Lim ⁡ B → Lim ⁡ B
3 1 2 jca ⊢ B ∈ C ∧ Lim ⁡ B → B ∈ On ∧ Lim ⁡ B
4 rdglim2a ⊢ B ∈ On ∧ Lim ⁡ B → rec ⁡ y ∈ V ⟼ y + 𝑜 A ∅ ⁡ B = ⋃ x ∈ B rec ⁡ y ∈ V ⟼ y + 𝑜 A ∅ ⁡ x
5 4 adantl ⊢ A ∈ On ∧ B ∈ On ∧ Lim ⁡ B → rec ⁡ y ∈ V ⟼ y + 𝑜 A ∅ ⁡ B = ⋃ x ∈ B rec ⁡ y ∈ V ⟼ y + 𝑜 A ∅ ⁡ x
6 omv ⊢ A ∈ On ∧ B ∈ On → A ⋅ 𝑜 B = rec ⁡ y ∈ V ⟼ y + 𝑜 A ∅ ⁡ B
7 onelon ⊢ B ∈ On ∧ x ∈ B → x ∈ On
8 omv ⊢ A ∈ On ∧ x ∈ On → A ⋅ 𝑜 x = rec ⁡ y ∈ V ⟼ y + 𝑜 A ∅ ⁡ x
9 7 8 sylan2 ⊢ A ∈ On ∧ B ∈ On ∧ x ∈ B → A ⋅ 𝑜 x = rec ⁡ y ∈ V ⟼ y + 𝑜 A ∅ ⁡ x
10 9 anassrs ⊢ A ∈ On ∧ B ∈ On ∧ x ∈ B → A ⋅ 𝑜 x = rec ⁡ y ∈ V ⟼ y + 𝑜 A ∅ ⁡ x
11 10 iuneq2dv ⊢ A ∈ On ∧ B ∈ On → ⋃ x ∈ B A ⋅ 𝑜 x = ⋃ x ∈ B rec ⁡ y ∈ V ⟼ y + 𝑜 A ∅ ⁡ x
12 6 11 eqeq12d ⊢ A ∈ On ∧ B ∈ On → A ⋅ 𝑜 B = ⋃ x ∈ B A ⋅ 𝑜 x ↔ rec ⁡ y ∈ V ⟼ y + 𝑜 A ∅ ⁡ B = ⋃ x ∈ B rec ⁡ y ∈ V ⟼ y + 𝑜 A ∅ ⁡ x
13 12 adantrr ⊢ A ∈ On ∧ B ∈ On ∧ Lim ⁡ B → A ⋅ 𝑜 B = ⋃ x ∈ B A ⋅ 𝑜 x ↔ rec ⁡ y ∈ V ⟼ y + 𝑜 A ∅ ⁡ B = ⋃ x ∈ B rec ⁡ y ∈ V ⟼ y + 𝑜 A ∅ ⁡ x
14 5 13 mpbird ⊢ A ∈ On ∧ B ∈ On ∧ Lim ⁡ B → A ⋅ 𝑜 B = ⋃ x ∈ B A ⋅ 𝑜 x
15 3 14 sylan2 ⊢ A ∈ On ∧ B ∈ C ∧ Lim ⁡ B → A ⋅ 𝑜 B = ⋃ x ∈ B A ⋅ 𝑜 x