Metamath Proof Explorer

Theorem r1sucg

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

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

Proof

Step Hyp Ref Expression
1 rdgsucg 
 |-  ( A e. dom rec ( ( x e. _V |-> ~P x ) , (/) ) -> ( rec ( ( x e. _V |-> ~P x ) , (/) ) ` suc A ) = ( ( x e. _V |-> ~P x ) ` ( rec ( ( x e. _V |-> ~P x ) , (/) ) ` A ) ) )
2 df-r1 
 |-  R1 = rec ( ( x e. _V |-> ~P x ) , (/) )
3 2 dmeqi 
 |-  dom R1 = dom rec ( ( x e. _V |-> ~P x ) , (/) )
4 1 3 eleq2s 
 |-  ( A e. dom R1 -> ( rec ( ( x e. _V |-> ~P x ) , (/) ) ` suc A ) = ( ( x e. _V |-> ~P x ) ` ( rec ( ( x e. _V |-> ~P x ) , (/) ) ` A ) ) )
5 2 fveq1i 
 |-  ( R1 ` suc A ) = ( rec ( ( x e. _V |-> ~P x ) , (/) ) ` suc A )
6 fvex 
 |-  ( R1 ` A ) e. _V
7 pweq 
 |-  ( x = ( R1 ` A ) -> ~P x = ~P ( R1 ` A ) )
8 eqid 
 |-  ( x e. _V |-> ~P x ) = ( x e. _V |-> ~P x )
9 6 pwex 
 |-  ~P ( R1 ` A ) e. _V
10 7 8 9 fvmpt 
 |-  ( ( R1 ` A ) e. _V -> ( ( x e. _V |-> ~P x ) ` ( R1 ` A ) ) = ~P ( R1 ` A ) )
11 6 10 ax-mp 
 |-  ( ( x e. _V |-> ~P x ) ` ( R1 ` A ) ) = ~P ( R1 ` A )
12 2 fveq1i 
 |-  ( R1 ` A ) = ( rec ( ( x e. _V |-> ~P x ) , (/) ) ` A )
13 12 fveq2i 
 |-  ( ( x e. _V |-> ~P x ) ` ( R1 ` A ) ) = ( ( x e. _V |-> ~P x ) ` ( rec ( ( x e. _V |-> ~P x ) , (/) ) ` A ) )
14 11 13 eqtr3i 
 |-  ~P ( R1 ` A ) = ( ( x e. _V |-> ~P x ) ` ( rec ( ( x e. _V |-> ~P x ) , (/) ) ` A ) )
15 4 5 14 3eqtr4g 
 |-  ( A e. dom R1 -> ( R1 ` suc A ) = ~P ( R1 ` A ) )