Theorem 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	⊢ ( ( 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ ∪ ( 𝑅1 “ 𝐵 ) ∧ Lim 𝐵 ) → 𝐴 ∈ ∪ ( 𝑅1 “ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		raleq	⊢ ( 𝑎 = 𝐴 → ( ∀ 𝑥 ∈ 𝑎 𝑥 ∈ ∪ ( 𝑅1 “ 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ ∪ ( 𝑅1 “ 𝐵 ) ) )
2		eleq1	⊢ ( 𝑎 = 𝐴 → ( 𝑎 ∈ ∪ ( 𝑅1 “ On ) ↔ 𝐴 ∈ ∪ ( 𝑅1 “ On ) ) )
3	1 2	imbi12d	⊢ ( 𝑎 = 𝐴 → ( ( ∀ 𝑥 ∈ 𝑎 𝑥 ∈ ∪ ( 𝑅1 “ 𝐵 ) → 𝑎 ∈ ∪ ( 𝑅1 “ On ) ) ↔ ( ∀ 𝑥 ∈ 𝐴 𝑥 ∈ ∪ ( 𝑅1 “ 𝐵 ) → 𝐴 ∈ ∪ ( 𝑅1 “ On ) ) ) )
4	3	imbi2d	⊢ ( 𝑎 = 𝐴 → ( ( Lim 𝐵 → ( ∀ 𝑥 ∈ 𝑎 𝑥 ∈ ∪ ( 𝑅1 “ 𝐵 ) → 𝑎 ∈ ∪ ( 𝑅1 “ On ) ) ) ↔ ( Lim 𝐵 → ( ∀ 𝑥 ∈ 𝐴 𝑥 ∈ ∪ ( 𝑅1 “ 𝐵 ) → 𝐴 ∈ ∪ ( 𝑅1 “ On ) ) ) ) )
5		r1funlim	⊢ ( Fun 𝑅1 ∧ Lim dom 𝑅1 )
6	5	simpli	⊢ Fun 𝑅1
7		eluniima	⊢ ( Fun 𝑅1 → ( 𝑥 ∈ ∪ ( 𝑅1 “ 𝐵 ) ↔ ∃ 𝑦 ∈ 𝐵 𝑥 ∈ ( 𝑅1 ‘ 𝑦 ) ) )
8	6 7	ax-mp	⊢ ( 𝑥 ∈ ∪ ( 𝑅1 “ 𝐵 ) ↔ ∃ 𝑦 ∈ 𝐵 𝑥 ∈ ( 𝑅1 ‘ 𝑦 ) )
9		limord	⊢ ( Lim 𝐵 → Ord 𝐵 )
10		ordsson	⊢ ( Ord 𝐵 → 𝐵 ⊆ On )
11	9 10	syl	⊢ ( Lim 𝐵 → 𝐵 ⊆ On )
12	11	sseld	⊢ ( Lim 𝐵 → ( 𝑦 ∈ 𝐵 → 𝑦 ∈ On ) )
13	12	anim1d	⊢ ( Lim 𝐵 → ( ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝑅1 ‘ 𝑦 ) ) → ( 𝑦 ∈ On ∧ 𝑥 ∈ ( 𝑅1 ‘ 𝑦 ) ) ) )
14	13	reximdv2	⊢ ( Lim 𝐵 → ( ∃ 𝑦 ∈ 𝐵 𝑥 ∈ ( 𝑅1 ‘ 𝑦 ) → ∃ 𝑦 ∈ On 𝑥 ∈ ( 𝑅1 ‘ 𝑦 ) ) )
15	8 14	biimtrid	⊢ ( Lim 𝐵 → ( 𝑥 ∈ ∪ ( 𝑅1 “ 𝐵 ) → ∃ 𝑦 ∈ On 𝑥 ∈ ( 𝑅1 ‘ 𝑦 ) ) )
16	15	ralimdv	⊢ ( Lim 𝐵 → ( ∀ 𝑥 ∈ 𝑎 𝑥 ∈ ∪ ( 𝑅1 “ 𝐵 ) → ∀ 𝑥 ∈ 𝑎 ∃ 𝑦 ∈ On 𝑥 ∈ ( 𝑅1 ‘ 𝑦 ) ) )
17		vex	⊢ 𝑎 ∈ V
18	17	tz9.12	⊢ ( ∀ 𝑥 ∈ 𝑎 ∃ 𝑦 ∈ On 𝑥 ∈ ( 𝑅1 ‘ 𝑦 ) → ∃ 𝑦 ∈ On 𝑎 ∈ ( 𝑅1 ‘ 𝑦 ) )
19		eluniima	⊢ ( Fun 𝑅1 → ( 𝑎 ∈ ∪ ( 𝑅1 “ On ) ↔ ∃ 𝑦 ∈ On 𝑎 ∈ ( 𝑅1 ‘ 𝑦 ) ) )
20	6 19	ax-mp	⊢ ( 𝑎 ∈ ∪ ( 𝑅1 “ On ) ↔ ∃ 𝑦 ∈ On 𝑎 ∈ ( 𝑅1 ‘ 𝑦 ) )
21	18 20	sylibr	⊢ ( ∀ 𝑥 ∈ 𝑎 ∃ 𝑦 ∈ On 𝑥 ∈ ( 𝑅1 ‘ 𝑦 ) → 𝑎 ∈ ∪ ( 𝑅1 “ On ) )
22	16 21	syl6	⊢ ( Lim 𝐵 → ( ∀ 𝑥 ∈ 𝑎 𝑥 ∈ ∪ ( 𝑅1 “ 𝐵 ) → 𝑎 ∈ ∪ ( 𝑅1 “ On ) ) )
23	4 22	vtoclg	⊢ ( 𝐴 ∈ Fin → ( Lim 𝐵 → ( ∀ 𝑥 ∈ 𝐴 𝑥 ∈ ∪ ( 𝑅1 “ 𝐵 ) → 𝐴 ∈ ∪ ( 𝑅1 “ On ) ) ) )
24	23	impcomd	⊢ ( 𝐴 ∈ Fin → ( ( ∀ 𝑥 ∈ 𝐴 𝑥 ∈ ∪ ( 𝑅1 “ 𝐵 ) ∧ Lim 𝐵 ) → 𝐴 ∈ ∪ ( 𝑅1 “ On ) ) )
25	24	3impib	⊢ ( ( 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ ∪ ( 𝑅1 “ 𝐵 ) ∧ Lim 𝐵 ) → 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
26		simp3	⊢ ( ( 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ ∪ ( 𝑅1 “ 𝐵 ) ∧ Lim 𝐵 ) → Lim 𝐵 )
27		simp1	⊢ ( ( 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ ∪ ( 𝑅1 “ 𝐵 ) ∧ Lim 𝐵 ) → 𝐴 ∈ Fin )
28		eluniima	⊢ ( Fun 𝑅1 → ( 𝑥 ∈ ∪ ( 𝑅1 “ 𝐵 ) ↔ ∃ 𝑧 ∈ 𝐵 𝑥 ∈ ( 𝑅1 ‘ 𝑧 ) ) )
29	6 28	ax-mp	⊢ ( 𝑥 ∈ ∪ ( 𝑅1 “ 𝐵 ) ↔ ∃ 𝑧 ∈ 𝐵 𝑥 ∈ ( 𝑅1 ‘ 𝑧 ) )
30		df-rex	⊢ ( ∃ 𝑧 ∈ 𝐵 𝑥 ∈ ( 𝑅1 ‘ 𝑧 ) ↔ ∃ 𝑧 ( 𝑧 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝑅1 ‘ 𝑧 ) ) )
31		rankr1ai	⊢ ( 𝑥 ∈ ( 𝑅1 ‘ 𝑧 ) → ( rank ‘ 𝑥 ) ∈ 𝑧 )
32		ordtr1	⊢ ( Ord 𝐵 → ( ( ( rank ‘ 𝑥 ) ∈ 𝑧 ∧ 𝑧 ∈ 𝐵 ) → ( rank ‘ 𝑥 ) ∈ 𝐵 ) )
33	31 32	sylani	⊢ ( Ord 𝐵 → ( ( 𝑥 ∈ ( 𝑅1 ‘ 𝑧 ) ∧ 𝑧 ∈ 𝐵 ) → ( rank ‘ 𝑥 ) ∈ 𝐵 ) )
34	33	ancomsd	⊢ ( Ord 𝐵 → ( ( 𝑧 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝑅1 ‘ 𝑧 ) ) → ( rank ‘ 𝑥 ) ∈ 𝐵 ) )
35	34	exlimdv	⊢ ( Ord 𝐵 → ( ∃ 𝑧 ( 𝑧 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝑅1 ‘ 𝑧 ) ) → ( rank ‘ 𝑥 ) ∈ 𝐵 ) )
36	30 35	biimtrid	⊢ ( Ord 𝐵 → ( ∃ 𝑧 ∈ 𝐵 𝑥 ∈ ( 𝑅1 ‘ 𝑧 ) → ( rank ‘ 𝑥 ) ∈ 𝐵 ) )
37	29 36	biimtrid	⊢ ( Ord 𝐵 → ( 𝑥 ∈ ∪ ( 𝑅1 “ 𝐵 ) → ( rank ‘ 𝑥 ) ∈ 𝐵 ) )
38	37	ralimdv	⊢ ( Ord 𝐵 → ( ∀ 𝑥 ∈ 𝐴 𝑥 ∈ ∪ ( 𝑅1 “ 𝐵 ) → ∀ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ∈ 𝐵 ) )
39	9 38	syl	⊢ ( Lim 𝐵 → ( ∀ 𝑥 ∈ 𝐴 𝑥 ∈ ∪ ( 𝑅1 “ 𝐵 ) → ∀ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ∈ 𝐵 ) )
40	39	impcom	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝑥 ∈ ∪ ( 𝑅1 “ 𝐵 ) ∧ Lim 𝐵 ) → ∀ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ∈ 𝐵 )
41	40	3adant1	⊢ ( ( 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ ∪ ( 𝑅1 “ 𝐵 ) ∧ Lim 𝐵 ) → ∀ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ∈ 𝐵 )
42		rankfilimbi	⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ∈ ∪ ( 𝑅1 “ On ) ) ∧ ( ∀ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ∈ 𝐵 ∧ Lim 𝐵 ) ) → ( rank ‘ 𝐴 ) ∈ 𝐵 )
43	27 25 41 26 42	syl22anc	⊢ ( ( 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ ∪ ( 𝑅1 “ 𝐵 ) ∧ Lim 𝐵 ) → ( rank ‘ 𝐴 ) ∈ 𝐵 )
44		fveq2	⊢ ( 𝑤 = suc ( rank ‘ 𝐴 ) → ( 𝑅1 ‘ 𝑤 ) = ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) )
45	44	eleq2d	⊢ ( 𝑤 = suc ( rank ‘ 𝐴 ) → ( 𝐴 ∈ ( 𝑅1 ‘ 𝑤 ) ↔ 𝐴 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) ) )
46		limsuc	⊢ ( Lim 𝐵 → ( ( rank ‘ 𝐴 ) ∈ 𝐵 ↔ suc ( rank ‘ 𝐴 ) ∈ 𝐵 ) )
47	46	biimpa	⊢ ( ( Lim 𝐵 ∧ ( rank ‘ 𝐴 ) ∈ 𝐵 ) → suc ( rank ‘ 𝐴 ) ∈ 𝐵 )
48	47	3adant1	⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ Lim 𝐵 ∧ ( rank ‘ 𝐴 ) ∈ 𝐵 ) → suc ( rank ‘ 𝐴 ) ∈ 𝐵 )
49		rankidb	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝐴 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) )
50	49	3ad2ant1	⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ Lim 𝐵 ∧ ( rank ‘ 𝐴 ) ∈ 𝐵 ) → 𝐴 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) )
51	45 48 50	rspcedvdw	⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ Lim 𝐵 ∧ ( rank ‘ 𝐴 ) ∈ 𝐵 ) → ∃ 𝑤 ∈ 𝐵 𝐴 ∈ ( 𝑅1 ‘ 𝑤 ) )
52		eluniima	⊢ ( Fun 𝑅1 → ( 𝐴 ∈ ∪ ( 𝑅1 “ 𝐵 ) ↔ ∃ 𝑤 ∈ 𝐵 𝐴 ∈ ( 𝑅1 ‘ 𝑤 ) ) )
53	6 52	ax-mp	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ 𝐵 ) ↔ ∃ 𝑤 ∈ 𝐵 𝐴 ∈ ( 𝑅1 ‘ 𝑤 ) )
54	51 53	sylibr	⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ Lim 𝐵 ∧ ( rank ‘ 𝐴 ) ∈ 𝐵 ) → 𝐴 ∈ ∪ ( 𝑅1 “ 𝐵 ) )
55	25 26 43 54	syl3anc	⊢ ( ( 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ ∪ ( 𝑅1 “ 𝐵 ) ∧ Lim 𝐵 ) → 𝐴 ∈ ∪ ( 𝑅1 “ 𝐵 ) )