Theorem isfin6

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

	Ref	Expression
Assertion	isfin6	|- ( A e. Fin6 <-> ( A ~< 2o \/ A ~< ( A X. A ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-fin6	|- Fin6 = { x | ( x ~< 2o \/ x ~< ( x X. x ) ) }
2	1	eleq2i	|- ( A e. Fin6 <-> A e. { x | ( x ~< 2o \/ x ~< ( x X. x ) ) } )
3		relsdom	|- Rel ~<
4	3	brrelex1i	|- ( A ~< 2o -> A e. _V )
5	3	brrelex1i	|- ( A ~< ( A X. A ) -> A e. _V )
6	4 5	jaoi	|- ( ( A ~< 2o \/ A ~< ( A X. A ) ) -> A e. _V )
7		breq1	|- ( x = A -> ( x ~< 2o <-> A ~< 2o ) )
8		id	|- ( x = A -> x = A )
9	8	sqxpeqd	|- ( x = A -> ( x X. x ) = ( A X. A ) )
10	8 9	breq12d	|- ( x = A -> ( x ~< ( x X. x ) <-> A ~< ( A X. A ) ) )
11	7 10	orbi12d	|- ( x = A -> ( ( x ~< 2o \/ x ~< ( x X. x ) ) <-> ( A ~< 2o \/ A ~< ( A X. A ) ) ) )
12	6 11	elab3	|- ( A e. { x | ( x ~< 2o \/ x ~< ( x X. x ) ) } <-> ( A ~< 2o \/ A ~< ( A X. A ) ) )
13	2 12	bitri	|- ( A e. Fin6 <-> ( A ~< 2o \/ A ~< ( A X. A ) ) )