Theorem ackbij1lem11

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

	Ref	Expression
Hypothesis	ackbij.f	⊢ 𝐹 = ( 𝑥 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑦 ∈ 𝑥 ( { 𝑦 } × 𝒫 𝑦 ) ) )
Assertion	ackbij1lem11	⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ⊆ 𝐴 ) → 𝐵 ∈ ( 𝒫 ω ∩ Fin ) )

Proof

Step	Hyp	Ref	Expression
1		ackbij.f	⊢ 𝐹 = ( 𝑥 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑦 ∈ 𝑥 ( { 𝑦 } × 𝒫 𝑦 ) ) )
2		ssexg	⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ) → 𝐵 ∈ V )
3		elinel1	⊢ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) → 𝐴 ∈ 𝒫 ω )
4	3	elpwid	⊢ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) → 𝐴 ⊆ ω )
5		sstr	⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ ω ) → 𝐵 ⊆ ω )
6	4 5	sylan2	⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ) → 𝐵 ⊆ ω )
7	2 6	elpwd	⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ) → 𝐵 ∈ 𝒫 ω )
8	7	ancoms	⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ⊆ 𝐴 ) → 𝐵 ∈ 𝒫 ω )
9		elinel2	⊢ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) → 𝐴 ∈ Fin )
10		ssfi	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴 ) → 𝐵 ∈ Fin )
11	9 10	sylan	⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ⊆ 𝐴 ) → 𝐵 ∈ Fin )
12	8 11	elind	⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ⊆ 𝐴 ) → 𝐵 ∈ ( 𝒫 ω ∩ Fin ) )