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

Metamath Proof Explorer

Definition df-fin4

Description: A set is IV-finite (Dedekind finite) iff it has no equinumerous proper subset. Definition IV of Levy58 p. 3. (Contributed by Stefan O'Rear, 12-Nov-2014)

Ref Expression
Assertion df-fin4 FinIV = { 𝑥 ∣ ¬ ∃ 𝑦 ( 𝑦 ⊊ 𝑥 ∧ 𝑦 ≈ 𝑥 ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfin4 ⊢ FinIV
1 vx ⊢ 𝑥
2 vy ⊢ 𝑦
3 2 cv ⊢ 𝑦
4 1 cv ⊢ 𝑥
5 3 4 wpss ⊢ 𝑦 ⊊ 𝑥
6 cen ⊢ ≈
7 3 4 6 wbr ⊢ 𝑦 ≈ 𝑥
8 5 7 wa ⊢ ( 𝑦 ⊊ 𝑥 ∧ 𝑦 ≈ 𝑥 )
9 8 2 wex ⊢ ∃ 𝑦 ( 𝑦 ⊊ 𝑥 ∧ 𝑦 ≈ 𝑥 )
10 9 wn ⊢ ¬ ∃ 𝑦 ( 𝑦 ⊊ 𝑥 ∧ 𝑦 ≈ 𝑥 )
11 10 1 cab ⊢ { 𝑥 ∣ ¬ ∃ 𝑦 ( 𝑦 ⊊ 𝑥 ∧ 𝑦 ≈ 𝑥 ) }
12 0 11 wceq ⊢ FinIV = { 𝑥 ∣ ¬ ∃ 𝑦 ( 𝑦 ⊊ 𝑥 ∧ 𝑦 ≈ 𝑥 ) }