r1filimi

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