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