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	|- ( ( ph /\ x e. A /\ y e. A ) -> ( x u. y ) e. A )
	fiunicl.2	|- ( ph -> A e. Fin )
	fiunicl.3	|- ( ph -> A =/= (/) )
Assertion	fiunicl	|- ( ph -> U. A e. A )

Proof

Step	Hyp	Ref	Expression
1		fiunicl.1	|- ( ( ph /\ x e. A /\ y e. A ) -> ( x u. y ) e. A )
2		fiunicl.2	|- ( ph -> A e. Fin )
3		fiunicl.3	|- ( ph -> A =/= (/) )
4		uniiun	|- U. A = U_ z e. A z
5		nfv	|- F/ z ph
6		simpr	|- ( ( ph /\ z e. A ) -> z e. A )
7	5 6 1 2 3	fiiuncl	|- ( ph -> U_ z e. A z e. A )
8	4 7	eqeltrid	|- ( ph -> U. A e. A )