Definition df-fin2 9710

Description: A set is II-finite (Tarski finite) iff every nonempty chain of subsets contains a maximum element. Definition II of [Levy58] p. 2. (Contributed by Stefan O'Rear, 12-Nov-2014.)

Assertion

Ref	Expression
df-fin2	⊢ FinII = {𝑥 ∣ ∀𝑦 ∈ 𝒫 𝒫 𝑥((𝑦 ≠ ∅ ∧ [⊊] Or 𝑦) → ∪ 𝑦 ∈ 𝑦)}

Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-fin2

Step	Hyp	Ref	Expression
1		cfin2 9703	. 2 class FinII
2		vy	. . . . . . . 8 setvar 𝑦
3	2	cv 1536	. . . . . . 7 class 𝑦
4		c0 4293	. . . . . . 7 class ∅
5	3, 4	wne 3018	. . . . . 6 wff 𝑦 ≠ ∅
6		crpss 7450	. . . . . . 7 class [⊊]
7	3, 6	wor 5475	. . . . . 6 wff [⊊] Or 𝑦
8	5, 7	wa 398	. . . . 5 wff (𝑦 ≠ ∅ ∧ [⊊] Or 𝑦)
9	3	cuni 4840	. . . . . 6 class ∪ 𝑦
10	9, 3	wcel 2114	. . . . 5 wff ∪ 𝑦 ∈ 𝑦
11	8, 10	wi 4	. . . 4 wff ((𝑦 ≠ ∅ ∧ [⊊] Or 𝑦) → ∪ 𝑦 ∈ 𝑦)
12		vx	. . . . . . 7 setvar 𝑥
13	12	cv 1536	. . . . . 6 class 𝑥
14	13	cpw 4541	. . . . 5 class 𝒫 𝑥
15	14	cpw 4541	. . . 4 class 𝒫 𝒫 𝑥
16	11, 2, 15	wral 3140	. . 3 wff ∀𝑦 ∈ 𝒫 𝒫 𝑥((𝑦 ≠ ∅ ∧ [⊊] Or 𝑦) → ∪ 𝑦 ∈ 𝑦)
17	16, 12	cab 2801	. 2 class {𝑥 ∣ ∀𝑦 ∈ 𝒫 𝒫 𝑥((𝑦 ≠ ∅ ∧ [⊊] Or 𝑦) → ∪ 𝑦 ∈ 𝑦)}
18	1, 17	wceq 1537	1 wff FinII = {𝑥 ∣ ∀𝑦 ∈ 𝒫 𝒫 𝑥((𝑦 ≠ ∅ ∧ [⊊] Or 𝑦) → ∪ 𝑦 ∈ 𝑦)}

This definition is referenced by:  isfin2  9718