Metamath Proof Explorer


Theorem usgrsscusgr

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 ) → ∀ 𝑒𝐸𝑓𝐹 𝑒 = 𝑓 )