Metamath Proof Explorer


Theorem umgredgprv

Description: In a multigraph, an edge is an unordered pair of vertices. This theorem would not hold for arbitrary hyper-/pseudographs since either M or N could be proper classes ( ( EX ) would be a loop in this case), which are no vertices of course. (Contributed by Alexander van der Vekens, 19-Aug-2017) (Revised by AV, 11-Dec-2020)

Ref Expression
Hypotheses umgrnloopv.e 𝐸 = ( iEdg ‘ 𝐺 )
umgredgprv.v 𝑉 = ( Vtx ‘ 𝐺 )
Assertion umgredgprv ( ( 𝐺 ∈ UMGraph ∧ 𝑋 ∈ dom 𝐸 ) → ( ( 𝐸𝑋 ) = { 𝑀 , 𝑁 } → ( 𝑀𝑉𝑁𝑉 ) ) )

Proof

Step Hyp Ref Expression
1 umgrnloopv.e 𝐸 = ( iEdg ‘ 𝐺 )
2 umgredgprv.v 𝑉 = ( Vtx ‘ 𝐺 )
3 umgruhgr ( 𝐺 ∈ UMGraph → 𝐺 ∈ UHGraph )
4 2 1 uhgrss ( ( 𝐺 ∈ UHGraph ∧ 𝑋 ∈ dom 𝐸 ) → ( 𝐸𝑋 ) ⊆ 𝑉 )
5 3 4 sylan ( ( 𝐺 ∈ UMGraph ∧ 𝑋 ∈ dom 𝐸 ) → ( 𝐸𝑋 ) ⊆ 𝑉 )
6 2 1 umgredg2 ( ( 𝐺 ∈ UMGraph ∧ 𝑋 ∈ dom 𝐸 ) → ( ♯ ‘ ( 𝐸𝑋 ) ) = 2 )
7 sseq1 ( ( 𝐸𝑋 ) = { 𝑀 , 𝑁 } → ( ( 𝐸𝑋 ) ⊆ 𝑉 ↔ { 𝑀 , 𝑁 } ⊆ 𝑉 ) )
8 fveqeq2 ( ( 𝐸𝑋 ) = { 𝑀 , 𝑁 } → ( ( ♯ ‘ ( 𝐸𝑋 ) ) = 2 ↔ ( ♯ ‘ { 𝑀 , 𝑁 } ) = 2 ) )
9 7 8 anbi12d ( ( 𝐸𝑋 ) = { 𝑀 , 𝑁 } → ( ( ( 𝐸𝑋 ) ⊆ 𝑉 ∧ ( ♯ ‘ ( 𝐸𝑋 ) ) = 2 ) ↔ ( { 𝑀 , 𝑁 } ⊆ 𝑉 ∧ ( ♯ ‘ { 𝑀 , 𝑁 } ) = 2 ) ) )
10 eqid { 𝑀 , 𝑁 } = { 𝑀 , 𝑁 }
11 10 hashprdifel ( ( ♯ ‘ { 𝑀 , 𝑁 } ) = 2 → ( 𝑀 ∈ { 𝑀 , 𝑁 } ∧ 𝑁 ∈ { 𝑀 , 𝑁 } ∧ 𝑀𝑁 ) )
12 prssg ( ( 𝑀 ∈ { 𝑀 , 𝑁 } ∧ 𝑁 ∈ { 𝑀 , 𝑁 } ) → ( ( 𝑀𝑉𝑁𝑉 ) ↔ { 𝑀 , 𝑁 } ⊆ 𝑉 ) )
13 12 3adant3 ( ( 𝑀 ∈ { 𝑀 , 𝑁 } ∧ 𝑁 ∈ { 𝑀 , 𝑁 } ∧ 𝑀𝑁 ) → ( ( 𝑀𝑉𝑁𝑉 ) ↔ { 𝑀 , 𝑁 } ⊆ 𝑉 ) )
14 13 biimprd ( ( 𝑀 ∈ { 𝑀 , 𝑁 } ∧ 𝑁 ∈ { 𝑀 , 𝑁 } ∧ 𝑀𝑁 ) → ( { 𝑀 , 𝑁 } ⊆ 𝑉 → ( 𝑀𝑉𝑁𝑉 ) ) )
15 11 14 syl ( ( ♯ ‘ { 𝑀 , 𝑁 } ) = 2 → ( { 𝑀 , 𝑁 } ⊆ 𝑉 → ( 𝑀𝑉𝑁𝑉 ) ) )
16 15 impcom ( ( { 𝑀 , 𝑁 } ⊆ 𝑉 ∧ ( ♯ ‘ { 𝑀 , 𝑁 } ) = 2 ) → ( 𝑀𝑉𝑁𝑉 ) )
17 9 16 syl6bi ( ( 𝐸𝑋 ) = { 𝑀 , 𝑁 } → ( ( ( 𝐸𝑋 ) ⊆ 𝑉 ∧ ( ♯ ‘ ( 𝐸𝑋 ) ) = 2 ) → ( 𝑀𝑉𝑁𝑉 ) ) )
18 17 com12 ( ( ( 𝐸𝑋 ) ⊆ 𝑉 ∧ ( ♯ ‘ ( 𝐸𝑋 ) ) = 2 ) → ( ( 𝐸𝑋 ) = { 𝑀 , 𝑁 } → ( 𝑀𝑉𝑁𝑉 ) ) )
19 5 6 18 syl2anc ( ( 𝐺 ∈ UMGraph ∧ 𝑋 ∈ dom 𝐸 ) → ( ( 𝐸𝑋 ) = { 𝑀 , 𝑁 } → ( 𝑀𝑉𝑁𝑉 ) ) )