theorem IsChain.pairwiseDisjoint_iUnion₂ {α : Type u_1} {β : Type u_2} [PartialOrder β] [OrderBot β] (c : Set (Set α)) (hc : IsChain (fun (x1 x2 : Set α) => x1 ⊆ x2) c) (f : α → β) (h : ∀ s ∈ c, s.PairwiseDisjoint f) : (⋃ s ∈ c, s).PairwiseDisjoint f