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 AdomR1LimAR1A=xAR1x

Proof

Step Hyp Ref Expression
1 df-r1 R1=recyV𝒫y
2 1 dmeqi domR1=domrecyV𝒫y
3 2 eleq2i AdomR1AdomrecyV𝒫y
4 rdglimg AdomrecyV𝒫yLimArecyV𝒫yA=recyV𝒫yA
5 3 4 sylanb AdomR1LimArecyV𝒫yA=recyV𝒫yA
6 1 fveq1i R1A=recyV𝒫yA
7 r1funlim FunR1LimdomR1
8 7 simpli FunR1
9 funiunfv FunR1xAR1x=R1A
10 8 9 ax-mp xAR1x=R1A
11 1 imaeq1i R1A=recyV𝒫yA
12 11 unieqi R1A=recyV𝒫yA
13 10 12 eqtri xAR1x=recyV𝒫yA
14 5 6 13 3eqtr4g AdomR1LimAR1A=xAR1x