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		r1elcl	⊢ ( ( 𝐴 ∈ ( 𝑅1 ‘ 𝑦 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ( 𝑅1 ‘ 𝑦 ) )
2	1	expcom	⊢ ( 𝑥 ∈ 𝐴 → ( 𝐴 ∈ ( 𝑅1 ‘ 𝑦 ) → 𝑥 ∈ ( 𝑅1 ‘ 𝑦 ) ) )
3	2	reximdv	⊢ ( 𝑥 ∈ 𝐴 → ( ∃ 𝑦 ∈ 𝐵 𝐴 ∈ ( 𝑅1 ‘ 𝑦 ) → ∃ 𝑦 ∈ 𝐵 𝑥 ∈ ( 𝑅1 ‘ 𝑦 ) ) )
4		r1funlim	⊢ ( Fun 𝑅1 ∧ Lim dom 𝑅1 )
5	4	simpli	⊢ Fun 𝑅1
6		eluniima	⊢ ( Fun 𝑅1 → ( 𝐴 ∈ ∪ ( 𝑅1 “ 𝐵 ) ↔ ∃ 𝑦 ∈ 𝐵 𝐴 ∈ ( 𝑅1 ‘ 𝑦 ) ) )
7	5 6	ax-mp	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ 𝐵 ) ↔ ∃ 𝑦 ∈ 𝐵 𝐴 ∈ ( 𝑅1 ‘ 𝑦 ) )
8		eluniima	⊢ ( Fun 𝑅1 → ( 𝑥 ∈ ∪ ( 𝑅1 “ 𝐵 ) ↔ ∃ 𝑦 ∈ 𝐵 𝑥 ∈ ( 𝑅1 ‘ 𝑦 ) ) )
9	5 8	ax-mp	⊢ ( 𝑥 ∈ ∪ ( 𝑅1 “ 𝐵 ) ↔ ∃ 𝑦 ∈ 𝐵 𝑥 ∈ ( 𝑅1 ‘ 𝑦 ) )
10	3 7 9	3imtr4g	⊢ ( 𝑥 ∈ 𝐴 → ( 𝐴 ∈ ∪ ( 𝑅1 “ 𝐵 ) → 𝑥 ∈ ∪ ( 𝑅1 “ 𝐵 ) ) )
11	10	com12	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ 𝐵 ) → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ∪ ( 𝑅1 “ 𝐵 ) ) )
12	11	ralrimiv	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ 𝐵 ) → ∀ 𝑥 ∈ 𝐴 𝑥 ∈ ∪ ( 𝑅1 “ 𝐵 ) )
13		r1filimi	⊢ ( ( 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ ∪ ( 𝑅1 “ 𝐵 ) ∧ Lim 𝐵 ) → 𝐴 ∈ ∪ ( 𝑅1 “ 𝐵 ) )
14	13	3com23	⊢ ( ( 𝐴 ∈ Fin ∧ Lim 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ ∪ ( 𝑅1 “ 𝐵 ) ) → 𝐴 ∈ ∪ ( 𝑅1 “ 𝐵 ) )
15	14	3expia	⊢ ( ( 𝐴 ∈ Fin ∧ Lim 𝐵 ) → ( ∀ 𝑥 ∈ 𝐴 𝑥 ∈ ∪ ( 𝑅1 “ 𝐵 ) → 𝐴 ∈ ∪ ( 𝑅1 “ 𝐵 ) ) )
16	12 15	impbid2	⊢ ( ( 𝐴 ∈ Fin ∧ Lim 𝐵 ) → ( 𝐴 ∈ ∪ ( 𝑅1 “ 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ ∪ ( 𝑅1 “ 𝐵 ) ) )