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

Metamath Proof Explorer

Theorem ssfin3ds

Description: A subset of a III-finite set is III-finite. (Contributed by Stefan O'Rear, 4-Nov-2014)

Ref Expression
Hypothesis isfin3ds.f ⊢ F = g | ∀ a ∈ 𝒫 g ω ∀ b ∈ ω a ⁡ suc ⁡ b ⊆ a ⁡ b → ⋂ ran ⁡ a ∈ ran ⁡ a
Assertion ssfin3ds ⊢ A ∈ F ∧ B ⊆ A → B ∈ F

Proof

Step Hyp Ref Expression
1 isfin3ds.f ⊢ F = g | ∀ a ∈ 𝒫 g ω ∀ b ∈ ω a ⁡ suc ⁡ b ⊆ a ⁡ b → ⋂ ran ⁡ a ∈ ran ⁡ a
2 pwexg ⊢ A ∈ F → 𝒫 A ∈ V
3 simpr ⊢ A ∈ F ∧ B ⊆ A → B ⊆ A
4 3 sspwd ⊢ A ∈ F ∧ B ⊆ A → 𝒫 B ⊆ 𝒫 A
5 mapss ⊢ 𝒫 A ∈ V ∧ 𝒫 B ⊆ 𝒫 A → 𝒫 B ω ⊆ 𝒫 A ω
6 2 4 5 syl2an2r ⊢ A ∈ F ∧ B ⊆ A → 𝒫 B ω ⊆ 𝒫 A ω
7 1 isfin3ds ⊢ A ∈ F → A ∈ F ↔ ∀ f ∈ 𝒫 A ω ∀ x ∈ ω f ⁡ suc ⁡ x ⊆ f ⁡ x → ⋂ ran ⁡ f ∈ ran ⁡ f
8 7 ibi ⊢ A ∈ F → ∀ f ∈ 𝒫 A ω ∀ x ∈ ω f ⁡ suc ⁡ x ⊆ f ⁡ x → ⋂ ran ⁡ f ∈ ran ⁡ f
9 8 adantr ⊢ A ∈ F ∧ B ⊆ A → ∀ f ∈ 𝒫 A ω ∀ x ∈ ω f ⁡ suc ⁡ x ⊆ f ⁡ x → ⋂ ran ⁡ f ∈ ran ⁡ f
10 ssralv ⊢ 𝒫 B ω ⊆ 𝒫 A ω → ∀ f ∈ 𝒫 A ω ∀ x ∈ ω f ⁡ suc ⁡ x ⊆ f ⁡ x → ⋂ ran ⁡ f ∈ ran ⁡ f → ∀ f ∈ 𝒫 B ω ∀ x ∈ ω f ⁡ suc ⁡ x ⊆ f ⁡ x → ⋂ ran ⁡ f ∈ ran ⁡ f
11 6 9 10 sylc ⊢ A ∈ F ∧ B ⊆ A → ∀ f ∈ 𝒫 B ω ∀ x ∈ ω f ⁡ suc ⁡ x ⊆ f ⁡ x → ⋂ ran ⁡ f ∈ ran ⁡ f
12 ssexg ⊢ B ⊆ A ∧ A ∈ F → B ∈ V
13 12 ancoms ⊢ A ∈ F ∧ B ⊆ A → B ∈ V
14 1 isfin3ds ⊢ B ∈ V → B ∈ F ↔ ∀ f ∈ 𝒫 B ω ∀ x ∈ ω f ⁡ suc ⁡ x ⊆ f ⁡ x → ⋂ ran ⁡ f ∈ ran ⁡ f
15 13 14 syl ⊢ A ∈ F ∧ B ⊆ A → B ∈ F ↔ ∀ f ∈ 𝒫 B ω ∀ x ∈ ω f ⁡ suc ⁡ x ⊆ f ⁡ x → ⋂ ran ⁡ f ∈ ran ⁡ f
16 11 15 mpbird ⊢ A ∈ F ∧ B ⊆ A → B ∈ F