Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Infinity
Eight inequivalent definitions of finite set
df-fin7
Metamath Proof Explorer
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 ∖ ω ) 𝑥 ≈ 𝑦 }