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 biimtrdi ⊢ ( ( 𝐸 ‘ 𝑋 ) = { 𝑀 , 𝑁 } → ( ( ( 𝐸 ‘ 𝑋 ) ⊆ 𝑉 ∧ ( ♯ ‘ ( 𝐸 ‘ 𝑋 ) ) = 2 ) → ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) )
18 17 com12 ⊢ ( ( ( 𝐸 ‘ 𝑋 ) ⊆ 𝑉 ∧ ( ♯ ‘ ( 𝐸 ‘ 𝑋 ) ) = 2 ) → ( ( 𝐸 ‘ 𝑋 ) = { 𝑀 , 𝑁 } → ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) )
19 5 6 18 syl2anc ⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑋 ∈ dom 𝐸 ) → ( ( 𝐸 ‘ 𝑋 ) = { 𝑀 , 𝑁 } → ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) )