This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) )