Theorem unifpw

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

	Ref	Expression
Assertion	unifpw	|- U. ( ~P A i^i Fin ) = A

Proof

Step	Hyp	Ref	Expression
1		inss1	|- ( ~P A i^i Fin ) C_ ~P A
2	1	unissi	|- U. ( ~P A i^i Fin ) C_ U. ~P A
3		unipw	|- U. ~P A = A
4	2 3	sseqtri	|- U. ( ~P A i^i Fin ) C_ A
5	4	sseli	|- ( a e. U. ( ~P A i^i Fin ) -> a e. A )
6		snelpwi	|- ( a e. A -> { a } e. ~P A )
7		snfi	|- { a } e. Fin
8	7	a1i	|- ( a e. A -> { a } e. Fin )
9	6 8	elind	|- ( a e. A -> { a } e. ( ~P A i^i Fin ) )
10		elssuni	|- ( { a } e. ( ~P A i^i Fin ) -> { a } C_ U. ( ~P A i^i Fin ) )
11	9 10	syl	|- ( a e. A -> { a } C_ U. ( ~P A i^i Fin ) )
12		snidg	|- ( a e. A -> a e. { a } )
13	11 12	sseldd	|- ( a e. A -> a e. U. ( ~P A i^i Fin ) )
14	5 13	impbii	|- ( a e. U. ( ~P A i^i Fin ) <-> a e. A )
15	14	eqriv	|- U. ( ~P A i^i Fin ) = A