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

Metamath Proof Explorer

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 biimtrid ⊢ ( ( 𝑀 ∈ { 𝑀 , 𝑁 } ∧ 𝑁 ∈ { 𝑀 , 𝑁 } ) → ( { 𝑀 , 𝑁 } ∈ 𝒫 ( Vtx ‘ 𝐺 ) → ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) )
14 13 3adant3 ⊢ ( ( 𝑀 ∈ { 𝑀 , 𝑁 } ∧ 𝑁 ∈ { 𝑀 , 𝑁 } ∧ 𝑀 ≠ 𝑁 ) → ( { 𝑀 , 𝑁 } ∈ 𝒫 ( Vtx ‘ 𝐺 ) → ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) )
15 7 14 syl ⊢ ( ( ♯ ‘ { 𝑀 , 𝑁 } ) = 2 → ( { 𝑀 , 𝑁 } ∈ 𝒫 ( Vtx ‘ 𝐺 ) → ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) )
16 15 impcom ⊢ ( ( { 𝑀 , 𝑁 } ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ { 𝑀 , 𝑁 } ) = 2 ) → ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) )
17 5 16 syl ⊢ ( ( 𝐺 ∈ UMGraph ∧ { 𝑀 , 𝑁 } ∈ 𝐸 ) → ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) )