Metamath Proof Explorer


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 ) )