r1filimi

Description: If all elements of a finite set appear in the cumulative hierarchy prior to a limit ordinal, then that set also appears in the cumulative hierarchy prior to the limit ordinal. (Contributed by BTernaryTau, 19-Jan-2026)

		Ref	Expression
	Assertion	r1filimi	$⊢ (A \in Fin \land \forall x \in A x \in ⋃ R_{1} [B] \land Lim B) \to A \in ⋃ R_{1} [B]$

Proof

Step	Hyp	Ref	Expression
1		raleq	$⊢ a = A \to (\forall x \in a x \in ⋃ R_{1} [B] \leftrightarrow \forall x \in A x \in ⋃ R_{1} [B])$
2		eleq1	$⊢ a = A \to (a \in ⋃ R_{1} [On] \leftrightarrow A \in ⋃ R_{1} [On])$
3	1 2	imbi12d	$⊢ a = A \to ((\forall x \in a x \in ⋃ R_{1} [B] \to a \in ⋃ R_{1} [On]) \leftrightarrow (\forall x \in A x \in ⋃ R_{1} [B] \to A \in ⋃ R_{1} [On]))$
4	3	imbi2d	$⊢ a = A \to ((Lim B \to (\forall x \in a x \in ⋃ R_{1} [B] \to a \in ⋃ R_{1} [On])) \leftrightarrow (Lim B \to (\forall x \in A x \in ⋃ R_{1} [B] \to A \in ⋃ R_{1} [On])))$
5		r1fun	$⊢ Fun R_{1}$
6		eluniima	$⊢ Fun R_{1} \to (x \in ⋃ R_{1} [B] \leftrightarrow \exists y \in B x \in R_{1} (y))$
7	5 6	ax-mp	$⊢ x \in ⋃ R_{1} [B] \leftrightarrow \exists y \in B x \in R_{1} (y)$
8		limord	$⊢ Lim B \to Ord B$
9		ordsson	$⊢ Ord B \to B \subseteq On$
10	8 9	syl	$⊢ Lim B \to B \subseteq On$
11	10	sseld	$⊢ Lim B \to (y \in B \to y \in On)$
12	11	anim1d	$⊢ Lim B \to ((y \in B \land x \in R_{1} (y)) \to (y \in On \land x \in R_{1} (y)))$
13	12	reximdv2	$⊢ Lim B \to (\exists y \in B x \in R_{1} (y) \to \exists y \in On x \in R_{1} (y))$
14	7 13	biimtrid	$⊢ Lim B \to (x \in ⋃ R_{1} [B] \to \exists y \in On x \in R_{1} (y))$
15	14	ralimdv	$⊢ Lim B \to (\forall x \in a x \in ⋃ R_{1} [B] \to \forall x \in a \exists y \in On x \in R_{1} (y))$
16		vex	$⊢ a \in V$
17	16	tz9.12	$⊢ \forall x \in a \exists y \in On x \in R_{1} (y) \to \exists y \in On a \in R_{1} (y)$
18		eluniima	$⊢ Fun R_{1} \to (a \in ⋃ R_{1} [On] \leftrightarrow \exists y \in On a \in R_{1} (y))$
19	5 18	ax-mp	$⊢ a \in ⋃ R_{1} [On] \leftrightarrow \exists y \in On a \in R_{1} (y)$
20	17 19	sylibr	$⊢ \forall x \in a \exists y \in On x \in R_{1} (y) \to a \in ⋃ R_{1} [On]$
21	15 20	syl6	$⊢ Lim B \to (\forall x \in a x \in ⋃ R_{1} [B] \to a \in ⋃ R_{1} [On])$
22	4 21	vtoclg	$⊢ A \in Fin \to (Lim B \to (\forall x \in A x \in ⋃ R_{1} [B] \to A \in ⋃ R_{1} [On]))$
23	22	impcomd	$⊢ A \in Fin \to ((\forall x \in A x \in ⋃ R_{1} [B] \land Lim B) \to A \in ⋃ R_{1} [On])$
24	23	3impib	$⊢ (A \in Fin \land \forall x \in A x \in ⋃ R_{1} [B] \land Lim B) \to A \in ⋃ R_{1} [On]$
25		simp3	$⊢ (A \in Fin \land \forall x \in A x \in ⋃ R_{1} [B] \land Lim B) \to Lim B$
26		simp1	$⊢ (A \in Fin \land \forall x \in A x \in ⋃ R_{1} [B] \land Lim B) \to A \in Fin$
27		eluniima	$⊢ Fun R_{1} \to (x \in ⋃ R_{1} [B] \leftrightarrow \exists z \in B x \in R_{1} (z))$
28	5 27	ax-mp	$⊢ x \in ⋃ R_{1} [B] \leftrightarrow \exists z \in B x \in R_{1} (z)$
29		df-rex	$⊢ \exists z \in B x \in R_{1} (z) \leftrightarrow \exists z (z \in B \land x \in R_{1} (z))$
30		rankr1ai	$⊢ x \in R_{1} (z) \to rank (x) \in z$
31		ordtr1	$⊢ Ord B \to ((rank (x) \in z \land z \in B) \to rank (x) \in B)$
32	30 31	sylani	$⊢ Ord B \to ((x \in R_{1} (z) \land z \in B) \to rank (x) \in B)$
33	32	ancomsd	$⊢ Ord B \to ((z \in B \land x \in R_{1} (z)) \to rank (x) \in B)$
34	33	exlimdv	$⊢ Ord B \to (\exists z (z \in B \land x \in R_{1} (z)) \to rank (x) \in B)$
35	29 34	biimtrid	$⊢ Ord B \to (\exists z \in B x \in R_{1} (z) \to rank (x) \in B)$
36	28 35	biimtrid	$⊢ Ord B \to (x \in ⋃ R_{1} [B] \to rank (x) \in B)$
37	36	ralimdv	$⊢ Ord B \to (\forall x \in A x \in ⋃ R_{1} [B] \to \forall x \in A rank (x) \in B)$
38	8 37	syl	$⊢ Lim B \to (\forall x \in A x \in ⋃ R_{1} [B] \to \forall x \in A rank (x) \in B)$
39	38	impcom	$⊢ (\forall x \in A x \in ⋃ R_{1} [B] \land Lim B) \to \forall x \in A rank (x) \in B$
40	39	3adant1	$⊢ (A \in Fin \land \forall x \in A x \in ⋃ R_{1} [B] \land Lim B) \to \forall x \in A rank (x) \in B$
41		rankfilimbi	$⊢ ((A \in Fin \land A \in ⋃ R_{1} [On]) \land (\forall x \in A rank (x) \in B \land Lim B)) \to rank (A) \in B$
42	26 24 40 25 41	syl22anc	$⊢ (A \in Fin \land \forall x \in A x \in ⋃ R_{1} [B] \land Lim B) \to rank (A) \in B$
43		fveq2	$⊢ w = suc rank (A) \to R_{1} (w) = R_{1} (suc rank (A))$
44	43	eleq2d	$⊢ w = suc rank (A) \to (A \in R_{1} (w) \leftrightarrow A \in R_{1} (suc rank (A)))$
45		limsuc	$⊢ Lim B \to (rank (A) \in B \leftrightarrow suc rank (A) \in B)$
46	45	biimpa	$⊢ (Lim B \land rank (A) \in B) \to suc rank (A) \in B$
47	46	3adant1	$⊢ (A \in ⋃ R_{1} [On] \land Lim B \land rank (A) \in B) \to suc rank (A) \in B$
48		rankidb	$⊢ A \in ⋃ R_{1} [On] \to A \in R_{1} (suc rank (A))$
49	48	3ad2ant1	$⊢ (A \in ⋃ R_{1} [On] \land Lim B \land rank (A) \in B) \to A \in R_{1} (suc rank (A))$
50	44 47 49	rspcedvdw	$⊢ (A \in ⋃ R_{1} [On] \land Lim B \land rank (A) \in B) \to \exists w \in B A \in R_{1} (w)$
51		eluniima	$⊢ Fun R_{1} \to (A \in ⋃ R_{1} [B] \leftrightarrow \exists w \in B A \in R_{1} (w))$
52	5 51	ax-mp	$⊢ A \in ⋃ R_{1} [B] \leftrightarrow \exists w \in B A \in R_{1} (w)$
53	50 52	sylibr	$⊢ (A \in ⋃ R_{1} [On] \land Lim B \land rank (A) \in B) \to A \in ⋃ R_{1} [B]$
54	24 25 42 53	syl3anc	$⊢ (A \in Fin \land \forall x \in A x \in ⋃ R_{1} [B] \land Lim B) \to A \in ⋃ R_{1} [B]$

Metamath Proof Explorer

Theorem r1filimi

Proof