isfin3ds

Description: Property of a III-finite set (descending sequence version). (Contributed by Mario Carneiro, 16-May-2015)

		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	isfin3ds	$⊢ A \in V \to (A \in F \leftrightarrow \forall f \in ({𝒫 A}^{ω}) (\forall x \in ω f (suc x) \subseteq f (x) \to ⋂ ran f \in ran 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		suceq	$⊢ b = x \to suc b = suc x$
3	2	fveq2d	$⊢ b = x \to a (suc b) = a (suc x)$
4		fveq2	$⊢ b = x \to a (b) = a (x)$
5	3 4	sseq12d	$⊢ b = x \to (a (suc b) \subseteq a (b) \leftrightarrow a (suc x) \subseteq a (x))$
6	5	cbvralvw	$⊢ \forall b \in ω a (suc b) \subseteq a (b) \leftrightarrow \forall x \in ω a (suc x) \subseteq a (x)$
7		fveq1	$⊢ a = f \to a (suc x) = f (suc x)$
8		fveq1	$⊢ a = f \to a (x) = f (x)$
9	7 8	sseq12d	$⊢ a = f \to (a (suc x) \subseteq a (x) \leftrightarrow f (suc x) \subseteq f (x))$
10	9	ralbidv	$⊢ a = f \to (\forall x \in ω a (suc x) \subseteq a (x) \leftrightarrow \forall x \in ω f (suc x) \subseteq f (x))$
11	6 10	syl5bb	$⊢ a = f \to (\forall b \in ω a (suc b) \subseteq a (b) \leftrightarrow \forall x \in ω f (suc x) \subseteq f (x))$
12		rneq	$⊢ a = f \to ran a = ran f$
13	12	inteqd	$⊢ a = f \to ⋂ ran a = ⋂ ran f$
14	13 12	eleq12d	$⊢ a = f \to (⋂ ran a \in ran a \leftrightarrow ⋂ ran f \in ran f)$
15	11 14	imbi12d	$⊢ a = f \to ((\forall b \in ω a (suc b) \subseteq a (b) \to ⋂ ran a \in ran a) \leftrightarrow (\forall x \in ω f (suc x) \subseteq f (x) \to ⋂ ran f \in ran f))$
16	15	cbvralvw	$⊢ \forall a \in ({𝒫 g}^{ω}) (\forall b \in ω a (suc b) \subseteq a (b) \to ⋂ ran a \in ran a) \leftrightarrow \forall f \in ({𝒫 g}^{ω}) (\forall x \in ω f (suc x) \subseteq f (x) \to ⋂ ran f \in ran f)$
17		pweq	$⊢ g = A \to 𝒫 g = 𝒫 A$
18	17	oveq1d	$⊢ g = A \to {𝒫 g}^{ω} = {𝒫 A}^{ω}$
19	18	raleqdv	$⊢ g = A \to (\forall f \in ({𝒫 g}^{ω}) (\forall x \in ω f (suc x) \subseteq f (x) \to ⋂ ran f \in ran f) \leftrightarrow \forall f \in ({𝒫 A}^{ω}) (\forall x \in ω f (suc x) \subseteq f (x) \to ⋂ ran f \in ran f))$
20	16 19	syl5bb	$⊢ g = A \to (\forall a \in ({𝒫 g}^{ω}) (\forall b \in ω a (suc b) \subseteq a (b) \to ⋂ ran a \in ran a) \leftrightarrow \forall f \in ({𝒫 A}^{ω}) (\forall x \in ω f (suc x) \subseteq f (x) \to ⋂ ran f \in ran f))$
21	20 1	elab2g	$⊢ A \in V \to (A \in F \leftrightarrow \forall f \in ({𝒫 A}^{ω}) (\forall x \in ω f (suc x) \subseteq f (x) \to ⋂ ran f \in ran f))$

Metamath Proof Explorer

Theorem isfin3ds

Proof