Metamath Proof Explorer


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