Theorem isfin5-2

Description: Alternate definition of V-finite which emphasizes the idempotent behavior of V-infinite sets. (Contributed by Stefan O'Rear, 30-Oct-2014) (Revised by Mario Carneiro, 17-May-2015)

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

Proof

Step	Hyp	Ref	Expression
1		nne	|- ( -. A =/= (/) <-> A = (/) )
2	1	bicomi	|- ( A = (/) <-> -. A =/= (/) )
3	2	a1i	|- ( A e. V -> ( A = (/) <-> -. A =/= (/) ) )
4		djudoml	|- ( ( A e. V /\ A e. V ) -> A ~<_ ( A |_| A ) )
5	4	anidms	|- ( A e. V -> A ~<_ ( A |_| A ) )
6		brsdom	|- ( A ~< ( A |_| A ) <-> ( A ~<_ ( A |_| A ) /\ -. A ~~ ( A |_| A ) ) )
7	6	baib	|- ( A ~<_ ( A |_| A ) -> ( A ~< ( A |_| A ) <-> -. A ~~ ( A |_| A ) ) )
8	5 7	syl	|- ( A e. V -> ( A ~< ( A |_| A ) <-> -. A ~~ ( A |_| A ) ) )
9	3 8	orbi12d	|- ( A e. V -> ( ( A = (/) \/ A ~< ( A |_| A ) ) <-> ( -. A =/= (/) \/ -. A ~~ ( A |_| A ) ) ) )
10		isfin5	|- ( A e. Fin5 <-> ( A = (/) \/ A ~< ( A |_| A ) ) )
11		ianor	|- ( -. ( A =/= (/) /\ A ~~ ( A |_| A ) ) <-> ( -. A =/= (/) \/ -. A ~~ ( A |_| A ) ) )
12	9 10 11	3bitr4g	|- ( A e. V -> ( A e. Fin5 <-> -. ( A =/= (/) /\ A ~~ ( A |_| A ) ) ) )