ackbij1lem6

		Ref	Expression
	Assertion	ackbij1lem6	$⊢ (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \to A \cup B \in (𝒫 ω \cap Fin)$

Step	Hyp	Ref	Expression
1		elinel2	$⊢ A \in (𝒫 ω \cap Fin) \to A \in Fin$
2		elinel2	$⊢ B \in (𝒫 ω \cap Fin) \to B \in Fin$
3		unfi	$⊢ (A \in Fin \land B \in Fin) \to A \cup B \in Fin$
4	1 2 3	syl2an	$⊢ (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \to A \cup B \in Fin$
5		elinel1	$⊢ A \in (𝒫 ω \cap Fin) \to A \in 𝒫 ω$
6		elinel1	$⊢ B \in (𝒫 ω \cap Fin) \to B \in 𝒫 ω$
7		elpwi	$⊢ A \in 𝒫 ω \to A \subseteq ω$
8		elpwi	$⊢ B \in 𝒫 ω \to B \subseteq ω$
9		simpl	$⊢ (A \subseteq ω \land B \subseteq ω) \to A \subseteq ω$
10		simpr	$⊢ (A \subseteq ω \land B \subseteq ω) \to B \subseteq ω$
11	9 10	unssd	$⊢ (A \subseteq ω \land B \subseteq ω) \to A \cup B \subseteq ω$
12	7 8 11	syl2an	$⊢ (A \in 𝒫 ω \land B \in 𝒫 ω) \to A \cup B \subseteq ω$
13	5 6 12	syl2an	$⊢ (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \to A \cup B \subseteq ω$
14	4 13	elpwd	$⊢ (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \to A \cup B \in 𝒫 ω$
15	14 4	elind	$⊢ (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \to A \cup B \in (𝒫 ω \cap Fin)$

Metamath Proof Explorer