Definition df-fin2 10305

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 10298	. 2 class FinII
2		vy	. . . . . . . 8 setvar 𝑦
3	2	cv 1539	. . . . . . 7 class 𝑦
4		c0 4313	. . . . . . 7 class ∅
5	3, 4	wne 2933	. . . . . 6 wff 𝑦 ≠ ∅
6		crpss 7721	. . . . . . 7 class [⊊]
7	3, 6	wor 5565	. . . . . 6 wff [⊊] Or 𝑦
8	5, 7	wa 395	. . . . 5 wff (𝑦 ≠ ∅ ∧ [⊊] Or 𝑦)
9	3	cuni 4888	. . . . . 6 class ∪ 𝑦
10	9, 3	wcel 2109	. . . . 5 wff ∪ 𝑦 ∈ 𝑦
11	8, 10	wi 4	. . . 4 wff ((𝑦 ≠ ∅ ∧ [⊊] Or 𝑦) → ∪ 𝑦 ∈ 𝑦)
12		vx	. . . . . . 7 setvar 𝑥
13	12	cv 1539	. . . . . 6 class 𝑥
14	13	cpw 4580	. . . . 5 class 𝒫 𝑥
15	14	cpw 4580	. . . 4 class 𝒫 𝒫 𝑥
16	11, 2, 15	wral 3052	. . 3 wff ∀𝑦 ∈ 𝒫 𝒫 𝑥((𝑦 ≠ ∅ ∧ [⊊] Or 𝑦) → ∪ 𝑦 ∈ 𝑦)
17	16, 12	cab 2714	. 2 class {𝑥 ∣ ∀𝑦 ∈ 𝒫 𝒫 𝑥((𝑦 ≠ ∅ ∧ [⊊] Or 𝑦) → ∪ 𝑦 ∈ 𝑦)}
18	1, 17	wceq 1540	1 wff FinII = {𝑥 ∣ ∀𝑦 ∈ 𝒫 𝒫 𝑥((𝑦 ≠ ∅ ∧ [⊊] Or 𝑦) → ∪ 𝑦 ∈ 𝑦)}

This definition is referenced by:  isfin2  10313