unifpw

Description: A set is the union of its finite subsets. (Contributed by Stefan O'Rear, 2-Apr-2015)

		Ref	Expression
	Assertion	unifpw	$⊢ ⋃ (𝒫 A \cap Fin) = A$

Step	Hyp	Ref	Expression
1		inss1	$⊢ 𝒫 A \cap Fin \subseteq 𝒫 A$
2	1	unissi	$⊢ ⋃ (𝒫 A \cap Fin) \subseteq ⋃ 𝒫 A$
3		unipw	$⊢ ⋃ 𝒫 A = A$
4	2 3	sseqtri	$⊢ ⋃ (𝒫 A \cap Fin) \subseteq A$
5	4	sseli	$⊢ a \in ⋃ (𝒫 A \cap Fin) \to a \in A$
6		snelpwi	$⊢ a \in A \to \{a\} \in 𝒫 A$
7		snfi	$⊢ \{a\} \in Fin$
8	7	a1i	$⊢ a \in A \to \{a\} \in Fin$
9	6 8	elind	$⊢ a \in A \to \{a\} \in (𝒫 A \cap Fin)$
10		elssuni	$⊢ \{a\} \in (𝒫 A \cap Fin) \to \{a\} \subseteq ⋃ (𝒫 A \cap Fin)$
11	9 10	syl	$⊢ a \in A \to \{a\} \subseteq ⋃ (𝒫 A \cap Fin)$
12		snidg	$⊢ a \in A \to a \in \{a\}$
13	11 12	sseldd	$⊢ a \in A \to a \in ⋃ (𝒫 A \cap Fin)$
14	5 13	impbii	$⊢ a \in ⋃ (𝒫 A \cap Fin) \leftrightarrow a \in A$
15	14	eqriv	$⊢ ⋃ (𝒫 A \cap Fin) = A$

Metamath Proof Explorer