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-1F
9 f1eq1 ⊢f=I↾E→f:E⟶1-1F↔I↾E:E⟶1-1F
10 7 8 9 spcedv ⊢G∈USGraph∧H∈ComplUSGraph→∃ff:E⟶1-1F
11 10 adantl ⊢E∈Fin∧F∈Fin∧G∈USGraph∧H∈ComplUSGraph→∃ff:E⟶1-1F
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↔∃ff:E⟶1-1F
15 14 adantl ⊢E∈Fin∧F∈Fin→E≼F↔∃ff:E⟶1-1F
16 15 adantr ⊢E∈Fin∧F∈Fin∧G∈USGraph∧H∈ComplUSGraph→E≼F↔∃ff:E⟶1-1F
17 13 16 bitrd ⊢E∈Fin∧F∈Fin∧G∈USGraph∧H∈ComplUSGraph→E≤F↔∃ff:E⟶1-1F
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