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

Metamath Proof Explorer

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 ‘ 𝑥 ) )