This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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