Metamath Proof Explorer


Theorem oalim

Description: Ordinal addition with a limit ordinal. Definition 8.1 of TakeutiZaring p. 56. (Contributed by NM, 3-Aug-2004) (Revised by Mario Carneiro, 8-Sep-2013)

Ref Expression
Assertion oalim ( ( 𝐴 ∈ 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 ↦ suc 𝑦 ) , 𝐴 ) ‘ 𝐵 ) = 𝑥𝐵 ( rec ( ( 𝑦 ∈ V ↦ suc 𝑦 ) , 𝐴 ) ‘ 𝑥 ) )
5 4 adantl ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ On ∧ Lim 𝐵 ) ) → ( rec ( ( 𝑦 ∈ V ↦ suc 𝑦 ) , 𝐴 ) ‘ 𝐵 ) = 𝑥𝐵 ( rec ( ( 𝑦 ∈ V ↦ suc 𝑦 ) , 𝐴 ) ‘ 𝑥 ) )
6 oav ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 +o 𝐵 ) = ( rec ( ( 𝑦 ∈ V ↦ suc 𝑦 ) , 𝐴 ) ‘ 𝐵 ) )
7 onelon ( ( 𝐵 ∈ On ∧ 𝑥𝐵 ) → 𝑥 ∈ On )
8 oav ( ( 𝐴 ∈ On ∧ 𝑥 ∈ On ) → ( 𝐴 +o 𝑥 ) = ( rec ( ( 𝑦 ∈ V ↦ suc 𝑦 ) , 𝐴 ) ‘ 𝑥 ) )
9 7 8 sylan2 ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ On ∧ 𝑥𝐵 ) ) → ( 𝐴 +o 𝑥 ) = ( rec ( ( 𝑦 ∈ V ↦ suc 𝑦 ) , 𝐴 ) ‘ 𝑥 ) )
10 9 anassrs ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝑥𝐵 ) → ( 𝐴 +o 𝑥 ) = ( rec ( ( 𝑦 ∈ V ↦ suc 𝑦 ) , 𝐴 ) ‘ 𝑥 ) )
11 10 iuneq2dv ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → 𝑥𝐵 ( 𝐴 +o 𝑥 ) = 𝑥𝐵 ( rec ( ( 𝑦 ∈ V ↦ suc 𝑦 ) , 𝐴 ) ‘ 𝑥 ) )
12 6 11 eqeq12d ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐴 +o 𝐵 ) = 𝑥𝐵 ( 𝐴 +o 𝑥 ) ↔ ( rec ( ( 𝑦 ∈ V ↦ suc 𝑦 ) , 𝐴 ) ‘ 𝐵 ) = 𝑥𝐵 ( rec ( ( 𝑦 ∈ V ↦ suc 𝑦 ) , 𝐴 ) ‘ 𝑥 ) ) )
13 12 adantrr ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ On ∧ Lim 𝐵 ) ) → ( ( 𝐴 +o 𝐵 ) = 𝑥𝐵 ( 𝐴 +o 𝑥 ) ↔ ( rec ( ( 𝑦 ∈ V ↦ suc 𝑦 ) , 𝐴 ) ‘ 𝐵 ) = 𝑥𝐵 ( rec ( ( 𝑦 ∈ V ↦ suc 𝑦 ) , 𝐴 ) ‘ 𝑥 ) ) )
14 5 13 mpbird ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ On ∧ Lim 𝐵 ) ) → ( 𝐴 +o 𝐵 ) = 𝑥𝐵 ( 𝐴 +o 𝑥 ) )
15 3 14 sylan2 ( ( 𝐴 ∈ On ∧ ( 𝐵𝐶 ∧ Lim 𝐵 ) ) → ( 𝐴 +o 𝐵 ) = 𝑥𝐵 ( 𝐴 +o 𝑥 ) )