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	|- ( ( ~P A i^i Fin ) e. _V -> A ~<_ ( ~P A i^i Fin ) )

Proof

Step	Hyp	Ref	Expression
1		snelpwi	|- ( x e. A -> { x } e. ~P A )
2		snfi	|- { x } e. Fin
3	2	a1i	|- ( x e. A -> { x } e. Fin )
4	1 3	elind	|- ( x e. A -> { x } e. ( ~P A i^i Fin ) )
5		sneqbg	|- ( x e. A -> ( { x } = { y } <-> x = y ) )
6	5	adantr	|- ( ( x e. A /\ y e. A ) -> ( { x } = { y } <-> x = y ) )
7	4 6	dom2	|- ( ( ~P A i^i Fin ) e. _V -> A ~<_ ( ~P A i^i Fin ) )