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 = { 𝑥 ∣ ∀ 𝑦 ∈ 𝒫 𝒫 𝑥 ( ( 𝑦 ≠ ∅ ∧ [⊊] Or 𝑦 ) → ∪ 𝑦 ∈ 𝑦 ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfin2 ⊢ FinII
1 vx ⊢ 𝑥
2 vy ⊢ 𝑦
3 1 cv ⊢ 𝑥
4 3 cpw ⊢ 𝒫 𝑥
5 4 cpw ⊢ 𝒫 𝒫 𝑥
6 2 cv ⊢ 𝑦
7 c0 ⊢ ∅
8 6 7 wne ⊢ 𝑦 ≠ ∅
9 crpss ⊢ [⊊]
10 6 9 wor ⊢ [⊊] Or 𝑦
11 8 10 wa ⊢ ( 𝑦 ≠ ∅ ∧ [⊊] Or 𝑦 )
12 6 cuni ⊢ ∪ 𝑦
13 12 6 wcel ⊢ ∪ 𝑦 ∈ 𝑦
14 11 13 wi ⊢ ( ( 𝑦 ≠ ∅ ∧ [⊊] Or 𝑦 ) → ∪ 𝑦 ∈ 𝑦 )
15 14 2 5 wral ⊢ ∀ 𝑦 ∈ 𝒫 𝒫 𝑥 ( ( 𝑦 ≠ ∅ ∧ [⊊] Or 𝑦 ) → ∪ 𝑦 ∈ 𝑦 )
16 15 1 cab ⊢ { 𝑥 ∣ ∀ 𝑦 ∈ 𝒫 𝒫 𝑥 ( ( 𝑦 ≠ ∅ ∧ [⊊] Or 𝑦 ) → ∪ 𝑦 ∈ 𝑦 ) }
17 0 16 wceq ⊢ FinII = { 𝑥 ∣ ∀ 𝑦 ∈ 𝒫 𝒫 𝑥 ( ( 𝑦 ≠ ∅ ∧ [⊊] Or 𝑦 ) → ∪ 𝑦 ∈ 𝑦 ) }