This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) = 𝐴