Theorem isfin5

Description: Definition of a V-finite set. (Contributed by Stefan O'Rear, 16-May-2015)

	Ref	Expression
Assertion	isfin5	|- ( A e. Fin5 <-> ( A = (/) \/ A ~< ( A |_| A ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-fin5	|- Fin5 = { x | ( x = (/) \/ x ~< ( x |_| x ) ) }
2	1	eleq2i	|- ( A e. Fin5 <-> A e. { x | ( x = (/) \/ x ~< ( x |_| x ) ) } )
3		id	|- ( A = (/) -> A = (/) )
4		0ex	|- (/) e. _V
5	3 4	eqeltrdi	|- ( A = (/) -> A e. _V )
6		relsdom	|- Rel ~<
7	6	brrelex1i	|- ( A ~< ( A |_| A ) -> A e. _V )
8	5 7	jaoi	|- ( ( A = (/) \/ A ~< ( A |_| A ) ) -> A e. _V )
9		eqeq1	|- ( x = A -> ( x = (/) <-> A = (/) ) )
10		id	|- ( x = A -> x = A )
11		djueq12	|- ( ( x = A /\ x = A ) -> ( x |_| x ) = ( A |_| A ) )
12	11	anidms	|- ( x = A -> ( x |_| x ) = ( A |_| A ) )
13	10 12	breq12d	|- ( x = A -> ( x ~< ( x |_| x ) <-> A ~< ( A |_| A ) ) )
14	9 13	orbi12d	|- ( x = A -> ( ( x = (/) \/ x ~< ( x |_| x ) ) <-> ( A = (/) \/ A ~< ( A |_| A ) ) ) )
15	8 14	elab3	|- ( A e. { x | ( x = (/) \/ x ~< ( x |_| x ) ) } <-> ( A = (/) \/ A ~< ( A |_| A ) ) )
16	2 15	bitri	|- ( A e. Fin5 <-> ( A = (/) \/ A ~< ( A |_| A ) ) )