Definition df-fin7 9707

Description: A set is VII-finite iff it cannot be infinitely well-ordered. Equivalent to definition VII of [Levy58] p. 4. (Contributed by Stefan O'Rear, 12-Nov-2014.)

Assertion

Ref	Expression
df-fin7	⊢ FinVII = {𝑥 ∣ ¬ ∃𝑦 ∈ (On ∖ ω)𝑥 ≈ 𝑦}

Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-fin7

Step	Hyp	Ref	Expression
1		cfin7 9700	. 2 class FinVII
2		vx	. . . . . . 7 setvar 𝑥
3	2	cv 1532	. . . . . 6 class 𝑥
4		vy	. . . . . . 7 setvar 𝑦
5	4	cv 1532	. . . . . 6 class 𝑦
6		cen 8500	. . . . . 6 class ≈
7	3, 5, 6	wbr 5058	. . . . 5 wff 𝑥 ≈ 𝑦
8		con0 6185	. . . . . 6 class On
9		com 7574	. . . . . 6 class ω
10	8, 9	cdif 3932	. . . . 5 class (On ∖ ω)
11	7, 4, 10	wrex 3139	. . . 4 wff ∃𝑦 ∈ (On ∖ ω)𝑥 ≈ 𝑦
12	11	wn 3	. . 3 wff ¬ ∃𝑦 ∈ (On ∖ ω)𝑥 ≈ 𝑦
13	12, 2	cab 2799	. 2 class {𝑥 ∣ ¬ ∃𝑦 ∈ (On ∖ ω)𝑥 ≈ 𝑦}
14	1, 13	wceq 1533	1 wff FinVII = {𝑥 ∣ ¬ ∃𝑦 ∈ (On ∖ ω)𝑥 ≈ 𝑦}

This definition is referenced by:  isfin7  9717