Theorem fiunicl

Description: If a set is closed under the union of two sets, then it is closed under finite union. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	fiunicl.1	$$⊢\left(\phi \wedge x\in A\wedge y\in A\right)\to x\cup y\in A$$
	fiunicl.2	$$⊢\phi \to A\in \mathrm{Fin}$$
	fiunicl.3	$$⊢\phi \to A\ne \varnothing$$
Assertion	fiunicl	$$⊢\phi \to \bigcup A\in A$$

Proof

Step	Hyp	Ref	Expression
1		fiunicl.1	$$⊢\left(\phi \wedge x\in A\wedge y\in A\right)\to x\cup y\in A$$
2		fiunicl.2	$$⊢\phi \to A\in \mathrm{Fin}$$
3		fiunicl.3	$$⊢\phi \to A\ne \varnothing$$
4		uniiun	$$⊢\bigcup A=\bigcup _{z\in A}z$$
5		nfv	$$⊢Ⅎz\phi$$
6		simpr	$$⊢\left(\phi \wedge z\in A\right)\to z\in A$$
7	5 6 1 2 3	fiiuncl	$$⊢\phi \to \bigcup _{z\in A}z\in A$$
8	4 7	eqeltrid	$$⊢\phi \to \bigcup A\in A$$