ackbij2lem1

		Ref	Expression
	Assertion	ackbij2lem1	$⊢ A \in ω \to 𝒫 A \subseteq 𝒫 ω \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	3	sspwd	$⊢ A \in ω \to 𝒫 A \subseteq 𝒫 ω$
5	4	sselda	$⊢ (A \in ω \land a \in 𝒫 A) \to a \in 𝒫 ω$
6		nnfi	$⊢ A \in ω \to A \in Fin$
7		elpwi	$⊢ a \in 𝒫 A \to a \subseteq A$
8		ssfi	$⊢ (A \in Fin \land a \subseteq A) \to a \in Fin$
9	6 7 8	syl2an	$⊢ (A \in ω \land a \in 𝒫 A) \to a \in Fin$
10	5 9	elind	$⊢ (A \in ω \land a \in 𝒫 A) \to a \in (𝒫 ω \cap Fin)$
11	10	ex	$⊢ A \in ω \to (a \in 𝒫 A \to a \in (𝒫 ω \cap Fin))$
12	11	ssrdv	$⊢ A \in ω \to 𝒫 A \subseteq 𝒫 ω \cap Fin$

Metamath Proof Explorer