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

Metamath Proof Explorer

Definition df-fin2

Description: A set is II-finite (Tarski finite) iff every nonempty chain of subsets contains a maximum element. Definition II of Levy58 p. 2. (Contributed by Stefan O'Rear, 12-Nov-2014)

Ref Expression
Assertion df-fin2 ⊢ FinII = x | ∀ y ∈ 𝒫 𝒫 x y ≠ ∅ ∧ [⊂] Or y → ⋃ y ∈ y

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfin2 class FinII
1 vx setvar x
2 vy setvar y
3 1 cv setvar x
4 3 cpw class 𝒫 x
5 4 cpw class 𝒫 𝒫 x
6 2 cv setvar y
7 c0 class ∅
8 6 7 wne wff y ≠ ∅
9 crpss class [⊂]
10 6 9 wor wff [⊂] Or y
11 8 10 wa wff y ≠ ∅ ∧ [⊂] Or y
12 6 cuni class ⋃ y
13 12 6 wcel wff ⋃ y ∈ y
14 11 13 wi wff y ≠ ∅ ∧ [⊂] Or y → ⋃ y ∈ y
15 14 2 5 wral wff ∀ y ∈ 𝒫 𝒫 x y ≠ ∅ ∧ [⊂] Or y → ⋃ y ∈ y
16 15 1 cab class x | ∀ y ∈ 𝒫 𝒫 x y ≠ ∅ ∧ [⊂] Or y → ⋃ y ∈ y
17 0 16 wceq wff FinII = x | ∀ y ∈ 𝒫 𝒫 x y ≠ ∅ ∧ [⊂] Or y → ⋃ y ∈ y