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