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

Metamath Proof Explorer

Theorem sizusglecusg

Description: The size of a simple graph with n vertices is at most the size of a complete simple graph with n vertices ( n may be infinite). (Contributed by Alexander van der Vekens, 13-Jan-2018) (Revised by AV, 13-Nov-2020)

Ref Expression
Hypotheses fusgrmaxsize.v 
|- V = ( Vtx ` G )
fusgrmaxsize.e 
|- E = ( Edg ` G )
usgrsscusgra.h 
|- V = ( Vtx ` H )
usgrsscusgra.f 
|- F = ( Edg ` H )
Assertion sizusglecusg 
|- ( ( G e. USGraph /\ H e. ComplUSGraph ) -> ( # ` E ) <_ ( # ` F ) )

Proof

Step Hyp Ref Expression
1 fusgrmaxsize.v 
 |-  V = ( Vtx ` G )
2 fusgrmaxsize.e 
 |-  E = ( Edg ` G )
3 usgrsscusgra.h 
 |-  V = ( Vtx ` H )
4 usgrsscusgra.f 
 |-  F = ( Edg ` H )
5 2 fvexi 
 |-  E e. _V
6 resiexg 
 |-  ( E e. _V -> ( _I |` E ) e. _V )
7 5 6 mp1i 
 |-  ( ( G e. USGraph /\ H e. ComplUSGraph ) -> ( _I |` E ) e. _V )
8 1 2 3 4 sizusglecusglem1 
 |-  ( ( G e. USGraph /\ H e. ComplUSGraph ) -> ( _I |` E ) : E -1-1-> F )
9 f1eq1 
 |-  ( f = ( _I |` E ) -> ( f : E -1-1-> F <-> ( _I |` E ) : E -1-1-> F ) )
10 7 8 9 spcedv 
 |-  ( ( G e. USGraph /\ H e. ComplUSGraph ) -> E. f f : E -1-1-> F )
11 10 adantl 
 |-  ( ( ( E e. Fin /\ F e. Fin ) /\ ( G e. USGraph /\ H e. ComplUSGraph ) ) -> E. f f : E -1-1-> F )
12 hashdom 
 |-  ( ( E e. Fin /\ F e. Fin ) -> ( ( # ` E ) <_ ( # ` F ) <-> E ~<_ F ) )
13 12 adantr 
 |-  ( ( ( E e. Fin /\ F e. Fin ) /\ ( G e. USGraph /\ H e. ComplUSGraph ) ) -> ( ( # ` E ) <_ ( # ` F ) <-> E ~<_ F ) )
14 brdomg 
 |-  ( F e. Fin -> ( E ~<_ F <-> E. f f : E -1-1-> F ) )
15 14 adantl 
 |-  ( ( E e. Fin /\ F e. Fin ) -> ( E ~<_ F <-> E. f f : E -1-1-> F ) )
16 15 adantr 
 |-  ( ( ( E e. Fin /\ F e. Fin ) /\ ( G e. USGraph /\ H e. ComplUSGraph ) ) -> ( E ~<_ F <-> E. f f : E -1-1-> F ) )
17 13 16 bitrd 
 |-  ( ( ( E e. Fin /\ F e. Fin ) /\ ( G e. USGraph /\ H e. ComplUSGraph ) ) -> ( ( # ` E ) <_ ( # ` F ) <-> E. f f : E -1-1-> F ) )
18 11 17 mpbird 
 |-  ( ( ( E e. Fin /\ F e. Fin ) /\ ( G e. USGraph /\ H e. ComplUSGraph ) ) -> ( # ` E ) <_ ( # ` F ) )
19 18 exp31 
 |-  ( E e. Fin -> ( F e. Fin -> ( ( G e. USGraph /\ H e. ComplUSGraph ) -> ( # ` E ) <_ ( # ` F ) ) ) )
20 1 2 3 4 sizusglecusglem2 
 |-  ( ( G e. USGraph /\ H e. ComplUSGraph /\ F e. Fin ) -> E e. Fin )
21 20 pm2.24d 
 |-  ( ( G e. USGraph /\ H e. ComplUSGraph /\ F e. Fin ) -> ( -. E e. Fin -> ( # ` E ) <_ ( # ` F ) ) )
22 21 3expia 
 |-  ( ( G e. USGraph /\ H e. ComplUSGraph ) -> ( F e. Fin -> ( -. E e. Fin -> ( # ` E ) <_ ( # ` F ) ) ) )
23 22 com13 
 |-  ( -. E e. Fin -> ( F e. Fin -> ( ( G e. USGraph /\ H e. ComplUSGraph ) -> ( # ` E ) <_ ( # ` F ) ) ) )
24 19 23 pm2.61i 
 |-  ( F e. Fin -> ( ( G e. USGraph /\ H e. ComplUSGraph ) -> ( # ` E ) <_ ( # ` F ) ) )
25 4 fvexi 
 |-  F e. _V
26 nfile 
 |-  ( ( E e. _V /\ F e. _V /\ -. F e. Fin ) -> ( # ` E ) <_ ( # ` F ) )
27 5 25 26 mp3an12 
 |-  ( -. F e. Fin -> ( # ` E ) <_ ( # ` F ) )
28 27 a1d 
 |-  ( -. F e. Fin -> ( ( G e. USGraph /\ H e. ComplUSGraph ) -> ( # ` E ) <_ ( # ` F ) ) )
29 24 28 pm2.61i 
 |-  ( ( G e. USGraph /\ H e. ComplUSGraph ) -> ( # ` E ) <_ ( # ` F ) )