Metamath Proof Explorer


Theorem unifpw

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

Ref Expression
Assertion unifpw 𝒫AFin=A

Proof

Step Hyp Ref Expression
1 inss1 𝒫AFin𝒫A
2 1 unissi 𝒫AFin𝒫A
3 unipw 𝒫A=A
4 2 3 sseqtri 𝒫AFinA
5 4 sseli a𝒫AFinaA
6 snelpwi aAa𝒫A
7 snfi aFin
8 7 a1i aAaFin
9 6 8 elind aAa𝒫AFin
10 elssuni a𝒫AFina𝒫AFin
11 9 10 syl aAa𝒫AFin
12 snidg aAaa
13 11 12 sseldd aAa𝒫AFin
14 5 13 impbii a𝒫AFinaA
15 14 eqriv 𝒫AFin=A