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 
|- U. ( ~P A i^i Fin ) = A

Proof

Step Hyp Ref Expression
1 inss1 
 |-  ( ~P A i^i Fin ) C_ ~P A
2 1 unissi 
 |-  U. ( ~P A i^i Fin ) C_ U. ~P A
3 unipw 
 |-  U. ~P A = A
4 2 3 sseqtri 
 |-  U. ( ~P A i^i Fin ) C_ A
5 4 sseli 
 |-  ( a e. U. ( ~P A i^i Fin ) -> a e. A )
6 snelpwi 
 |-  ( a e. A -> { a } e. ~P A )
7 snfi 
 |-  { a } e. Fin
8 7 a1i 
 |-  ( a e. A -> { a } e. Fin )
9 6 8 elind 
 |-  ( a e. A -> { a } e. ( ~P A i^i Fin ) )
10 elssuni 
 |-  ( { a } e. ( ~P A i^i Fin ) -> { a } C_ U. ( ~P A i^i Fin ) )
11 9 10 syl 
 |-  ( a e. A -> { a } C_ U. ( ~P A i^i Fin ) )
12 snidg 
 |-  ( a e. A -> a e. { a } )
13 11 12 sseldd 
 |-  ( a e. A -> a e. U. ( ~P A i^i Fin ) )
14 5 13 impbii 
 |-  ( a e. U. ( ~P A i^i Fin ) <-> a e. A )
15 14 eqriv 
 |-  U. ( ~P A i^i Fin ) = A