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