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 )