Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-fin7 | Structured version Visualization version GIF version |
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 |
---|---|
df-fin7 | ⊢ FinVII = {𝑥 ∣ ¬ ∃𝑦 ∈ (On ∖ ω)𝑥 ≈ 𝑦} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cfin7 9928 | . 2 class FinVII | |
2 | vx | . . . . . . 7 setvar 𝑥 | |
3 | 2 | cv 1542 | . . . . . 6 class 𝑥 |
4 | vy | . . . . . . 7 setvar 𝑦 | |
5 | 4 | cv 1542 | . . . . . 6 class 𝑦 |
6 | cen 8647 | . . . . . 6 class ≈ | |
7 | 3, 5, 6 | wbr 5070 | . . . . 5 wff 𝑥 ≈ 𝑦 |
8 | con0 6234 | . . . . . 6 class On | |
9 | com 7666 | . . . . . 6 class ω | |
10 | 8, 9 | cdif 3880 | . . . . 5 class (On ∖ ω) |
11 | 7, 4, 10 | wrex 3065 | . . . 4 wff ∃𝑦 ∈ (On ∖ ω)𝑥 ≈ 𝑦 |
12 | 11 | wn 3 | . . 3 wff ¬ ∃𝑦 ∈ (On ∖ ω)𝑥 ≈ 𝑦 |
13 | 12, 2 | cab 2716 | . 2 class {𝑥 ∣ ¬ ∃𝑦 ∈ (On ∖ ω)𝑥 ≈ 𝑦} |
14 | 1, 13 | wceq 1543 | 1 wff FinVII = {𝑥 ∣ ¬ ∃𝑦 ∈ (On ∖ ω)𝑥 ≈ 𝑦} |
Colors of variables: wff setvar class |
This definition is referenced by: isfin7 9945 |
Copyright terms: Public domain | W3C validator |