Metamath Proof Explorer


Definition df-fin5

Description: A set is V-finite iff it behaves finitely under |_| . Definition V of Levy58 p. 3. (Contributed by Stefan O'Rear, 12-Nov-2014)

Ref Expression
Assertion df-fin5
|- Fin5 = { x | ( x = (/) \/ x ~< ( x |_| x ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfin5
 |-  Fin5
1 vx
 |-  x
2 1 cv
 |-  x
3 c0
 |-  (/)
4 2 3 wceq
 |-  x = (/)
5 csdm
 |-  ~<
6 2 2 cdju
 |-  ( x |_| x )
7 2 6 5 wbr
 |-  x ~< ( x |_| x )
8 4 7 wo
 |-  ( x = (/) \/ x ~< ( x |_| x ) )
9 8 1 cab
 |-  { x | ( x = (/) \/ x ~< ( x |_| x ) ) }
10 0 9 wceq
 |-  Fin5 = { x | ( x = (/) \/ x ~< ( x |_| x ) ) }