Metamath Proof Explorer

Definition df-fin3

Description: A set is III-finite (weakly Dedekind finite) iff its power set is Dedekind finite. Definition III of Levy58 p. 2. (Contributed by Stefan O'Rear, 12-Nov-2014)

		Ref	Expression
	Assertion	df-fin3	⊢ Fin^III = { 𝑥 ∣ 𝒫 𝑥 ∈ Fin^IV }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfin3	⊢ Fin^III
1		vx	⊢ 𝑥
2	1	cv	⊢ 𝑥
3	2	cpw	⊢ 𝒫 𝑥
4		cfin4	⊢ Fin^IV
5	3 4	wcel	⊢ 𝒫 𝑥 ∈ Fin^IV
6	5 1	cab	⊢ { 𝑥 ∣ 𝒫 𝑥 ∈ Fin^IV }
7	0 6	wceq	⊢ Fin^III = { 𝑥 ∣ 𝒫 𝑥 ∈ Fin^IV }