[Merged by Bors] - feat: A disjoint union is finite iff all sets are finite, and all but finitely many are empty

[Merged by Bors] - feat: A disjoint union is finite iff all sets are finite, and all but finitely many are empty #38559