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

Metamath Proof Explorer

Theorem r1val3

Description: The value of the cumulative hierarchy of sets function expressed in terms of rank. Theorem 15.18 of Monk1 p. 113. (Contributed by NM, 30-Nov-2003) (Revised by Mario Carneiro, 17-Nov-2014)

Ref Expression
Assertion r1val3 
|- ( A e. On -> ( R1 ` A ) = U_ x e. A ~P { y | ( rank ` y ) e. x } )

Proof

Step Hyp Ref Expression
1 r1fnon 
 |-  R1 Fn On
2 1 fndmi 
 |-  dom R1 = On
3 2 eleq2i 
 |-  ( A e. dom R1 <-> A e. On )
4 r1val1 
 |-  ( A e. dom R1 -> ( R1 ` A ) = U_ x e. A ~P ( R1 ` x ) )
5 3 4 sylbir 
 |-  ( A e. On -> ( R1 ` A ) = U_ x e. A ~P ( R1 ` x ) )
6 onelon 
 |-  ( ( A e. On /\ x e. A ) -> x e. On )
7 r1val2 
 |-  ( x e. On -> ( R1 ` x ) = { y | ( rank ` y ) e. x } )
8 6 7 syl 
 |-  ( ( A e. On /\ x e. A ) -> ( R1 ` x ) = { y | ( rank ` y ) e. x } )
9 8 pweqd 
 |-  ( ( A e. On /\ x e. A ) -> ~P ( R1 ` x ) = ~P { y | ( rank ` y ) e. x } )
10 9 iuneq2dv 
 |-  ( A e. On -> U_ x e. A ~P ( R1 ` x ) = U_ x e. A ~P { y | ( rank ` y ) e. x } )
11 5 10 eqtrd 
 |-  ( A e. On -> ( R1 ` A ) = U_ x e. A ~P { y | ( rank ` y ) e. x } )