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		r1elcl	|- ( ( A e. ( R1 ` y ) /\ x e. A ) -> x e. ( R1 ` y ) )
2	1	expcom	|- ( x e. A -> ( A e. ( R1 ` y ) -> x e. ( R1 ` y ) ) )
3	2	reximdv	|- ( x e. A -> ( E. y e. B A e. ( R1 ` y ) -> E. y e. B x e. ( R1 ` y ) ) )
4		r1funlim	|- ( Fun R1 /\ Lim dom R1 )
5	4	simpli	|- Fun R1
6		eluniima	|- ( Fun R1 -> ( A e. U. ( R1 " B ) <-> E. y e. B A e. ( R1 ` y ) ) )
7	5 6	ax-mp	|- ( A e. U. ( R1 " B ) <-> E. y e. B A e. ( R1 ` y ) )
8		eluniima	|- ( Fun R1 -> ( x e. U. ( R1 " B ) <-> E. y e. B x e. ( R1 ` y ) ) )
9	5 8	ax-mp	|- ( x e. U. ( R1 " B ) <-> E. y e. B x e. ( R1 ` y ) )
10	3 7 9	3imtr4g	|- ( x e. A -> ( A e. U. ( R1 " B ) -> x e. U. ( R1 " B ) ) )
11	10	com12	|- ( A e. U. ( R1 " B ) -> ( x e. A -> x e. U. ( R1 " B ) ) )
12	11	ralrimiv	|- ( A e. U. ( R1 " B ) -> A. x e. A x e. U. ( R1 " B ) )
13		r1filimi	|- ( ( A e. Fin /\ A. x e. A x e. U. ( R1 " B ) /\ Lim B ) -> A e. U. ( R1 " B ) )
14	13	3com23	|- ( ( A e. Fin /\ Lim B /\ A. x e. A x e. U. ( R1 " B ) ) -> A e. U. ( R1 " B ) )
15	14	3expia	|- ( ( A e. Fin /\ Lim B ) -> ( A. x e. A x e. U. ( R1 " B ) -> A e. U. ( R1 " B ) ) )
16	12 15	impbid2	|- ( ( A e. Fin /\ Lim B ) -> ( A e. U. ( R1 " B ) <-> A. x e. A x e. U. ( R1 " B ) ) )