Theorem rankelg

Description: The membership relation is inherited by the rank function. Closed form of rankel . (Contributed by Scott Fenton, 16-Jul-2015)

	Ref	Expression
Assertion	rankelg	|- ( ( B e. V /\ A e. B ) -> ( rank ` A ) e. ( rank ` B ) )

Proof

Step	Hyp	Ref	Expression
1		eleq2	|- ( y = B -> ( A e. y <-> A e. B ) )
2		fveq2	|- ( y = B -> ( rank ` y ) = ( rank ` B ) )
3	2	eleq2d	|- ( y = B -> ( ( rank ` A ) e. ( rank ` y ) <-> ( rank ` A ) e. ( rank ` B ) ) )
4	1 3	imbi12d	|- ( y = B -> ( ( A e. y -> ( rank ` A ) e. ( rank ` y ) ) <-> ( A e. B -> ( rank ` A ) e. ( rank ` B ) ) ) )
5		vex	|- y e. _V
6	5	rankel	|- ( A e. y -> ( rank ` A ) e. ( rank ` y ) )
7	4 6	vtoclg	|- ( B e. V -> ( A e. B -> ( rank ` A ) e. ( rank ` B ) ) )
8	7	imp	|- ( ( B e. V /\ A e. B ) -> ( rank ` A ) e. ( rank ` B ) )