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 } )