Metamath Proof Explorer


Theorem ackbij2lem1

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

Ref Expression
Assertion ackbij2lem1 ( 𝐴 ∈ ω → 𝒫 𝐴 ⊆ ( 𝒫 ω ∩ Fin ) )

Proof

Step Hyp Ref Expression
1 ordom Ord ω
2 ordelss ( ( Ord ω ∧ 𝐴 ∈ ω ) → 𝐴 ⊆ ω )
3 1 2 mpan ( 𝐴 ∈ ω → 𝐴 ⊆ ω )
4 3 sspwd ( 𝐴 ∈ ω → 𝒫 𝐴 ⊆ 𝒫 ω )
5 4 sselda ( ( 𝐴 ∈ ω ∧ 𝑎 ∈ 𝒫 𝐴 ) → 𝑎 ∈ 𝒫 ω )
6 nnfi ( 𝐴 ∈ ω → 𝐴 ∈ Fin )
7 elpwi ( 𝑎 ∈ 𝒫 𝐴𝑎𝐴 )
8 ssfi ( ( 𝐴 ∈ Fin ∧ 𝑎𝐴 ) → 𝑎 ∈ Fin )
9 6 7 8 syl2an ( ( 𝐴 ∈ ω ∧ 𝑎 ∈ 𝒫 𝐴 ) → 𝑎 ∈ Fin )
10 5 9 elind ( ( 𝐴 ∈ ω ∧ 𝑎 ∈ 𝒫 𝐴 ) → 𝑎 ∈ ( 𝒫 ω ∩ Fin ) )
11 10 ex ( 𝐴 ∈ ω → ( 𝑎 ∈ 𝒫 𝐴𝑎 ∈ ( 𝒫 ω ∩ Fin ) ) )
12 11 ssrdv ( 𝐴 ∈ ω → 𝒫 𝐴 ⊆ ( 𝒫 ω ∩ Fin ) )