Definition df-fin7 9978

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 9971	. 2 class FinVII
2		vx	. . . . . . 7 setvar 𝑥
3	2	cv 1538	. . . . . 6 class 𝑥
4		vy	. . . . . . 7 setvar 𝑦
5	4	cv 1538	. . . . . 6 class 𝑦
6		cen 8688	. . . . . 6 class ≈
7	3, 5, 6	wbr 5070	. . . . 5 wff 𝑥 ≈ 𝑦
8		con0 6251	. . . . . 6 class On
9		com 7687	. . . . . 6 class ω
10	8, 9	cdif 3880	. . . . 5 class (On ∖ ω)
11	7, 4, 10	wrex 3064	. . . 4 wff ∃𝑦 ∈ (On ∖ ω)𝑥 ≈ 𝑦
12	11	wn 3	. . 3 wff ¬ ∃𝑦 ∈ (On ∖ ω)𝑥 ≈ 𝑦
13	12, 2	cab 2715	. 2 class {𝑥 ∣ ¬ ∃𝑦 ∈ (On ∖ ω)𝑥 ≈ 𝑦}
14	1, 13	wceq 1539	1 wff FinVII = {𝑥 ∣ ¬ ∃𝑦 ∈ (On ∖ ω)𝑥 ≈ 𝑦}

This definition is referenced by:  isfin7  9988