Theorem umgrpredgv

Description: An edge of a multigraph always connects two vertices. Analogue of umgredgprv . This theorem does not hold for arbitrary pseudographs: if either M or N is a proper class, then { M , N } e. E could still hold ( { M , N } would be either { M } or { N } , see prprc1 or prprc2 , i.e. a loop), but M e. V or N e. V would not be true. (Contributed by AV, 27-Nov-2020)

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

Proof

Step	Hyp	Ref	Expression
1		upgredg.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		upgredg.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
3	2	eleq2i	⊢ ( { 𝑀 , 𝑁 } ∈ 𝐸 ↔ { 𝑀 , 𝑁 } ∈ ( Edg ‘ 𝐺 ) )
4		edgumgr	⊢ ( ( 𝐺 ∈ UMGraph ∧ { 𝑀 , 𝑁 } ∈ ( Edg ‘ 𝐺 ) ) → ( { 𝑀 , 𝑁 } ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ { 𝑀 , 𝑁 } ) = 2 ) )
5	3 4	sylan2b	⊢ ( ( 𝐺 ∈ UMGraph ∧ { 𝑀 , 𝑁 } ∈ 𝐸 ) → ( { 𝑀 , 𝑁 } ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ { 𝑀 , 𝑁 } ) = 2 ) )
6		eqid	⊢ { 𝑀 , 𝑁 } = { 𝑀 , 𝑁 }
7	6	hashprdifel	⊢ ( ( ♯ ‘ { 𝑀 , 𝑁 } ) = 2 → ( 𝑀 ∈ { 𝑀 , 𝑁 } ∧ 𝑁 ∈ { 𝑀 , 𝑁 } ∧ 𝑀 ≠ 𝑁 ) )
8	1	eqcomi	⊢ ( Vtx ‘ 𝐺 ) = 𝑉
9	8	pweqi	⊢ 𝒫 ( Vtx ‘ 𝐺 ) = 𝒫 𝑉
10	9	eleq2i	⊢ ( { 𝑀 , 𝑁 } ∈ 𝒫 ( Vtx ‘ 𝐺 ) ↔ { 𝑀 , 𝑁 } ∈ 𝒫 𝑉 )
11		prelpw	⊢ ( ( 𝑀 ∈ { 𝑀 , 𝑁 } ∧ 𝑁 ∈ { 𝑀 , 𝑁 } ) → ( ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ↔ { 𝑀 , 𝑁 } ∈ 𝒫 𝑉 ) )
12	11	biimprd	⊢ ( ( 𝑀 ∈ { 𝑀 , 𝑁 } ∧ 𝑁 ∈ { 𝑀 , 𝑁 } ) → ( { 𝑀 , 𝑁 } ∈ 𝒫 𝑉 → ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) )
13	10 12	syl5bi	⊢ ( ( 𝑀 ∈ { 𝑀 , 𝑁 } ∧ 𝑁 ∈ { 𝑀 , 𝑁 } ) → ( { 𝑀 , 𝑁 } ∈ 𝒫 ( Vtx ‘ 𝐺 ) → ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) )
14	13	3adant3	⊢ ( ( 𝑀 ∈ { 𝑀 , 𝑁 } ∧ 𝑁 ∈ { 𝑀 , 𝑁 } ∧ 𝑀 ≠ 𝑁 ) → ( { 𝑀 , 𝑁 } ∈ 𝒫 ( Vtx ‘ 𝐺 ) → ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) )
15	7 14	syl	⊢ ( ( ♯ ‘ { 𝑀 , 𝑁 } ) = 2 → ( { 𝑀 , 𝑁 } ∈ 𝒫 ( Vtx ‘ 𝐺 ) → ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) )
16	15	impcom	⊢ ( ( { 𝑀 , 𝑁 } ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ { 𝑀 , 𝑁 } ) = 2 ) → ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) )
17	5 16	syl	⊢ ( ( 𝐺 ∈ UMGraph ∧ { 𝑀 , 𝑁 } ∈ 𝐸 ) → ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) )