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

Metamath Proof Explorer

Theorem ssfin2

Description: A subset of a II-finite set is II-finite. (Contributed by Stefan O'Rear, 2-Nov-2014) (Revised by Mario Carneiro, 16-May-2015)

Ref Expression
Assertion ssfin2 ⊢ A ∈ FinII ∧ B ⊆ A → B ∈ FinII

Proof

Step Hyp Ref Expression
1 simpll ⊢ A ∈ FinII ∧ B ⊆ A ∧ x ∈ 𝒫 𝒫 B → A ∈ FinII
2 elpwi ⊢ x ∈ 𝒫 𝒫 B → x ⊆ 𝒫 B
3 2 adantl ⊢ A ∈ FinII ∧ B ⊆ A ∧ x ∈ 𝒫 𝒫 B → x ⊆ 𝒫 B
4 simplr ⊢ A ∈ FinII ∧ B ⊆ A ∧ x ∈ 𝒫 𝒫 B → B ⊆ A
5 4 sspwd ⊢ A ∈ FinII ∧ B ⊆ A ∧ x ∈ 𝒫 𝒫 B → 𝒫 B ⊆ 𝒫 A
6 3 5 sstrd ⊢ A ∈ FinII ∧ B ⊆ A ∧ x ∈ 𝒫 𝒫 B → x ⊆ 𝒫 A
7 fin2i ⊢ A ∈ FinII ∧ x ⊆ 𝒫 A ∧ x ≠ ∅ ∧ [⊂] Or x → ⋃ x ∈ x
8 7 ex ⊢ A ∈ FinII ∧ x ⊆ 𝒫 A → x ≠ ∅ ∧ [⊂] Or x → ⋃ x ∈ x
9 1 6 8 syl2anc ⊢ A ∈ FinII ∧ B ⊆ A ∧ x ∈ 𝒫 𝒫 B → x ≠ ∅ ∧ [⊂] Or x → ⋃ x ∈ x
10 9 ralrimiva ⊢ A ∈ FinII ∧ B ⊆ A → ∀ x ∈ 𝒫 𝒫 B x ≠ ∅ ∧ [⊂] Or x → ⋃ x ∈ x
11 ssexg ⊢ B ⊆ A ∧ A ∈ FinII → B ∈ V
12 11 ancoms ⊢ A ∈ FinII ∧ B ⊆ A → B ∈ V
13 isfin2 ⊢ B ∈ V → B ∈ FinII ↔ ∀ x ∈ 𝒫 𝒫 B x ≠ ∅ ∧ [⊂] Or x → ⋃ x ∈ x
14 12 13 syl ⊢ A ∈ FinII ∧ B ⊆ A → B ∈ FinII ↔ ∀ x ∈ 𝒫 𝒫 B x ≠ ∅ ∧ [⊂] Or x → ⋃ x ∈ x
15 10 14 mpbird ⊢ A ∈ FinII ∧ B ⊆ A → B ∈ FinII