ackbij1lem3

		Ref	Expression
	Assertion	ackbij1lem3	$⊢ A \in ω \to A \in (𝒫 ω \cap Fin)$

Step	Hyp	Ref	Expression
1		ordom	$⊢ Ord ω$
2		ordelss	$⊢ (Ord ω \land A \in ω) \to A \subseteq ω$
3	1 2	mpan	$⊢ A \in ω \to A \subseteq ω$
4		elpwg	$⊢ A \in ω \to (A \in 𝒫 ω \leftrightarrow A \subseteq ω)$
5	3 4	mpbird	$⊢ A \in ω \to A \in 𝒫 ω$
6		nnfi	$⊢ A \in ω \to A \in Fin$
7	5 6	elind	$⊢ A \in ω \to A \in (𝒫 ω \cap Fin)$

Metamath Proof Explorer