Definition df-fin7

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)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfin7	⊢ FinVII
1		vx	⊢ 𝑥
2		vy	⊢ 𝑦
3		con0	⊢ On
4		com	⊢ ω
5	3 4	cdif	⊢ ( On ∖ ω )
6	1	cv	⊢ 𝑥
7		cen	⊢ ≈
8	2	cv	⊢ 𝑦
9	6 8 7	wbr	⊢ 𝑥 ≈ 𝑦
10	9 2 5	wrex	⊢ ∃ 𝑦 ∈ ( On ∖ ω ) 𝑥 ≈ 𝑦
11	10	wn	⊢ ¬ ∃ 𝑦 ∈ ( On ∖ ω ) 𝑥 ≈ 𝑦
12	11 1	cab	⊢ { 𝑥 ∣ ¬ ∃ 𝑦 ∈ ( On ∖ ω ) 𝑥 ≈ 𝑦 }
13	0 12	wceq	⊢ FinVII = { 𝑥 ∣ ¬ ∃ 𝑦 ∈ ( On ∖ ω ) 𝑥 ≈ 𝑦 }