Theorem rabrexfi

Description: Conditions for a class abstraction with a restricted existential quantification to be finite. (Contributed by Thierry Arnoux, 6-Jul-2025)

	Ref	Expression
Hypotheses	rabrexfi.1	⊢ ( 𝜑 → 𝐵 ∈ Fin )
	rabrexfi.2	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → { 𝑥 ∈ 𝐴 ∣ 𝜓 } ∈ Fin )
Assertion	rabrexfi	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ ∃ 𝑦 ∈ 𝐵 𝜓 } ∈ Fin )

Proof

Step	Hyp	Ref	Expression
1		rabrexfi.1	⊢ ( 𝜑 → 𝐵 ∈ Fin )
2		rabrexfi.2	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → { 𝑥 ∈ 𝐴 ∣ 𝜓 } ∈ Fin )
3		iunrab	⊢ ∪ 𝑦 ∈ 𝐵 { 𝑥 ∈ 𝐴 ∣ 𝜓 } = { 𝑥 ∈ 𝐴 ∣ ∃ 𝑦 ∈ 𝐵 𝜓 }
4	2	ralrimiva	⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐵 { 𝑥 ∈ 𝐴 ∣ 𝜓 } ∈ Fin )
5		iunfi	⊢ ( ( 𝐵 ∈ Fin ∧ ∀ 𝑦 ∈ 𝐵 { 𝑥 ∈ 𝐴 ∣ 𝜓 } ∈ Fin ) → ∪ 𝑦 ∈ 𝐵 { 𝑥 ∈ 𝐴 ∣ 𝜓 } ∈ Fin )
6	1 4 5	syl2anc	⊢ ( 𝜑 → ∪ 𝑦 ∈ 𝐵 { 𝑥 ∈ 𝐴 ∣ 𝜓 } ∈ Fin )
7	3 6	eqeltrrid	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ ∃ 𝑦 ∈ 𝐵 𝜓 } ∈ Fin )