Theorem ranksng

Description: The rank of a singleton. Closed form of ranksn . (Contributed by Scott Fenton, 15-Jul-2015)

	Ref	Expression
Assertion	ranksng	⊢ ( 𝐴 ∈ 𝑉 → ( rank ‘ { 𝐴 } ) = suc ( rank ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		sneq	⊢ ( 𝑥 = 𝐴 → { 𝑥 } = { 𝐴 } )
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	ranksn	⊢ ( rank ‘ { 𝑥 } ) = suc ( rank ‘ 𝑥 )
9	6 8	vtoclg	⊢ ( 𝐴 ∈ 𝑉 → ( rank ‘ { 𝐴 } ) = suc ( rank ‘ 𝐴 ) )