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	|- Fin2 = { x | A. y e. ~P ~P x ( ( y =/= (/) /\ [C.] Or y ) -> U. y e. y ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfin2	|- Fin2
1		vx	|- x
2		vy	|- y
3	1	cv	|- x
4	3	cpw	|- ~P x
5	4	cpw	|- ~P ~P x
6	2	cv	|- y
7		c0	|- (/)
8	6 7	wne	|- y =/= (/)
9		crpss	|- [C.]
10	6 9	wor	|- [C.] Or y
11	8 10	wa	|- ( y =/= (/) /\ [C.] Or y )
12	6	cuni	|- U. y
13	12 6	wcel	|- U. y e. y
14	11 13	wi	|- ( ( y =/= (/) /\ [C.] Or y ) -> U. y e. y )
15	14 2 5	wral	|- A. y e. ~P ~P x ( ( y =/= (/) /\ [C.] Or y ) -> U. y e. y )
16	15 1	cab	|- { x | A. y e. ~P ~P x ( ( y =/= (/) /\ [C.] Or y ) -> U. y e. y ) }
17	0 16	wceq	|- Fin2 = { x | A. y e. ~P ~P x ( ( y =/= (/) /\ [C.] Or y ) -> U. y e. y ) }