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	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) → ∪ 𝐴 ∈ Fin )

Proof

Step	Hyp	Ref	Expression
1		dfss3	⊢ ( 𝐴 ⊆ Fin ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ Fin )
2		uniiun	⊢ ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 𝑥
3		iunfi	⊢ ( ( 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ Fin ) → ∪ 𝑥 ∈ 𝐴 𝑥 ∈ Fin )
4	2 3	eqeltrid	⊢ ( ( 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ Fin ) → ∪ 𝐴 ∈ Fin )
5	1 4	sylan2b	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) → ∪ 𝐴 ∈ Fin )