Theorem rankpwg

Description: The rank of the powerset is the successor of the rank. Closed form of rankpw . (Contributed by Scott Fenton, 16-Jul-2015)

	Ref	Expression
Assertion	rankpwg	⊢ ( 𝐴 ∈ 𝑉 → ( rank ‘ 𝒫 𝐴 ) = suc ( rank ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		pweq	⊢ ( 𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴 )
2	1	fveq2d	⊢ ( 𝑥 = 𝐴 → ( rank ‘ 𝒫 𝑥 ) = ( rank ‘ 𝒫 𝐴 ) )
3		fveq2	⊢ ( 𝑥 = 𝐴 → ( rank ‘ 𝑥 ) = ( rank ‘ 𝐴 ) )
4		suceq	⊢ ( ( rank ‘ 𝑥 ) = ( rank ‘ 𝐴 ) → suc ( rank ‘ 𝑥 ) = suc ( rank ‘ 𝐴 ) )
5	3 4	syl	⊢ ( 𝑥 = 𝐴 → suc ( rank ‘ 𝑥 ) = suc ( rank ‘ 𝐴 ) )
6	2 5	eqeq12d	⊢ ( 𝑥 = 𝐴 → ( ( rank ‘ 𝒫 𝑥 ) = suc ( rank ‘ 𝑥 ) ↔ ( rank ‘ 𝒫 𝐴 ) = suc ( rank ‘ 𝐴 ) ) )
7		vex	⊢ 𝑥 ∈ V
8	7	rankpw	⊢ ( rank ‘ 𝒫 𝑥 ) = suc ( rank ‘ 𝑥 )
9	6 8	vtoclg	⊢ ( 𝐴 ∈ 𝑉 → ( rank ‘ 𝒫 𝐴 ) = suc ( rank ‘ 𝐴 ) )