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

Metamath Proof Explorer

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