Description: The value of the recursive definition generator at a limit ordinal. (Contributed by NM, 23-Apr-1995) (Revised by Mario Carneiro, 14-Nov-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | rdglim | ⊢ ( ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) → ( rec ( 𝐹 , 𝐴 ) ‘ 𝐵 ) = ∪ ( rec ( 𝐹 , 𝐴 ) “ 𝐵 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | limelon | ⊢ ( ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) → 𝐵 ∈ On ) | |
2 | rdgfnon | ⊢ rec ( 𝐹 , 𝐴 ) Fn On | |
3 | fndm | ⊢ ( rec ( 𝐹 , 𝐴 ) Fn On → dom rec ( 𝐹 , 𝐴 ) = On ) | |
4 | 2 3 | ax-mp | ⊢ dom rec ( 𝐹 , 𝐴 ) = On |
5 | 1 4 | eleqtrrdi | ⊢ ( ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) → 𝐵 ∈ dom rec ( 𝐹 , 𝐴 ) ) |
6 | rdglimg | ⊢ ( ( 𝐵 ∈ dom rec ( 𝐹 , 𝐴 ) ∧ Lim 𝐵 ) → ( rec ( 𝐹 , 𝐴 ) ‘ 𝐵 ) = ∪ ( rec ( 𝐹 , 𝐴 ) “ 𝐵 ) ) | |
7 | 5 6 | sylancom | ⊢ ( ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) → ( rec ( 𝐹 , 𝐴 ) ‘ 𝐵 ) = ∪ ( rec ( 𝐹 , 𝐴 ) “ 𝐵 ) ) |