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 ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ∅ ∈ 𝐴 ) → ( 𝐴 ↑o 𝐵 ) = ∪ 𝑥 ∈ 𝐵 ( 𝐴 ↑o 𝑥 ) )

Proof

Step Hyp Ref Expression
1 limelon ⊢ ( ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) → 𝐵 ∈ On )
2 simpr ⊢ ( ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) → Lim 𝐵 )
3 1 2 jca ⊢ ( ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) → ( 𝐵 ∈ On ∧ Lim 𝐵 ) )
4 rdglim2a ⊢ ( ( 𝐵 ∈ On ∧ Lim 𝐵 ) → ( rec ( ( 𝑦 ∈ V ↦ ( 𝑦 ·o 𝐴 ) ) , 1o ) ‘ 𝐵 ) = ∪ 𝑥 ∈ 𝐵 ( rec ( ( 𝑦 ∈ V ↦ ( 𝑦 ·o 𝐴 ) ) , 1o ) ‘ 𝑥 ) )
5 4 ad2antlr ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ On ∧ Lim 𝐵 ) ) ∧ ∅ ∈ 𝐴 ) → ( rec ( ( 𝑦 ∈ V ↦ ( 𝑦 ·o 𝐴 ) ) , 1o ) ‘ 𝐵 ) = ∪ 𝑥 ∈ 𝐵 ( rec ( ( 𝑦 ∈ V ↦ ( 𝑦 ·o 𝐴 ) ) , 1o ) ‘ 𝑥 ) )
6 oevn0 ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ( 𝐴 ↑o 𝐵 ) = ( rec ( ( 𝑦 ∈ V ↦ ( 𝑦 ·o 𝐴 ) ) , 1o ) ‘ 𝐵 ) )
7 onelon ⊢ ( ( 𝐵 ∈ On ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ On )
8 oevn0 ⊢ ( ( ( 𝐴 ∈ On ∧ 𝑥 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ( 𝐴 ↑o 𝑥 ) = ( rec ( ( 𝑦 ∈ V ↦ ( 𝑦 ·o 𝐴 ) ) , 1o ) ‘ 𝑥 ) )
9 7 8 sylanl2 ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ On ∧ 𝑥 ∈ 𝐵 ) ) ∧ ∅ ∈ 𝐴 ) → ( 𝐴 ↑o 𝑥 ) = ( rec ( ( 𝑦 ∈ V ↦ ( 𝑦 ·o 𝐴 ) ) , 1o ) ‘ 𝑥 ) )
10 9 exp42 ⊢ ( 𝐴 ∈ On → ( 𝐵 ∈ On → ( 𝑥 ∈ 𝐵 → ( ∅ ∈ 𝐴 → ( 𝐴 ↑o 𝑥 ) = ( rec ( ( 𝑦 ∈ V ↦ ( 𝑦 ·o 𝐴 ) ) , 1o ) ‘ 𝑥 ) ) ) ) )
11 10 com34 ⊢ ( 𝐴 ∈ On → ( 𝐵 ∈ On → ( ∅ ∈ 𝐴 → ( 𝑥 ∈ 𝐵 → ( 𝐴 ↑o 𝑥 ) = ( rec ( ( 𝑦 ∈ V ↦ ( 𝑦 ·o 𝐴 ) ) , 1o ) ‘ 𝑥 ) ) ) ) )
12 11 imp41 ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ∅ ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝐴 ↑o 𝑥 ) = ( rec ( ( 𝑦 ∈ V ↦ ( 𝑦 ·o 𝐴 ) ) , 1o ) ‘ 𝑥 ) )
13 12 iuneq2dv ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ∪ 𝑥 ∈ 𝐵 ( 𝐴 ↑o 𝑥 ) = ∪ 𝑥 ∈ 𝐵 ( rec ( ( 𝑦 ∈ V ↦ ( 𝑦 ·o 𝐴 ) ) , 1o ) ‘ 𝑥 ) )
14 6 13 eqeq12d ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ( ( 𝐴 ↑o 𝐵 ) = ∪ 𝑥 ∈ 𝐵 ( 𝐴 ↑o 𝑥 ) ↔ ( rec ( ( 𝑦 ∈ V ↦ ( 𝑦 ·o 𝐴 ) ) , 1o ) ‘ 𝐵 ) = ∪ 𝑥 ∈ 𝐵 ( rec ( ( 𝑦 ∈ V ↦ ( 𝑦 ·o 𝐴 ) ) , 1o ) ‘ 𝑥 ) ) )
15 14 adantlrr ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ On ∧ Lim 𝐵 ) ) ∧ ∅ ∈ 𝐴 ) → ( ( 𝐴 ↑o 𝐵 ) = ∪ 𝑥 ∈ 𝐵 ( 𝐴 ↑o 𝑥 ) ↔ ( rec ( ( 𝑦 ∈ V ↦ ( 𝑦 ·o 𝐴 ) ) , 1o ) ‘ 𝐵 ) = ∪ 𝑥 ∈ 𝐵 ( rec ( ( 𝑦 ∈ V ↦ ( 𝑦 ·o 𝐴 ) ) , 1o ) ‘ 𝑥 ) ) )
16 5 15 mpbird ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ On ∧ Lim 𝐵 ) ) ∧ ∅ ∈ 𝐴 ) → ( 𝐴 ↑o 𝐵 ) = ∪ 𝑥 ∈ 𝐵 ( 𝐴 ↑o 𝑥 ) )
17 3 16 sylanl2 ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ∅ ∈ 𝐴 ) → ( 𝐴 ↑o 𝐵 ) = ∪ 𝑥 ∈ 𝐵 ( 𝐴 ↑o 𝑥 ) )