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

Metamath Proof Explorer

Theorem umgrnloop2

Description: A multigraph has no loops. (Contributed by AV, 27-Oct-2020) (Revised by AV, 30-Nov-2020)

Ref Expression
Assertion umgrnloop2 
|- ( G e. UMGraph -> { N , N } e/ ( Edg ` G ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
2 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
3 1 2 umgrpredgv 
 |-  ( ( G e. UMGraph /\ { N , N } e. ( Edg ` G ) ) -> ( N e. ( Vtx ` G ) /\ N e. ( Vtx ` G ) ) )
4 3 simpld 
 |-  ( ( G e. UMGraph /\ { N , N } e. ( Edg ` G ) ) -> N e. ( Vtx ` G ) )
5 eqid 
 |-  N = N
6 2 umgredgne 
 |-  ( ( G e. UMGraph /\ { N , N } e. ( Edg ` G ) ) -> N =/= N )
7 eqneqall 
 |-  ( N = N -> ( N =/= N -> -. N e. ( Vtx ` G ) ) )
8 5 6 7 mpsyl 
 |-  ( ( G e. UMGraph /\ { N , N } e. ( Edg ` G ) ) -> -. N e. ( Vtx ` G ) )
9 4 8 pm2.65da 
 |-  ( G e. UMGraph -> -. { N , N } e. ( Edg ` G ) )
10 df-nel 
 |-  ( { N , N } e/ ( Edg ` G ) <-> -. { N , N } e. ( Edg ` G ) )
11 9 10 sylibr 
 |-  ( G e. UMGraph -> { N , N } e/ ( Edg ` G ) )