Theorem r1limg

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

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

Proof

Step	Hyp	Ref	Expression
1		df-r1	⊢ 𝑅1 = rec ( ( 𝑦 ∈ V ↦ 𝒫 𝑦 ) , ∅ )
2	1	dmeqi	⊢ dom 𝑅1 = dom rec ( ( 𝑦 ∈ V ↦ 𝒫 𝑦 ) , ∅ )
3	2	eleq2i	⊢ ( 𝐴 ∈ dom 𝑅1 ↔ 𝐴 ∈ dom rec ( ( 𝑦 ∈ V ↦ 𝒫 𝑦 ) , ∅ ) )
4		rdglimg	⊢ ( ( 𝐴 ∈ dom rec ( ( 𝑦 ∈ V ↦ 𝒫 𝑦 ) , ∅ ) ∧ Lim 𝐴 ) → ( rec ( ( 𝑦 ∈ V ↦ 𝒫 𝑦 ) , ∅ ) ‘ 𝐴 ) = ∪ ( rec ( ( 𝑦 ∈ V ↦ 𝒫 𝑦 ) , ∅ ) “ 𝐴 ) )
5	3 4	sylanb	⊢ ( ( 𝐴 ∈ dom 𝑅1 ∧ Lim 𝐴 ) → ( rec ( ( 𝑦 ∈ V ↦ 𝒫 𝑦 ) , ∅ ) ‘ 𝐴 ) = ∪ ( rec ( ( 𝑦 ∈ V ↦ 𝒫 𝑦 ) , ∅ ) “ 𝐴 ) )
6	1	fveq1i	⊢ ( 𝑅1 ‘ 𝐴 ) = ( rec ( ( 𝑦 ∈ V ↦ 𝒫 𝑦 ) , ∅ ) ‘ 𝐴 )
7		r1funlim	⊢ ( Fun 𝑅1 ∧ Lim dom 𝑅1 )
8	7	simpli	⊢ Fun 𝑅1
9		funiunfv	⊢ ( Fun 𝑅1 → ∪ 𝑥 ∈ 𝐴 ( 𝑅1 ‘ 𝑥 ) = ∪ ( 𝑅1 “ 𝐴 ) )
10	8 9	ax-mp	⊢ ∪ 𝑥 ∈ 𝐴 ( 𝑅1 ‘ 𝑥 ) = ∪ ( 𝑅1 “ 𝐴 )
11	1	imaeq1i	⊢ ( 𝑅1 “ 𝐴 ) = ( rec ( ( 𝑦 ∈ V ↦ 𝒫 𝑦 ) , ∅ ) “ 𝐴 )
12	11	unieqi	⊢ ∪ ( 𝑅1 “ 𝐴 ) = ∪ ( rec ( ( 𝑦 ∈ V ↦ 𝒫 𝑦 ) , ∅ ) “ 𝐴 )
13	10 12	eqtri	⊢ ∪ 𝑥 ∈ 𝐴 ( 𝑅1 ‘ 𝑥 ) = ∪ ( rec ( ( 𝑦 ∈ V ↦ 𝒫 𝑦 ) , ∅ ) “ 𝐴 )
14	5 6 13	3eqtr4g	⊢ ( ( 𝐴 ∈ dom 𝑅1 ∧ Lim 𝐴 ) → ( 𝑅1 ‘ 𝐴 ) = ∪ 𝑥 ∈ 𝐴 ( 𝑅1 ‘ 𝑥 ) )