This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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