Metamath Proof Explorer

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 A B Lim A R1 A = x A R1 x


Step Hyp Ref Expression
1 limelon A B Lim A A On
2 r1fnon R1 Fn On
3 fndm R1 Fn On dom R1 = On
4 2 3 ax-mp dom R1 = On
5 1 4 eleqtrrdi A B Lim A A dom R1
6 r1limg A dom R1 Lim A R1 A = x A R1 x
7 5 6 sylancom A B Lim A R1 A = x A R1 x