proposition: Lemma bigcup_disjointP U P F : reflect (forall i : I, P i -> [disjoint U & F i]) [disjoint U & \bigcup_(i | P i) F i].
proof: Proof. apply: (iffP idP) => [disUF i Pp|]; last exact: bigcup_disjoint. apply: disjointWr disUF; exact: bigcup_sup. Qed.
imports: mathcomp(all_ssreflect)