Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Union
Finite sets
unifpw
Next ⟩
f1opwfi
Metamath Proof Explorer
Ascii
Unicode
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