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 ( 𝒫 𝐴 ∩ 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 ) = 𝐴