ackbij1lem11

		Ref	Expression
	Hypothesis	ackbij.f	$⊢ F = (x \in (𝒫 ω \cap Fin) ⟼ card (⋃_{y \in x} (\{y\} \times 𝒫 y)))$
	Assertion	ackbij1lem11	$⊢ (A \in (𝒫 ω \cap Fin) \land B \subseteq A) \to B \in (𝒫 ω \cap Fin)$

Step	Hyp	Ref	Expression
1		ackbij.f	$⊢ F = (x \in (𝒫 ω \cap Fin) ⟼ card (⋃_{y \in x} (\{y\} \times 𝒫 y)))$
2		ssexg	$⊢ (B \subseteq A \land A \in (𝒫 ω \cap Fin)) \to B \in V$
3		elinel1	$⊢ A \in (𝒫 ω \cap Fin) \to A \in 𝒫 ω$
4	3	elpwid	$⊢ A \in (𝒫 ω \cap Fin) \to A \subseteq ω$
5		sstr	$⊢ (B \subseteq A \land A \subseteq ω) \to B \subseteq ω$
6	4 5	sylan2	$⊢ (B \subseteq A \land A \in (𝒫 ω \cap Fin)) \to B \subseteq ω$
7	2 6	elpwd	$⊢ (B \subseteq A \land A \in (𝒫 ω \cap Fin)) \to B \in 𝒫 ω$
8	7	ancoms	$⊢ (A \in (𝒫 ω \cap Fin) \land B \subseteq A) \to B \in 𝒫 ω$
9		elinel2	$⊢ A \in (𝒫 ω \cap Fin) \to A \in Fin$
10		ssfi	$⊢ (A \in Fin \land B \subseteq A) \to B \in Fin$
11	9 10	sylan	$⊢ (A \in (𝒫 ω \cap Fin) \land B \subseteq A) \to B \in Fin$
12	8 11	elind	$⊢ (A \in (𝒫 ω \cap Fin) \land B \subseteq A) \to B \in (𝒫 ω \cap Fin)$

Metamath Proof Explorer