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 \in {Fin}^{II} \land B \subseteq A) \to B \in {Fin}^{II}$

Proof

Step	Hyp	Ref	Expression
1		simpll	$⊢ ((A \in {Fin}^{II} \land B \subseteq A) \land x \in 𝒫 𝒫 B) \to A \in {Fin}^{II}$
2		elpwi	$⊢ x \in 𝒫 𝒫 B \to x \subseteq 𝒫 B$
3	2	adantl	$⊢ ((A \in {Fin}^{II} \land B \subseteq A) \land x \in 𝒫 𝒫 B) \to x \subseteq 𝒫 B$
4		simplr	$⊢ ((A \in {Fin}^{II} \land B \subseteq A) \land x \in 𝒫 𝒫 B) \to B \subseteq A$
5	4	sspwd	$⊢ ((A \in {Fin}^{II} \land B \subseteq A) \land x \in 𝒫 𝒫 B) \to 𝒫 B \subseteq 𝒫 A$
6	3 5	sstrd	$⊢ ((A \in {Fin}^{II} \land B \subseteq A) \land x \in 𝒫 𝒫 B) \to x \subseteq 𝒫 A$
7		fin2i	$⊢ ((A \in {Fin}^{II} \land x \subseteq 𝒫 A) \land (x \neq \emptyset \land [\subset] Or x)) \to ⋃ x \in x$
8	7	ex	$⊢ (A \in {Fin}^{II} \land x \subseteq 𝒫 A) \to ((x \neq \emptyset \land [\subset] Or x) \to ⋃ x \in x)$
9	1 6 8	syl2anc	$⊢ ((A \in {Fin}^{II} \land B \subseteq A) \land x \in 𝒫 𝒫 B) \to ((x \neq \emptyset \land [\subset] Or x) \to ⋃ x \in x)$
10	9	ralrimiva	$⊢ (A \in {Fin}^{II} \land B \subseteq A) \to \forall x \in 𝒫 𝒫 B ((x \neq \emptyset \land [\subset] Or x) \to ⋃ x \in x)$
11		ssexg	$⊢ (B \subseteq A \land A \in {Fin}^{II}) \to B \in V$
12	11	ancoms	$⊢ (A \in {Fin}^{II} \land B \subseteq A) \to B \in V$
13		isfin2	$⊢ B \in V \to (B \in {Fin}^{II} \leftrightarrow \forall x \in 𝒫 𝒫 B ((x \neq \emptyset \land [\subset] Or x) \to ⋃ x \in x))$
14	12 13	syl	$⊢ (A \in {Fin}^{II} \land B \subseteq A) \to (B \in {Fin}^{II} \leftrightarrow \forall x \in 𝒫 𝒫 B ((x \neq \emptyset \land [\subset] Or x) \to ⋃ x \in x))$
15	10 14	mpbird	$⊢ (A \in {Fin}^{II} \land B \subseteq A) \to B \in {Fin}^{II}$