Theorem r1lim

Description: Value of the cumulative hierarchy of sets function at a limit ordinal. Part of Definition 9.9 of TakeutiZaring p. 76. (Contributed by NM, 4-Oct-2003) (Revised by Mario Carneiro, 16-Nov-2014)

	Ref	Expression
Assertion	r1lim	⊢ ( ( 𝐴 ∈ 𝐵 ∧ Lim 𝐴 ) → ( 𝑅1 ‘ 𝐴 ) = ∪ 𝑥 ∈ 𝐴 ( 𝑅1 ‘ 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		limelon	⊢ ( ( 𝐴 ∈ 𝐵 ∧ Lim 𝐴 ) → 𝐴 ∈ On )
2		r1fnon	⊢ 𝑅1 Fn On
3		fndm	⊢ ( 𝑅1 Fn On → dom 𝑅1 = On )
4	2 3	ax-mp	⊢ dom 𝑅1 = On
5	1 4	eleqtrrdi	⊢ ( ( 𝐴 ∈ 𝐵 ∧ Lim 𝐴 ) → 𝐴 ∈ dom 𝑅1 )
6		r1limg	⊢ ( ( 𝐴 ∈ dom 𝑅1 ∧ Lim 𝐴 ) → ( 𝑅1 ‘ 𝐴 ) = ∪ 𝑥 ∈ 𝐴 ( 𝑅1 ‘ 𝑥 ) )
7	5 6	sylancom	⊢ ( ( 𝐴 ∈ 𝐵 ∧ Lim 𝐴 ) → ( 𝑅1 ‘ 𝐴 ) = ∪ 𝑥 ∈ 𝐴 ( 𝑅1 ‘ 𝑥 ) )