Theorem ackbij1lem3

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

	Ref	Expression
Assertion	ackbij1lem3	$$⊢A\in \mathrm{\omega }\to A\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)$$

Proof

Step	Hyp	Ref	Expression
1		ordom	$$⊢\mathrm{Ord}\mathrm{\omega }$$
2		ordelss	$$⊢\left(\mathrm{Ord}\mathrm{\omega }\wedge A\in \mathrm{\omega }\right)\to A\subseteq \mathrm{\omega }$$
3	1 2	mpan	$$⊢A\in \mathrm{\omega }\to A\subseteq \mathrm{\omega }$$
4		elpwg	$$⊢A\in \mathrm{\omega }\to \left(A\in 𝒫\mathrm{\omega }\leftrightarrow A\subseteq \mathrm{\omega }\right)$$
5	3 4	mpbird	$$⊢A\in \mathrm{\omega }\to A\in 𝒫\mathrm{\omega }$$
6		nnfi	$$⊢A\in \mathrm{\omega }\to A\in \mathrm{Fin}$$
7	5 6	elind	$$⊢A\in \mathrm{\omega }\to A\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)$$