Theorem rankpwg

Description: The rank of a power set. Closed form of rankpw . (Contributed by Scott Fenton, 16-Jul-2015)

	Ref	Expression
Assertion	rankpwg	|- ( A e. V -> ( rank ` ~P A ) = suc ( rank ` A ) )

Proof

Step	Hyp	Ref	Expression
1		pweq	|- ( x = A -> ~P x = ~P A )
2	1	fveq2d	|- ( x = A -> ( rank ` ~P x ) = ( rank ` ~P A ) )
3		fveq2	|- ( x = A -> ( rank ` x ) = ( rank ` A ) )
4		suceq	|- ( ( rank ` x ) = ( rank ` A ) -> suc ( rank ` x ) = suc ( rank ` A ) )
5	3 4	syl	|- ( x = A -> suc ( rank ` x ) = suc ( rank ` A ) )
6	2 5	eqeq12d	|- ( x = A -> ( ( rank ` ~P x ) = suc ( rank ` x ) <-> ( rank ` ~P A ) = suc ( rank ` A ) ) )
7		vex	|- x e. _V
8	7	rankpw	|- ( rank ` ~P x ) = suc ( rank ` x )
9	6 8	vtoclg	|- ( A e. V -> ( rank ` ~P A ) = suc ( rank ` A ) )