Theorem unifi3

Description: If a union is finite, then all its elements are finite. See unifi . (Contributed by Thierry Arnoux, 27-Aug-2017)

	Ref	Expression
Assertion	unifi3	$$⊢\bigcup A\in \mathrm{Fin}\to A\subseteq \mathrm{Fin}$$

Proof

Step	Hyp	Ref	Expression
1		elssuni	$$⊢x\in A\to x\subseteq \bigcup A$$
2		ssfi	$$⊢\left(\bigcup A\in \mathrm{Fin}\wedge x\subseteq \bigcup A\right)\to x\in \mathrm{Fin}$$
3	2	ex	$$⊢\bigcup A\in \mathrm{Fin}\to \left(x\subseteq \bigcup A\to x\in \mathrm{Fin}\right)$$
4	1 3	syl5	$$⊢\bigcup A\in \mathrm{Fin}\to \left(x\in A\to x\in \mathrm{Fin}\right)$$
5	4	ssrdv	$$⊢\bigcup A\in \mathrm{Fin}\to A\subseteq \mathrm{Fin}$$