Theorem r1elcl

Description: Each set of the cumulative hierarchy is closed under membership. (Contributed by BTernaryTau, 30-Dec-2025)

	Ref	Expression
Assertion	r1elcl	|- ( ( A e. ( R1 ` B ) /\ C e. A ) -> C e. ( R1 ` B ) )

Proof

Step	Hyp	Ref	Expression
1		r1elwf	|- ( A e. ( R1 ` B ) -> A e. U. ( R1 " On ) )
2		rankelb	|- ( A e. U. ( R1 " On ) -> ( C e. A -> ( rank ` C ) e. ( rank ` A ) ) )
3	1 2	syl	|- ( A e. ( R1 ` B ) -> ( C e. A -> ( rank ` C ) e. ( rank ` A ) ) )
4	3	imp	|- ( ( A e. ( R1 ` B ) /\ C e. A ) -> ( rank ` C ) e. ( rank ` A ) )
5		rankr1ai	|- ( A e. ( R1 ` B ) -> ( rank ` A ) e. B )
6		elfvdm	|- ( A e. ( R1 ` B ) -> B e. dom R1 )
7		r1fnon	|- R1 Fn On
8	7	fndmi	|- dom R1 = On
9	6 8	eleqtrdi	|- ( A e. ( R1 ` B ) -> B e. On )
10		ontr1	|- ( B e. On -> ( ( ( rank ` C ) e. ( rank ` A ) /\ ( rank ` A ) e. B ) -> ( rank ` C ) e. B ) )
11	9 10	syl	|- ( A e. ( R1 ` B ) -> ( ( ( rank ` C ) e. ( rank ` A ) /\ ( rank ` A ) e. B ) -> ( rank ` C ) e. B ) )
12	5 11	mpan2d	|- ( A e. ( R1 ` B ) -> ( ( rank ` C ) e. ( rank ` A ) -> ( rank ` C ) e. B ) )
13	12	adantr	|- ( ( A e. ( R1 ` B ) /\ C e. A ) -> ( ( rank ` C ) e. ( rank ` A ) -> ( rank ` C ) e. B ) )
14	4 13	mpd	|- ( ( A e. ( R1 ` B ) /\ C e. A ) -> ( rank ` C ) e. B )
15		elwf	|- ( ( A e. U. ( R1 " On ) /\ C e. A ) -> C e. U. ( R1 " On ) )
16	1 15	sylan	|- ( ( A e. ( R1 ` B ) /\ C e. A ) -> C e. U. ( R1 " On ) )
17		rankr1ag	|- ( ( C e. U. ( R1 " On ) /\ B e. dom R1 ) -> ( C e. ( R1 ` B ) <-> ( rank ` C ) e. B ) )
18	6 17	sylan2	|- ( ( C e. U. ( R1 " On ) /\ A e. ( R1 ` B ) ) -> ( C e. ( R1 ` B ) <-> ( rank ` C ) e. B ) )
19	18	ancoms	|- ( ( A e. ( R1 ` B ) /\ C e. U. ( R1 " On ) ) -> ( C e. ( R1 ` B ) <-> ( rank ` C ) e. B ) )
20	16 19	syldan	|- ( ( A e. ( R1 ` B ) /\ C e. A ) -> ( C e. ( R1 ` B ) <-> ( rank ` C ) e. B ) )
21	14 20	mpbird	|- ( ( A e. ( R1 ` B ) /\ C e. A ) -> C e. ( R1 ` B ) )