Metamath Proof Explorer

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 \in Fin \land Lim B) \to (A \in ⋃ R_{1} [B] \leftrightarrow \forall x \in A x \in ⋃ R_{1} [B])$

Proof

Step	Hyp	Ref	Expression
1		r1elcl	$⊢ (A \in R_{1} (y) \land x \in A) \to x \in R_{1} (y)$
2	1	expcom	$⊢ x \in A \to (A \in R_{1} (y) \to x \in R_{1} (y))$
3	2	reximdv	$⊢ x \in A \to (\exists y \in B A \in R_{1} (y) \to \exists y \in B x \in R_{1} (y))$
4		r1funlim	$⊢ (Fun R_{1} \land Lim dom R_{1})$
5	4	simpli	$⊢ Fun R_{1}$
6		eluniima	$⊢ Fun R_{1} \to (A \in ⋃ R_{1} [B] \leftrightarrow \exists y \in B A \in R_{1} (y))$
7	5 6	ax-mp	$⊢ A \in ⋃ R_{1} [B] \leftrightarrow \exists y \in B A \in R_{1} (y)$
8		eluniima	$⊢ Fun R_{1} \to (x \in ⋃ R_{1} [B] \leftrightarrow \exists y \in B x \in R_{1} (y))$
9	5 8	ax-mp	$⊢ x \in ⋃ R_{1} [B] \leftrightarrow \exists y \in B x \in R_{1} (y)$
10	3 7 9	3imtr4g	$⊢ x \in A \to (A \in ⋃ R_{1} [B] \to x \in ⋃ R_{1} [B])$
11	10	com12	$⊢ A \in ⋃ R_{1} [B] \to (x \in A \to x \in ⋃ R_{1} [B])$
12	11	ralrimiv	$⊢ A \in ⋃ R_{1} [B] \to \forall x \in A x \in ⋃ R_{1} [B]$
13		r1filimi	$⊢ (A \in Fin \land \forall x \in A x \in ⋃ R_{1} [B] \land Lim B) \to A \in ⋃ R_{1} [B]$
14	13	3com23	$⊢ (A \in Fin \land Lim B \land \forall x \in A x \in ⋃ R_{1} [B]) \to A \in ⋃ R_{1} [B]$
15	14	3expia	$⊢ (A \in Fin \land Lim B) \to (\forall x \in A x \in ⋃ R_{1} [B] \to A \in ⋃ R_{1} [B])$
16	12 15	impbid2	$⊢ (A \in Fin \land Lim B) \to (A \in ⋃ R_{1} [B] \leftrightarrow \forall x \in A x \in ⋃ R_{1} [B])$