This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ (φ \land x \in A \land y \in A) \to x \cup y \in A$
	fiunicl.2	$⊢ φ \to A \in Fin$
	fiunicl.3	$⊢ φ \to A \neq \emptyset$
Assertion	fiunicl	$⊢ φ \to ⋃ A \in A$

Proof

Step	Hyp	Ref	Expression
1		fiunicl.1	$⊢ (φ \land x \in A \land y \in A) \to x \cup y \in A$
2		fiunicl.2	$⊢ φ \to A \in Fin$
3		fiunicl.3	$⊢ φ \to A \neq \emptyset$
4		uniiun	$⊢ ⋃ A = ⋃_{z \in A} z$
5		nfv	$⊢ Ⅎ z φ$
6		simpr	$⊢ (φ \land z \in A) \to z \in A$
7	5 6 1 2 3	fiiuncl	$⊢ φ \to ⋃_{z \in A} z \in A$
8	4 7	eqeltrid	$⊢ φ \to ⋃ A \in A$