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		r1tr	$⊢ Tr R_{1} (y)$
2		trel	$⊢ Tr R_{1} (y) \to ((x \in A \land A \in R_{1} (y)) \to x \in R_{1} (y))$
3	1 2	ax-mp	$⊢ (x \in A \land A \in R_{1} (y)) \to x \in R_{1} (y)$
4	3	ex	$⊢ x \in A \to (A \in R_{1} (y) \to x \in R_{1} (y))$
5	4	reximdv	$⊢ x \in A \to (\exists y \in B A \in R_{1} (y) \to \exists y \in B x \in R_{1} (y))$
6		r1fun	$⊢ Fun R_{1}$
7		eluniima	$⊢ Fun R_{1} \to (A \in ⋃ R_{1} [B] \leftrightarrow \exists y \in B A \in R_{1} (y))$
8	6 7	ax-mp	$⊢ A \in ⋃ R_{1} [B] \leftrightarrow \exists y \in B A \in R_{1} (y)$
9		eluniima	$⊢ Fun R_{1} \to (x \in ⋃ R_{1} [B] \leftrightarrow \exists y \in B x \in R_{1} (y))$
10	6 9	ax-mp	$⊢ x \in ⋃ R_{1} [B] \leftrightarrow \exists y \in B x \in R_{1} (y)$
11	5 8 10	3imtr4g	$⊢ x \in A \to (A \in ⋃ R_{1} [B] \to x \in ⋃ R_{1} [B])$
12	11	com12	$⊢ A \in ⋃ R_{1} [B] \to (x \in A \to x \in ⋃ R_{1} [B])$
13	12	ralrimiv	$⊢ A \in ⋃ R_{1} [B] \to \forall x \in A x \in ⋃ R_{1} [B]$
14		r1filimi	$⊢ (A \in Fin \land \forall x \in A x \in ⋃ R_{1} [B] \land Lim B) \to A \in ⋃ R_{1} [B]$
15	14	3com23	$⊢ (A \in Fin \land Lim B \land \forall x \in A x \in ⋃ R_{1} [B]) \to A \in ⋃ R_{1} [B]$
16	15	3expia	$⊢ (A \in Fin \land Lim B) \to (\forall x \in A x \in ⋃ R_{1} [B] \to A \in ⋃ R_{1} [B])$
17	13 16	impbid2	$⊢ (A \in Fin \land Lim B) \to (A \in ⋃ R_{1} [B] \leftrightarrow \forall x \in A x \in ⋃ R_{1} [B])$