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 𝒫 A Fin = A

Proof

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