Metamath Proof Explorer


Theorem ackbij1lem4

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

Ref Expression
Assertion ackbij1lem4 AωA𝒫ωFin

Proof

Step Hyp Ref Expression
1 snelpwi AωA𝒫ω
2 snfi AFin
3 2 a1i AωAFin
4 1 3 elind AωA𝒫ωFin