Metamath Proof Explorer


Theorem r1suc

Description: Value of the cumulative hierarchy of sets function at a successor ordinal. Part of Definition 9.9 of TakeutiZaring p. 76. (Contributed by NM, 2-Sep-2003) (Revised by Mario Carneiro, 10-Sep-2013)

Ref Expression
Assertion r1suc
|- ( A e. On -> ( R1 ` suc A ) = ~P ( R1 ` A ) )

Proof

Step Hyp Ref Expression
1 r1sucg
 |-  ( A e. dom R1 -> ( R1 ` suc A ) = ~P ( R1 ` A ) )
2 r1fnon
 |-  R1 Fn On
3 2 fndmi
 |-  dom R1 = On
4 3 eqcomi
 |-  On = dom R1
5 1 4 eleq2s
 |-  ( A e. On -> ( R1 ` suc A ) = ~P ( R1 ` A ) )