Definition df-fin2

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)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfin2	⊢ FinII
1		vx	⊢ 𝑥
2		vy	⊢ 𝑦
3	1	cv	⊢ 𝑥
4	3	cpw	⊢ 𝒫 𝑥
5	4	cpw	⊢ 𝒫 𝒫 𝑥
6	2	cv	⊢ 𝑦
7		c0	⊢ ∅
8	6 7	wne	⊢ 𝑦 ≠ ∅
9		crpss	⊢ [⊊]
10	6 9	wor	⊢ [⊊] Or 𝑦
11	8 10	wa	⊢ ( 𝑦 ≠ ∅ ∧ [⊊] Or 𝑦 )
12	6	cuni	⊢ ∪ 𝑦
13	12 6	wcel	⊢ ∪ 𝑦 ∈ 𝑦
14	11 13	wi	⊢ ( ( 𝑦 ≠ ∅ ∧ [⊊] Or 𝑦 ) → ∪ 𝑦 ∈ 𝑦 )
15	14 2 5	wral	⊢ ∀ 𝑦 ∈ 𝒫 𝒫 𝑥 ( ( 𝑦 ≠ ∅ ∧ [⊊] Or 𝑦 ) → ∪ 𝑦 ∈ 𝑦 )
16	15 1	cab	⊢ { 𝑥 ∣ ∀ 𝑦 ∈ 𝒫 𝒫 𝑥 ( ( 𝑦 ≠ ∅ ∧ [⊊] Or 𝑦 ) → ∪ 𝑦 ∈ 𝑦 ) }
17	0 16	wceq	⊢ FinII = { 𝑥 ∣ ∀ 𝑦 ∈ 𝒫 𝒫 𝑥 ( ( 𝑦 ≠ ∅ ∧ [⊊] Or 𝑦 ) → ∪ 𝑦 ∈ 𝑦 ) }