Metamath Proof Explorer


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 ∖ ω ) 𝑥𝑦 }