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 ⊢ V = Vtx ⁡ G
fusgrmaxsize.e ⊢ E = Edg ⁡ G
usgrsscusgra.h ⊢ V = Vtx ⁡ H
usgrsscusgra.f ⊢ F = Edg ⁡ H
Assertion usgrsscusgr ⊢ G ∈ USGraph ∧ H ∈ ComplUSGraph → ∀ e ∈ E ∃ f ∈ F 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 1 2 3 4 usgredgsscusgredg ⊢ G ∈ USGraph ∧ H ∈ ComplUSGraph → E ⊆ F
6 dfss5 ⊢ E ⊆ F ↔ ∀ e ∈ E ∃ f ∈ F e = f
7 5 6 sylib ⊢ G ∈ USGraph ∧ H ∈ ComplUSGraph → ∀ e ∈ E ∃ f ∈ F e = f