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