Definition df-fin2 9108

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.)

Assertion

Ref	Expression
df-fin2	|- FinII = { x | A. y e. ~P ~P x ( ( y =/= (/) /\ [ C.] Or y ) -> U. y e. y ) }

Distinct variable group:   x, y

Detailed syntax breakdown of Definition df-fin2

Step	Hyp	Ref	Expression
1		cfin2 9101	. 2 class FinII
2		vy	. . . . . . . 8 setvar y
3	2	cv 1482	. . . . . . 7 class y
4		c0 3915	. . . . . . 7 class (/)
5	3, 4	wne 2794	. . . . . 6 wff y =/= (/)
6		crpss 6936	. . . . . . 7 class [ C.]
7	3, 6	wor 5034	. . . . . 6 wff [ C.] Or y
8	5, 7	wa 384	. . . . 5 wff ( y =/= (/) /\ [ C.] Or y )
9	3	cuni 4436	. . . . . 6 class U. y
10	9, 3	wcel 1990	. . . . 5 wff U. y e. y
11	8, 10	wi 4	. . . 4 wff ( ( y =/= (/) /\ [ C.] Or y ) -> U. y e. y )
12		vx	. . . . . . 7 setvar x
13	12	cv 1482	. . . . . 6 class x
14	13	cpw 4158	. . . . 5 class ~P x
15	14	cpw 4158	. . . 4 class ~P ~P x
16	11, 2, 15	wral 2912	. . 3 wff A. y e. ~P ~P x ( ( y =/= (/) /\ [ C.] Or y ) -> U. y e. y )
17	16, 12	cab 2608	. 2 class { x | A. y e. ~P ~P x ( ( y =/= (/) /\ [ C.] Or y ) -> U. y e. y ) }
18	1, 17	wceq 1483	1 wff FinII = { x | A. y e. ~P ~P x ( ( y =/= (/) /\ [ C.] Or y ) -> U. y e. y ) }

This definition is referenced by:  isfin2  9116