# 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 ${⊢}{\mathrm{Fin}}^{II}=\left\{{x}|\forall {y}\in 𝒫𝒫{x}\phantom{\rule{.4em}{0ex}}\left(\left({y}\ne \varnothing \wedge \left[\subset \right]\mathrm{Or}{y}\right)\to \bigcup {y}\in {y}\right)\right\}$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cfin2 ${class}{\mathrm{Fin}}^{II}$
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}\varnothing$
8 6 7 wne ${wff}{y}\ne \varnothing$
9 crpss ${class}\left[\subset \right]$
10 6 9 wor ${wff}\left[\subset \right]\mathrm{Or}{y}$
11 8 10 wa ${wff}\left({y}\ne \varnothing \wedge \left[\subset \right]\mathrm{Or}{y}\right)$
12 6 cuni ${class}\bigcup {y}$
13 12 6 wcel ${wff}\bigcup {y}\in {y}$
14 11 13 wi ${wff}\left(\left({y}\ne \varnothing \wedge \left[\subset \right]\mathrm{Or}{y}\right)\to \bigcup {y}\in {y}\right)$
15 14 2 5 wral ${wff}\forall {y}\in 𝒫𝒫{x}\phantom{\rule{.4em}{0ex}}\left(\left({y}\ne \varnothing \wedge \left[\subset \right]\mathrm{Or}{y}\right)\to \bigcup {y}\in {y}\right)$
16 15 1 cab ${class}\left\{{x}|\forall {y}\in 𝒫𝒫{x}\phantom{\rule{.4em}{0ex}}\left(\left({y}\ne \varnothing \wedge \left[\subset \right]\mathrm{Or}{y}\right)\to \bigcup {y}\in {y}\right)\right\}$
17 0 16 wceq ${wff}{\mathrm{Fin}}^{II}=\left\{{x}|\forall {y}\in 𝒫𝒫{x}\phantom{\rule{.4em}{0ex}}\left(\left({y}\ne \varnothing \wedge \left[\subset \right]\mathrm{Or}{y}\right)\to \bigcup {y}\in {y}\right)\right\}$