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

Proof

Step	Hyp	Ref	Expression
1		r1tr	⊢ Tr ( 𝑅1 ‘ 𝑦 )
2		trel	⊢ ( Tr ( 𝑅1 ‘ 𝑦 ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝐴 ∈ ( 𝑅1 ‘ 𝑦 ) ) → 𝑥 ∈ ( 𝑅1 ‘ 𝑦 ) ) )
3	1 2	ax-mp	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐴 ∈ ( 𝑅1 ‘ 𝑦 ) ) → 𝑥 ∈ ( 𝑅1 ‘ 𝑦 ) )
4	3	ex	⊢ ( 𝑥 ∈ 𝐴 → ( 𝐴 ∈ ( 𝑅1 ‘ 𝑦 ) → 𝑥 ∈ ( 𝑅1 ‘ 𝑦 ) ) )
5	4	reximdv	⊢ ( 𝑥 ∈ 𝐴 → ( ∃ 𝑦 ∈ 𝐵 𝐴 ∈ ( 𝑅1 ‘ 𝑦 ) → ∃ 𝑦 ∈ 𝐵 𝑥 ∈ ( 𝑅1 ‘ 𝑦 ) ) )
6		r1fun	⊢ Fun 𝑅1
7		eluniima	⊢ ( Fun 𝑅1 → ( 𝐴 ∈ ∪ ( 𝑅1 “ 𝐵 ) ↔ ∃ 𝑦 ∈ 𝐵 𝐴 ∈ ( 𝑅1 ‘ 𝑦 ) ) )
8	6 7	ax-mp	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ 𝐵 ) ↔ ∃ 𝑦 ∈ 𝐵 𝐴 ∈ ( 𝑅1 ‘ 𝑦 ) )
9		eluniima	⊢ ( Fun 𝑅1 → ( 𝑥 ∈ ∪ ( 𝑅1 “ 𝐵 ) ↔ ∃ 𝑦 ∈ 𝐵 𝑥 ∈ ( 𝑅1 ‘ 𝑦 ) ) )
10	6 9	ax-mp	⊢ ( 𝑥 ∈ ∪ ( 𝑅1 “ 𝐵 ) ↔ ∃ 𝑦 ∈ 𝐵 𝑥 ∈ ( 𝑅1 ‘ 𝑦 ) )
11	5 8 10	3imtr4g	⊢ ( 𝑥 ∈ 𝐴 → ( 𝐴 ∈ ∪ ( 𝑅1 “ 𝐵 ) → 𝑥 ∈ ∪ ( 𝑅1 “ 𝐵 ) ) )
12	11	com12	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ 𝐵 ) → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ∪ ( 𝑅1 “ 𝐵 ) ) )
13	12	ralrimiv	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ 𝐵 ) → ∀ 𝑥 ∈ 𝐴 𝑥 ∈ ∪ ( 𝑅1 “ 𝐵 ) )
14		r1filimi	⊢ ( ( 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ ∪ ( 𝑅1 “ 𝐵 ) ∧ Lim 𝐵 ) → 𝐴 ∈ ∪ ( 𝑅1 “ 𝐵 ) )
15	14	3com23	⊢ ( ( 𝐴 ∈ Fin ∧ Lim 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ ∪ ( 𝑅1 “ 𝐵 ) ) → 𝐴 ∈ ∪ ( 𝑅1 “ 𝐵 ) )
16	15	3expia	⊢ ( ( 𝐴 ∈ Fin ∧ Lim 𝐵 ) → ( ∀ 𝑥 ∈ 𝐴 𝑥 ∈ ∪ ( 𝑅1 “ 𝐵 ) → 𝐴 ∈ ∪ ( 𝑅1 “ 𝐵 ) ) )
17	13 16	impbid2	⊢ ( ( 𝐴 ∈ Fin ∧ Lim 𝐵 ) → ( 𝐴 ∈ ∪ ( 𝑅1 “ 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ ∪ ( 𝑅1 “ 𝐵 ) ) )