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 USGraph H 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 V
6 resiexg E V I E V
7 5 6 mp1i G USGraph H ComplUSGraph I E V
8 1 2 3 4 sizusglecusglem1 G USGraph H 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 USGraph H ComplUSGraph f f : E 1-1 F
11 10 adantl E Fin F Fin G USGraph H ComplUSGraph f f : E 1-1 F
12 hashdom E Fin F Fin E F E F
13 12 adantr E Fin F Fin G USGraph H ComplUSGraph E F E F
14 brdomg F Fin E F f f : E 1-1 F
15 14 adantl E Fin F Fin E F f f : E 1-1 F
16 15 adantr E Fin F Fin G USGraph H ComplUSGraph E F f f : E 1-1 F
17 13 16 bitrd E Fin F Fin G USGraph H ComplUSGraph E F f f : E 1-1 F
18 11 17 mpbird E Fin F Fin G USGraph H ComplUSGraph E F
19 18 exp31 E Fin F Fin G USGraph H ComplUSGraph E F
20 1 2 3 4 sizusglecusglem2 G USGraph H ComplUSGraph F Fin E Fin
21 20 pm2.24d G USGraph H ComplUSGraph F Fin ¬ E Fin E F
22 21 3expia G USGraph H ComplUSGraph F Fin ¬ E Fin E F
23 22 com13 ¬ E Fin F Fin G USGraph H ComplUSGraph E F
24 19 23 pm2.61i F Fin G USGraph H ComplUSGraph E F
25 4 fvexi F V
26 nfile E V F V ¬ F Fin E F
27 5 25 26 mp3an12 ¬ F Fin E F
28 27 a1d ¬ F Fin G USGraph H ComplUSGraph E F
29 24 28 pm2.61i G USGraph H ComplUSGraph E F