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