Theorem r1filim

Description: A finite set appears in the cumulative hierarchy prior to a limit ordinal iff all of its elements appear in the cumulative hierarchy prior to that limit ordinal. (Contributed by BTernaryTau, 22-Jan-2026)

	Ref	Expression
Assertion	r1filim	|- ( ( A e. Fin /\ Lim B ) -> ( A e. U. ( R1 " B ) <-> A. x e. A x e. U. ( R1 " B ) ) )

Proof

Step	Hyp	Ref	Expression
1		r1tr	|- Tr ( R1 ` y )
2		trel	|- ( Tr ( R1 ` y ) -> ( ( x e. A /\ A e. ( R1 ` y ) ) -> x e. ( R1 ` y ) ) )
3	1 2	ax-mp	|- ( ( x e. A /\ A e. ( R1 ` y ) ) -> x e. ( R1 ` y ) )
4	3	ex	|- ( x e. A -> ( A e. ( R1 ` y ) -> x e. ( R1 ` y ) ) )
5	4	reximdv	|- ( x e. A -> ( E. y e. B A e. ( R1 ` y ) -> E. y e. B x e. ( R1 ` y ) ) )
6		r1fun	|- Fun R1
7		eluniima	|- ( Fun R1 -> ( A e. U. ( R1 " B ) <-> E. y e. B A e. ( R1 ` y ) ) )
8	6 7	ax-mp	|- ( A e. U. ( R1 " B ) <-> E. y e. B A e. ( R1 ` y ) )
9		eluniima	|- ( Fun R1 -> ( x e. U. ( R1 " B ) <-> E. y e. B x e. ( R1 ` y ) ) )
10	6 9	ax-mp	|- ( x e. U. ( R1 " B ) <-> E. y e. B x e. ( R1 ` y ) )
11	5 8 10	3imtr4g	|- ( x e. A -> ( A e. U. ( R1 " B ) -> x e. U. ( R1 " B ) ) )
12	11	com12	|- ( A e. U. ( R1 " B ) -> ( x e. A -> x e. U. ( R1 " B ) ) )
13	12	ralrimiv	|- ( A e. U. ( R1 " B ) -> A. x e. A x e. U. ( R1 " B ) )
14		r1filimi	|- ( ( A e. Fin /\ A. x e. A x e. U. ( R1 " B ) /\ Lim B ) -> A e. U. ( R1 " B ) )
15	14	3com23	|- ( ( A e. Fin /\ Lim B /\ A. x e. A x e. U. ( R1 " B ) ) -> A e. U. ( R1 " B ) )
16	15	3expia	|- ( ( A e. Fin /\ Lim B ) -> ( A. x e. A x e. U. ( R1 " B ) -> A e. U. ( R1 " B ) ) )
17	13 16	impbid2	|- ( ( A e. Fin /\ Lim B ) -> ( A e. U. ( R1 " B ) <-> A. x e. A x e. U. ( R1 " B ) ) )