Metamath Proof Explorer

Theorem ackbij1lem6

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

Ref Expression
Assertion ackbij1lem6 ⊢ A ∈ 𝒫 ω ∩ Fin ∧ B ∈ 𝒫 ω ∩ Fin → A ∪ B ∈ 𝒫 ω ∩ Fin

Proof

Step Hyp Ref Expression
1 elinel2 ⊢ A ∈ 𝒫 ω ∩ Fin → A ∈ Fin
2 elinel2 ⊢ B ∈ 𝒫 ω ∩ Fin → B ∈ Fin
3 unfi ⊢ A ∈ Fin ∧ B ∈ Fin → A ∪ B ∈ Fin
4 1 2 3 syl2an ⊢ A ∈ 𝒫 ω ∩ Fin ∧ B ∈ 𝒫 ω ∩ Fin → A ∪ B ∈ Fin
5 elinel1 ⊢ A ∈ 𝒫 ω ∩ Fin → A ∈ 𝒫 ω
6 elinel1 ⊢ B ∈ 𝒫 ω ∩ Fin → B ∈ 𝒫 ω
7 elpwi ⊢ A ∈ 𝒫 ω → A ⊆ ω
8 elpwi ⊢ B ∈ 𝒫 ω → B ⊆ ω
9 simpl ⊢ A ⊆ ω ∧ B ⊆ ω → A ⊆ ω
10 simpr ⊢ A ⊆ ω ∧ B ⊆ ω → B ⊆ ω
11 9 10 unssd ⊢ A ⊆ ω ∧ B ⊆ ω → A ∪ B ⊆ ω
12 7 8 11 syl2an ⊢ A ∈ 𝒫 ω ∧ B ∈ 𝒫 ω → A ∪ B ⊆ ω
13 5 6 12 syl2an ⊢ A ∈ 𝒫 ω ∩ Fin ∧ B ∈ 𝒫 ω ∩ Fin → A ∪ B ⊆ ω
14 4 13 elpwd ⊢ A ∈ 𝒫 ω ∩ Fin ∧ B ∈ 𝒫 ω ∩ Fin → A ∪ B ∈ 𝒫 ω
15 14 4 elind ⊢ A ∈ 𝒫 ω ∩ Fin ∧ B ∈ 𝒫 ω ∩ Fin → A ∪ B ∈ 𝒫 ω ∩ Fin