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

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 
|- E = ( iEdg ` G )
umgredgprv.v 
|- V = ( Vtx ` G )
Assertion umgredgprv 
|- ( ( G e. UMGraph /\ X e. dom E ) -> ( ( E ` X ) = { M , N } -> ( M e. V /\ N e. V ) ) )

Proof

Step Hyp Ref Expression
1 umgrnloopv.e 
 |-  E = ( iEdg ` G )
2 umgredgprv.v 
 |-  V = ( Vtx ` G )
3 umgruhgr 
 |-  ( G e. UMGraph -> G e. UHGraph )
4 2 1 uhgrss 
 |-  ( ( G e. UHGraph /\ X e. dom E ) -> ( E ` X ) C_ V )
5 3 4 sylan 
 |-  ( ( G e. UMGraph /\ X e. dom E ) -> ( E ` X ) C_ V )
6 2 1 umgredg2 
 |-  ( ( G e. UMGraph /\ X e. dom E ) -> ( # ` ( E ` X ) ) = 2 )
7 sseq1 
 |-  ( ( E ` X ) = { M , N } -> ( ( E ` X ) C_ V <-> { M , N } C_ V ) )
8 fveqeq2 
 |-  ( ( E ` X ) = { M , N } -> ( ( # ` ( E ` X ) ) = 2 <-> ( # ` { M , N } ) = 2 ) )
9 7 8 anbi12d 
 |-  ( ( E ` X ) = { M , N } -> ( ( ( E ` X ) C_ V /\ ( # ` ( E ` X ) ) = 2 ) <-> ( { M , N } C_ V /\ ( # ` { M , N } ) = 2 ) ) )
10 eqid 
 |-  { M , N } = { M , N }
11 10 hashprdifel 
 |-  ( ( # ` { M , N } ) = 2 -> ( M e. { M , N } /\ N e. { M , N } /\ M =/= N ) )
12 prssg 
 |-  ( ( M e. { M , N } /\ N e. { M , N } ) -> ( ( M e. V /\ N e. V ) <-> { M , N } C_ V ) )
13 12 3adant3 
 |-  ( ( M e. { M , N } /\ N e. { M , N } /\ M =/= N ) -> ( ( M e. V /\ N e. V ) <-> { M , N } C_ V ) )
14 13 biimprd 
 |-  ( ( M e. { M , N } /\ N e. { M , N } /\ M =/= N ) -> ( { M , N } C_ V -> ( M e. V /\ N e. V ) ) )
15 11 14 syl 
 |-  ( ( # ` { M , N } ) = 2 -> ( { M , N } C_ V -> ( M e. V /\ N e. V ) ) )
16 15 impcom 
 |-  ( ( { M , N } C_ V /\ ( # ` { M , N } ) = 2 ) -> ( M e. V /\ N e. V ) )
17 9 16 biimtrdi 
 |-  ( ( E ` X ) = { M , N } -> ( ( ( E ` X ) C_ V /\ ( # ` ( E ` X ) ) = 2 ) -> ( M e. V /\ N e. V ) ) )
18 17 com12 
 |-  ( ( ( E ` X ) C_ V /\ ( # ` ( E ` X ) ) = 2 ) -> ( ( E ` X ) = { M , N } -> ( M e. V /\ N e. V ) ) )
19 5 6 18 syl2anc 
 |-  ( ( G e. UMGraph /\ X e. dom E ) -> ( ( E ` X ) = { M , N } -> ( M e. V /\ N e. V ) ) )