Theorem unifpw

Description: A set is the union of its finite subsets. (Contributed by Stefan O'Rear, 2-Apr-2015)

	Ref	Expression
Assertion	unifpw	$$⊢\bigcup \left(𝒫A\cap \mathrm{Fin}\right)=A$$

Proof

Step	Hyp	Ref	Expression
1		inss1	$$⊢𝒫A\cap \mathrm{Fin}\subseteq 𝒫A$$
2	1	unissi	$$⊢\bigcup \left(𝒫A\cap \mathrm{Fin}\right)\subseteq \bigcup 𝒫A$$
3		unipw	$$⊢\bigcup 𝒫A=A$$
4	2 3	sseqtri	$$⊢\bigcup \left(𝒫A\cap \mathrm{Fin}\right)\subseteq A$$
5	4	sseli	$$⊢a\in \bigcup \left(𝒫A\cap \mathrm{Fin}\right)\to a\in A$$
6		snelpwi	$$⊢a\in A\to \left\{a\right\}\in 𝒫A$$
7		snfi	$$⊢\left\{a\right\}\in \mathrm{Fin}$$
8	7	a1i	$$⊢a\in A\to \left\{a\right\}\in \mathrm{Fin}$$
9	6 8	elind	$$⊢a\in A\to \left\{a\right\}\in \left(𝒫A\cap \mathrm{Fin}\right)$$
10		elssuni	$$⊢\left\{a\right\}\in \left(𝒫A\cap \mathrm{Fin}\right)\to \left\{a\right\}\subseteq \bigcup \left(𝒫A\cap \mathrm{Fin}\right)$$
11	9 10	syl	$$⊢a\in A\to \left\{a\right\}\subseteq \bigcup \left(𝒫A\cap \mathrm{Fin}\right)$$
12		snidg	$$⊢a\in A\to a\in \left\{a\right\}$$
13	11 12	sseldd	$$⊢a\in A\to a\in \bigcup \left(𝒫A\cap \mathrm{Fin}\right)$$
14	5 13	impbii	$$⊢a\in \bigcup \left(𝒫A\cap \mathrm{Fin}\right)\leftrightarrow a\in A$$
15	14	eqriv	$$⊢\bigcup \left(𝒫A\cap \mathrm{Fin}\right)=A$$