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

Metamath Proof Explorer

Theorem infpwfidom

Description: The collection of finite subsets of a set dominates the set. (We use the weaker sethood assumption ( ~P A i^i Fin ) e. _V because this theorem also implies that A is a set if ~P A i^i Fin is.) (Contributed by Mario Carneiro, 17-May-2015)

		Ref	Expression
	Assertion	infpwfidom	$⊢ 𝒫 A \cap Fin \in V \to A ≼ (𝒫 A \cap Fin)$

Proof

Step	Hyp	Ref	Expression
1		snelpwi	$⊢ x \in A \to \{x\} \in 𝒫 A$
2		snfi	$⊢ \{x\} \in Fin$
3	2	a1i	$⊢ x \in A \to \{x\} \in Fin$
4	1 3	elind	$⊢ x \in A \to \{x\} \in (𝒫 A \cap Fin)$
5		sneqbg	$⊢ x \in A \to (\{x\} = \{y\} \leftrightarrow x = y)$
6	5	adantr	$⊢ (x \in A \land y \in A) \to (\{x\} = \{y\} \leftrightarrow x = y)$
7	4 6	dom2	$⊢ 𝒫 A \cap Fin \in V \to A ≼ (𝒫 A \cap Fin)$