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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
fusgrmaxsize.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
usgrsscusgra.h ⊢ 𝑉 = ( Vtx ‘ 𝐻 )
usgrsscusgra.f ⊢ 𝐹 = ( Edg ‘ 𝐻 )
Assertion sizusglecusg ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ ComplUSGraph ) → ( ♯ ‘ 𝐸 ) ≤ ( ♯ ‘ 𝐹 ) )

Proof

Step Hyp Ref Expression
1 fusgrmaxsize.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 fusgrmaxsize.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 usgrsscusgra.h ⊢ 𝑉 = ( Vtx ‘ 𝐻 )
4 usgrsscusgra.f ⊢ 𝐹 = ( Edg ‘ 𝐻 )
5 2 fvexi ⊢ 𝐸 ∈ V
6 resiexg ⊢ ( 𝐸 ∈ V → ( I ↾ 𝐸 ) ∈ V )
7 5 6 mp1i ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ ComplUSGraph ) → ( I ↾ 𝐸 ) ∈ V )
8 1 2 3 4 sizusglecusglem1 ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ ComplUSGraph ) → ( I ↾ 𝐸 ) : 𝐸 –1-1→ 𝐹 )
9 f1eq1 ⊢ ( 𝑓 = ( I ↾ 𝐸 ) → ( 𝑓 : 𝐸 –1-1→ 𝐹 ↔ ( I ↾ 𝐸 ) : 𝐸 –1-1→ 𝐹 ) )
10 7 8 9 spcedv ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ ComplUSGraph ) → ∃ 𝑓 𝑓 : 𝐸 –1-1→ 𝐹 )
11 10 adantl ⊢ ( ( ( 𝐸 ∈ Fin ∧ 𝐹 ∈ Fin ) ∧ ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ ComplUSGraph ) ) → ∃ 𝑓 𝑓 : 𝐸 –1-1→ 𝐹 )
12 hashdom ⊢ ( ( 𝐸 ∈ Fin ∧ 𝐹 ∈ Fin ) → ( ( ♯ ‘ 𝐸 ) ≤ ( ♯ ‘ 𝐹 ) ↔ 𝐸 ≼ 𝐹 ) )
13 12 adantr ⊢ ( ( ( 𝐸 ∈ Fin ∧ 𝐹 ∈ Fin ) ∧ ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ ComplUSGraph ) ) → ( ( ♯ ‘ 𝐸 ) ≤ ( ♯ ‘ 𝐹 ) ↔ 𝐸 ≼ 𝐹 ) )
14 brdomg ⊢ ( 𝐹 ∈ Fin → ( 𝐸 ≼ 𝐹 ↔ ∃ 𝑓 𝑓 : 𝐸 –1-1→ 𝐹 ) )
15 14 adantl ⊢ ( ( 𝐸 ∈ Fin ∧ 𝐹 ∈ Fin ) → ( 𝐸 ≼ 𝐹 ↔ ∃ 𝑓 𝑓 : 𝐸 –1-1→ 𝐹 ) )
16 15 adantr ⊢ ( ( ( 𝐸 ∈ Fin ∧ 𝐹 ∈ Fin ) ∧ ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ ComplUSGraph ) ) → ( 𝐸 ≼ 𝐹 ↔ ∃ 𝑓 𝑓 : 𝐸 –1-1→ 𝐹 ) )
17 13 16 bitrd ⊢ ( ( ( 𝐸 ∈ Fin ∧ 𝐹 ∈ Fin ) ∧ ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ ComplUSGraph ) ) → ( ( ♯ ‘ 𝐸 ) ≤ ( ♯ ‘ 𝐹 ) ↔ ∃ 𝑓 𝑓 : 𝐸 –1-1→ 𝐹 ) )
18 11 17 mpbird ⊢ ( ( ( 𝐸 ∈ Fin ∧ 𝐹 ∈ Fin ) ∧ ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ ComplUSGraph ) ) → ( ♯ ‘ 𝐸 ) ≤ ( ♯ ‘ 𝐹 ) )
19 18 exp31 ⊢ ( 𝐸 ∈ Fin → ( 𝐹 ∈ Fin → ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ ComplUSGraph ) → ( ♯ ‘ 𝐸 ) ≤ ( ♯ ‘ 𝐹 ) ) ) )
20 1 2 3 4 sizusglecusglem2 ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ ComplUSGraph ∧ 𝐹 ∈ Fin ) → 𝐸 ∈ Fin )
21 20 pm2.24d ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ ComplUSGraph ∧ 𝐹 ∈ Fin ) → ( ¬ 𝐸 ∈ Fin → ( ♯ ‘ 𝐸 ) ≤ ( ♯ ‘ 𝐹 ) ) )
22 21 3expia ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ ComplUSGraph ) → ( 𝐹 ∈ Fin → ( ¬ 𝐸 ∈ Fin → ( ♯ ‘ 𝐸 ) ≤ ( ♯ ‘ 𝐹 ) ) ) )
23 22 com13 ⊢ ( ¬ 𝐸 ∈ Fin → ( 𝐹 ∈ Fin → ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ ComplUSGraph ) → ( ♯ ‘ 𝐸 ) ≤ ( ♯ ‘ 𝐹 ) ) ) )
24 19 23 pm2.61i ⊢ ( 𝐹 ∈ Fin → ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ ComplUSGraph ) → ( ♯ ‘ 𝐸 ) ≤ ( ♯ ‘ 𝐹 ) ) )
25 4 fvexi ⊢ 𝐹 ∈ V
26 nfile ⊢ ( ( 𝐸 ∈ V ∧ 𝐹 ∈ V ∧ ¬ 𝐹 ∈ Fin ) → ( ♯ ‘ 𝐸 ) ≤ ( ♯ ‘ 𝐹 ) )
27 5 25 26 mp3an12 ⊢ ( ¬ 𝐹 ∈ Fin → ( ♯ ‘ 𝐸 ) ≤ ( ♯ ‘ 𝐹 ) )
28 27 a1d ⊢ ( ¬ 𝐹 ∈ Fin → ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ ComplUSGraph ) → ( ♯ ‘ 𝐸 ) ≤ ( ♯ ‘ 𝐹 ) ) )
29 24 28 pm2.61i ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ ComplUSGraph ) → ( ♯ ‘ 𝐸 ) ≤ ( ♯ ‘ 𝐹 ) )