Metamath Proof Explorer

Theorem ackbij1lem6

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

Ref Expression
Assertion ackbij1lem6 ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) → ( 𝐴 ∪ 𝐵 ) ∈ ( 𝒫 ω ∩ Fin ) )

Proof

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