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