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 \| \forall a \in ({𝒫 g}^{ω}) (\forall b \in ω a (suc b) \subseteq a (b) \to ⋂ ran a \in ran a)\}$
	Assertion	ssfin3ds	$⊢ (A \in F \land B \subseteq A) \to B \in F$

Proof

Step	Hyp	Ref	Expression
1		isfin3ds.f	$⊢ F = \{g \| \forall a \in ({𝒫 g}^{ω}) (\forall b \in ω a (suc b) \subseteq a (b) \to ⋂ ran a \in ran a)\}$
2		pwexg	$⊢ A \in F \to 𝒫 A \in V$
3		simpr	$⊢ (A \in F \land B \subseteq A) \to B \subseteq A$
4	3	sspwd	$⊢ (A \in F \land B \subseteq A) \to 𝒫 B \subseteq 𝒫 A$
5		mapss	$⊢ (𝒫 A \in V \land 𝒫 B \subseteq 𝒫 A) \to {𝒫 B}^{ω} \subseteq {𝒫 A}^{ω}$
6	2 4 5	syl2an2r	$⊢ (A \in F \land B \subseteq A) \to {𝒫 B}^{ω} \subseteq {𝒫 A}^{ω}$
7	1	isfin3ds	$⊢ A \in F \to (A \in F \leftrightarrow \forall f \in ({𝒫 A}^{ω}) (\forall x \in ω f (suc x) \subseteq f (x) \to ⋂ ran f \in ran f))$
8	7	ibi	$⊢ A \in F \to \forall f \in ({𝒫 A}^{ω}) (\forall x \in ω f (suc x) \subseteq f (x) \to ⋂ ran f \in ran f)$
9	8	adantr	$⊢ (A \in F \land B \subseteq A) \to \forall f \in ({𝒫 A}^{ω}) (\forall x \in ω f (suc x) \subseteq f (x) \to ⋂ ran f \in ran f)$
10		ssralv	$⊢ {𝒫 B}^{ω} \subseteq {𝒫 A}^{ω} \to (\forall f \in ({𝒫 A}^{ω}) (\forall x \in ω f (suc x) \subseteq f (x) \to ⋂ ran f \in ran f) \to \forall f \in ({𝒫 B}^{ω}) (\forall x \in ω f (suc x) \subseteq f (x) \to ⋂ ran f \in ran f))$
11	6 9 10	sylc	$⊢ (A \in F \land B \subseteq A) \to \forall f \in ({𝒫 B}^{ω}) (\forall x \in ω f (suc x) \subseteq f (x) \to ⋂ ran f \in ran f)$
12		ssexg	$⊢ (B \subseteq A \land A \in F) \to B \in V$
13	12	ancoms	$⊢ (A \in F \land B \subseteq A) \to B \in V$
14	1	isfin3ds	$⊢ B \in V \to (B \in F \leftrightarrow \forall f \in ({𝒫 B}^{ω}) (\forall x \in ω f (suc x) \subseteq f (x) \to ⋂ ran f \in ran f))$
15	13 14	syl	$⊢ (A \in F \land B \subseteq A) \to (B \in F \leftrightarrow \forall f \in ({𝒫 B}^{ω}) (\forall x \in ω f (suc x) \subseteq f (x) \to ⋂ ran f \in ran f))$
16	11 15	mpbird	$⊢ (A \in F \land B \subseteq A) \to B \in F$