Theorem r1rankcld

Description: Any rank of the cumulative hierarchy is closed under the rank function. (Contributed by Rohan Ridenour, 11-Aug-2023)

	Ref	Expression
Hypothesis	r1rankcld.1	|- ( ph -> A e. ( R1 ` R ) )
Assertion	r1rankcld	|- ( ph -> ( rank ` A ) e. ( R1 ` R ) )

Proof

Step	Hyp	Ref	Expression
1		r1rankcld.1	|- ( ph -> A e. ( R1 ` R ) )
2		onssr1	|- ( R e. dom R1 -> R C_ ( R1 ` R ) )
3	2	adantl	|- ( ( ph /\ R e. dom R1 ) -> R C_ ( R1 ` R ) )
4		rankr1ai	|- ( A e. ( R1 ` R ) -> ( rank ` A ) e. R )
5	1 4	syl	|- ( ph -> ( rank ` A ) e. R )
6	5	adantr	|- ( ( ph /\ R e. dom R1 ) -> ( rank ` A ) e. R )
7	3 6	sseldd	|- ( ( ph /\ R e. dom R1 ) -> ( rank ` A ) e. ( R1 ` R ) )
8	1	adantr	|- ( ( ph /\ -. R e. dom R1 ) -> A e. ( R1 ` R ) )
9		noel	|- -. A e. (/)
10	9	a1i	|- ( -. R e. dom R1 -> -. A e. (/) )
11		ndmfv	|- ( -. R e. dom R1 -> ( R1 ` R ) = (/) )
12	10 11	neleqtrrd	|- ( -. R e. dom R1 -> -. A e. ( R1 ` R ) )
13	12	adantl	|- ( ( ph /\ -. R e. dom R1 ) -> -. A e. ( R1 ` R ) )
14	8 13	pm2.21dd	|- ( ( ph /\ -. R e. dom R1 ) -> ( rank ` A ) e. ( R1 ` R ) )
15	7 14	pm2.61dan	|- ( ph -> ( rank ` A ) e. ( R1 ` R ) )