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

Metamath Proof Explorer

Theorem oalim

Description: Ordinal addition with a limit ordinal. Definition 8.1 of TakeutiZaring p. 56. Definition 2.3 of Schloeder p. 4. (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 𝑥 ) )