Metamath Proof Explorer

Theorem unifi

Description: The finite union of finite sets is finite. Exercise 13 of Enderton p. 144. (Contributed by NM, 22-Aug-2008) (Revised by Mario Carneiro, 31-Aug-2015)

		Ref	Expression
	Assertion	unifi	$⊢ (A \in Fin \land A \subseteq Fin) \to ⋃ A \in Fin$

Proof

Step	Hyp	Ref	Expression
1		dfss3	$⊢ A \subseteq Fin \leftrightarrow \forall x \in A x \in Fin$
2		uniiun	$⊢ ⋃ A = ⋃_{x \in A} x$
3		iunfi	$⊢ (A \in Fin \land \forall x \in A x \in Fin) \to ⋃_{x \in A} x \in Fin$
4	2 3	eqeltrid	$⊢ (A \in Fin \land \forall x \in A x \in Fin) \to ⋃ A \in Fin$
5	1 4	sylan2b	$⊢ (A \in Fin \land A \subseteq Fin) \to ⋃ A \in Fin$