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 𝒫AFinVA𝒫AFin

Proof

Step Hyp Ref Expression
1 snelpwi xAx𝒫A
2 snfi xFin
3 2 a1i xAxFin
4 1 3 elind xAx𝒫AFin
5 sneqbg xAx=yx=y
6 5 adantr xAyAx=yx=y
7 4 6 dom2 𝒫AFinVA𝒫AFin