Theorem unifpw

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

	Ref	Expression
Assertion	unifpw	⊢ ∪ ( 𝒫 𝐴 ∩ Fin ) = 𝐴

Proof

Step	Hyp	Ref	Expression
1		inss1	⊢ ( 𝒫 𝐴 ∩ Fin ) ⊆ 𝒫 𝐴
2	1	unissi	⊢ ∪ ( 𝒫 𝐴 ∩ Fin ) ⊆ ∪ 𝒫 𝐴
3		unipw	⊢ ∪ 𝒫 𝐴 = 𝐴
4	2 3	sseqtri	⊢ ∪ ( 𝒫 𝐴 ∩ Fin ) ⊆ 𝐴
5	4	sseli	⊢ ( 𝑎 ∈ ∪ ( 𝒫 𝐴 ∩ Fin ) → 𝑎 ∈ 𝐴 )
6		snelpwi	⊢ ( 𝑎 ∈ 𝐴 → { 𝑎 } ∈ 𝒫 𝐴 )
7		snfi	⊢ { 𝑎 } ∈ Fin
8	7	a1i	⊢ ( 𝑎 ∈ 𝐴 → { 𝑎 } ∈ Fin )
9	6 8	elind	⊢ ( 𝑎 ∈ 𝐴 → { 𝑎 } ∈ ( 𝒫 𝐴 ∩ Fin ) )
10		elssuni	⊢ ( { 𝑎 } ∈ ( 𝒫 𝐴 ∩ Fin ) → { 𝑎 } ⊆ ∪ ( 𝒫 𝐴 ∩ Fin ) )
11	9 10	syl	⊢ ( 𝑎 ∈ 𝐴 → { 𝑎 } ⊆ ∪ ( 𝒫 𝐴 ∩ Fin ) )
12		snidg	⊢ ( 𝑎 ∈ 𝐴 → 𝑎 ∈ { 𝑎 } )
13	11 12	sseldd	⊢ ( 𝑎 ∈ 𝐴 → 𝑎 ∈ ∪ ( 𝒫 𝐴 ∩ Fin ) )
14	5 13	impbii	⊢ ( 𝑎 ∈ ∪ ( 𝒫 𝐴 ∩ Fin ) ↔ 𝑎 ∈ 𝐴 )
15	14	eqriv	⊢ ∪ ( 𝒫 𝐴 ∩ Fin ) = 𝐴