Database
GRAPH THEORY
Undirected graphs
Neighbors, complete graphs and universal vertices
Complete graphs
usgrsscusgr
Metamath Proof Explorer
Description: A simple graph is a subgraph of a complete simple graph. (Contributed by Alexander van der Vekens , 11-Jan-2018) (Revised by AV , 13-Nov-2020)
Ref
Expression
Hypotheses
fusgrmaxsize.v
⊢ 𝑉 = ( Vtx ‘ 𝐺 )
fusgrmaxsize.e
⊢ 𝐸 = ( Edg ‘ 𝐺 )
usgrsscusgra.h
⊢ 𝑉 = ( Vtx ‘ 𝐻 )
usgrsscusgra.f
⊢ 𝐹 = ( Edg ‘ 𝐻 )
Assertion
usgrsscusgr
⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ ComplUSGraph ) → ∀ 𝑒 ∈ 𝐸 ∃ 𝑓 ∈ 𝐹 𝑒 = 𝑓 )
Proof
Step
Hyp
Ref
Expression
1
fusgrmaxsize.v
⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2
fusgrmaxsize.e
⊢ 𝐸 = ( Edg ‘ 𝐺 )
3
usgrsscusgra.h
⊢ 𝑉 = ( Vtx ‘ 𝐻 )
4
usgrsscusgra.f
⊢ 𝐹 = ( Edg ‘ 𝐻 )
5
1 2 3 4
usgredgsscusgredg
⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ ComplUSGraph ) → 𝐸 ⊆ 𝐹 )
6
dfss5
⊢ ( 𝐸 ⊆ 𝐹 ↔ ∀ 𝑒 ∈ 𝐸 ∃ 𝑓 ∈ 𝐹 𝑒 = 𝑓 )
7
5 6
sylib
⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ ComplUSGraph ) → ∀ 𝑒 ∈ 𝐸 ∃ 𝑓 ∈ 𝐹 𝑒 = 𝑓 )