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

Metamath Proof Explorer

Theorem fin45

Description: Every IV-finite set is V-finite: if we can pack two copies of the set into itself, we can certainly leave space. (Contributed by Stefan O'Rear, 30-Oct-2014) (Proof shortened by Mario Carneiro, 18-May-2015)

Ref Expression
Assertion fin45 
|- ( A e. Fin4 -> A e. Fin5 )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( A =/= (/) /\ A ~~ ( A |_| A ) ) -> A =/= (/) )
2 relen 
 |-  Rel ~~
3 2 brrelex1i 
 |-  ( A ~~ ( A |_| A ) -> A e. _V )
4 3 adantl 
 |-  ( ( A =/= (/) /\ A ~~ ( A |_| A ) ) -> A e. _V )
5 0sdomg 
 |-  ( A e. _V -> ( (/) ~< A <-> A =/= (/) ) )
6 4 5 syl 
 |-  ( ( A =/= (/) /\ A ~~ ( A |_| A ) ) -> ( (/) ~< A <-> A =/= (/) ) )
7 1 6 mpbird 
 |-  ( ( A =/= (/) /\ A ~~ ( A |_| A ) ) -> (/) ~< A )
8 0sdom1dom 
 |-  ( (/) ~< A <-> 1o ~<_ A )
9 7 8 sylib 
 |-  ( ( A =/= (/) /\ A ~~ ( A |_| A ) ) -> 1o ~<_ A )
10 djudom2 
 |-  ( ( 1o ~<_ A /\ A e. _V ) -> ( A |_| 1o ) ~<_ ( A |_| A ) )
11 9 4 10 syl2anc 
 |-  ( ( A =/= (/) /\ A ~~ ( A |_| A ) ) -> ( A |_| 1o ) ~<_ ( A |_| A ) )
12 domen2 
 |-  ( A ~~ ( A |_| A ) -> ( ( A |_| 1o ) ~<_ A <-> ( A |_| 1o ) ~<_ ( A |_| A ) ) )
13 12 adantl 
 |-  ( ( A =/= (/) /\ A ~~ ( A |_| A ) ) -> ( ( A |_| 1o ) ~<_ A <-> ( A |_| 1o ) ~<_ ( A |_| A ) ) )
14 11 13 mpbird 
 |-  ( ( A =/= (/) /\ A ~~ ( A |_| A ) ) -> ( A |_| 1o ) ~<_ A )
15 domnsym 
 |-  ( ( A |_| 1o ) ~<_ A -> -. A ~< ( A |_| 1o ) )
16 14 15 syl 
 |-  ( ( A =/= (/) /\ A ~~ ( A |_| A ) ) -> -. A ~< ( A |_| 1o ) )
17 isfin4p1 
 |-  ( A e. Fin4 <-> A ~< ( A |_| 1o ) )
18 17 biimpi 
 |-  ( A e. Fin4 -> A ~< ( A |_| 1o ) )
19 16 18 nsyl3 
 |-  ( A e. Fin4 -> -. ( A =/= (/) /\ A ~~ ( A |_| A ) ) )
20 isfin5-2 
 |-  ( A e. Fin4 -> ( A e. Fin5 <-> -. ( A =/= (/) /\ A ~~ ( A |_| A ) ) ) )
21 19 20 mpbird 
 |-  ( A e. Fin4 -> A e. Fin5 )