Theorem unfib

Description: A union is finite if and only if the operands are finite. (Contributed by AV, 10-May-2025)

	Ref	Expression
Assertion	unfib	⊢ ( ( 𝐴 ∪ 𝐵 ) ∈ Fin ↔ ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) )

Proof

Step	Hyp	Ref	Expression
1		unfir	⊢ ( ( 𝐴 ∪ 𝐵 ) ∈ Fin → ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) )
2		unfi	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( 𝐴 ∪ 𝐵 ) ∈ Fin )
3	1 2	impbii	⊢ ( ( 𝐴 ∪ 𝐵 ) ∈ Fin ↔ ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) )