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

Metamath Proof Explorer

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