Description: Lemma for ackbij2 . (Contributed by Stefan O'Rear, 19-Nov-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | ackbij1lem4 | ⊢ ( 𝐴 ∈ ω → { 𝐴 } ∈ ( 𝒫 ω ∩ Fin ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | snelpwi | ⊢ ( 𝐴 ∈ ω → { 𝐴 } ∈ 𝒫 ω ) | |
2 | snfi | ⊢ { 𝐴 } ∈ Fin | |
3 | 2 | a1i | ⊢ ( 𝐴 ∈ ω → { 𝐴 } ∈ Fin ) |
4 | 1 3 | elind | ⊢ ( 𝐴 ∈ ω → { 𝐴 } ∈ ( 𝒫 ω ∩ Fin ) ) |