This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem oelim

Description: Ordinal exponentiation with a limit exponent and nonzero base. Definition 8.30 of TakeutiZaring p. 67. Definition 2.6 of Schloeder p. 4. (Contributed by NM, 1-Jan-2005) (Revised by Mario Carneiro, 8-Sep-2013)

Ref Expression
Assertion oelim ⊢ A ∈ On ∧ B ∈ C ∧ Lim ⁡ B ∧ ∅ ∈ A → 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 1 𝑜 ⁡ B = ⋃ x ∈ B rec ⁡ y ∈ V ⟼ y ⋅ 𝑜 A 1 𝑜 ⁡ x
5 4 ad2antlr ⊢ A ∈ On ∧ B ∈ On ∧ Lim ⁡ B ∧ ∅ ∈ A → rec ⁡ y ∈ V ⟼ y ⋅ 𝑜 A 1 𝑜 ⁡ B = ⋃ x ∈ B rec ⁡ y ∈ V ⟼ y ⋅ 𝑜 A 1 𝑜 ⁡ x
6 oevn0 ⊢ A ∈ On ∧ B ∈ On ∧ ∅ ∈ A → A ↑ 𝑜 B = rec ⁡ y ∈ V ⟼ y ⋅ 𝑜 A 1 𝑜 ⁡ B
7 onelon ⊢ B ∈ On ∧ x ∈ B → x ∈ On
8 oevn0 ⊢ A ∈ On ∧ x ∈ On ∧ ∅ ∈ A → A ↑ 𝑜 x = rec ⁡ y ∈ V ⟼ y ⋅ 𝑜 A 1 𝑜 ⁡ x
9 7 8 sylanl2 ⊢ A ∈ On ∧ B ∈ On ∧ x ∈ B ∧ ∅ ∈ A → A ↑ 𝑜 x = rec ⁡ y ∈ V ⟼ y ⋅ 𝑜 A 1 𝑜 ⁡ x
10 9 exp42 ⊢ A ∈ On → B ∈ On → x ∈ B → ∅ ∈ A → A ↑ 𝑜 x = rec ⁡ y ∈ V ⟼ y ⋅ 𝑜 A 1 𝑜 ⁡ x
11 10 com34 ⊢ A ∈ On → B ∈ On → ∅ ∈ A → x ∈ B → A ↑ 𝑜 x = rec ⁡ y ∈ V ⟼ y ⋅ 𝑜 A 1 𝑜 ⁡ x
12 11 imp41 ⊢ A ∈ On ∧ B ∈ On ∧ ∅ ∈ A ∧ x ∈ B → A ↑ 𝑜 x = rec ⁡ y ∈ V ⟼ y ⋅ 𝑜 A 1 𝑜 ⁡ x
13 12 iuneq2dv ⊢ A ∈ On ∧ B ∈ On ∧ ∅ ∈ A → ⋃ x ∈ B A ↑ 𝑜 x = ⋃ x ∈ B rec ⁡ y ∈ V ⟼ y ⋅ 𝑜 A 1 𝑜 ⁡ x
14 6 13 eqeq12d ⊢ A ∈ On ∧ B ∈ On ∧ ∅ ∈ A → A ↑ 𝑜 B = ⋃ x ∈ B A ↑ 𝑜 x ↔ rec ⁡ y ∈ V ⟼ y ⋅ 𝑜 A 1 𝑜 ⁡ B = ⋃ x ∈ B rec ⁡ y ∈ V ⟼ y ⋅ 𝑜 A 1 𝑜 ⁡ x
15 14 adantlrr ⊢ A ∈ On ∧ B ∈ On ∧ Lim ⁡ B ∧ ∅ ∈ A → A ↑ 𝑜 B = ⋃ x ∈ B A ↑ 𝑜 x ↔ rec ⁡ y ∈ V ⟼ y ⋅ 𝑜 A 1 𝑜 ⁡ B = ⋃ x ∈ B rec ⁡ y ∈ V ⟼ y ⋅ 𝑜 A 1 𝑜 ⁡ x
16 5 15 mpbird ⊢ A ∈ On ∧ B ∈ On ∧ Lim ⁡ B ∧ ∅ ∈ A → A ↑ 𝑜 B = ⋃ x ∈ B A ↑ 𝑜 x
17 3 16 sylanl2 ⊢ A ∈ On ∧ B ∈ C ∧ Lim ⁡ B ∧ ∅ ∈ A → A ↑ 𝑜 B = ⋃ x ∈ B A ↑ 𝑜 x