This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem usgrpredgv

Description: An edge of a simple graph always connects two vertices. Analogue of usgredgprv . (Contributed by Alexander van der Vekens, 7-Oct-2017) (Revised by AV, 9-Jan-2020) (Revised by AV, 23-Oct-2020) (Proof shortened by AV, 27-Nov-2020)

	Ref	Expression
Hypotheses	usgredgppr.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
	usgrpredgv.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion	usgrpredgv	⊢ ( ( 𝐺 ∈ USGraph ∧ { 𝑀 , 𝑁 } ∈ 𝐸 ) → ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) )

Proof

Step	Hyp	Ref	Expression
1		usgredgppr.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
2		usgrpredgv.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
3		usgrumgr	⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ UMGraph )
4	2 1	umgrpredgv	⊢ ( ( 𝐺 ∈ UMGraph ∧ { 𝑀 , 𝑁 } ∈ 𝐸 ) → ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) )
5	3 4	sylan	⊢ ( ( 𝐺 ∈ USGraph ∧ { 𝑀 , 𝑁 } ∈ 𝐸 ) → ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) )