Theorem ackbij1lem4

Description: Lemma for ackbij2 . (Contributed by Stefan O'Rear, 19-Nov-2014)

	Ref	Expression
Assertion	ackbij1lem4	|- ( A e. _om -> { A } e. ( ~P _om i^i Fin ) )

Proof

Step	Hyp	Ref	Expression
1		snelpwi	|- ( A e. _om -> { A } e. ~P _om )
2		snfi	|- { A } e. Fin
3	2	a1i	|- ( A e. _om -> { A } e. Fin )
4	1 3	elind	|- ( A e. _om -> { A } e. ( ~P _om i^i Fin ) )