Metamath Proof Explorer


Theorem ackbij1lem4

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

Ref Expression
Assertion ackbij1lem4 ( 𝐴 ∈ ω → { 𝐴 } ∈ ( 𝒫 ω ∩ Fin ) )

Proof

Step Hyp Ref Expression
1 snelpwi ( 𝐴 ∈ ω → { 𝐴 } ∈ 𝒫 ω )
2 snfi { 𝐴 } ∈ Fin
3 2 a1i ( 𝐴 ∈ ω → { 𝐴 } ∈ Fin )
4 1 3 elind ( 𝐴 ∈ ω → { 𝐴 } ∈ ( 𝒫 ω ∩ Fin ) )