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

Metamath Proof Explorer

Theorem usgredg3

Description: The value of the "edge function" of a simple graph is a set containing two elements (the endvertices of the corresponding edge). (Contributed by Alexander van der Vekens, 18-Dec-2017) (Revised by AV, 17-Oct-2020)

Ref Expression
Hypotheses usgredg3.v 
|- V = ( Vtx ` G )
usgredg3.e 
|- E = ( iEdg ` G )
Assertion usgredg3 
|- ( ( G e. USGraph /\ X e. dom E ) -> E. x e. V E. y e. V ( x =/= y /\ ( E ` X ) = { x , y } ) )

Proof

Step Hyp Ref Expression
1 usgredg3.v 
 |-  V = ( Vtx ` G )
2 usgredg3.e 
 |-  E = ( iEdg ` G )
3 usgrfun 
 |-  ( G e. USGraph -> Fun ( iEdg ` G ) )
4 2 funeqi 
 |-  ( Fun E <-> Fun ( iEdg ` G ) )
5 3 4 sylibr 
 |-  ( G e. USGraph -> Fun E )
6 fvelrn 
 |-  ( ( Fun E /\ X e. dom E ) -> ( E ` X ) e. ran E )
7 5 6 sylan 
 |-  ( ( G e. USGraph /\ X e. dom E ) -> ( E ` X ) e. ran E )
8 edgval 
 |-  ( Edg ` G ) = ran ( iEdg ` G )
9 8 a1i 
 |-  ( G e. USGraph -> ( Edg ` G ) = ran ( iEdg ` G ) )
10 2 eqcomi 
 |-  ( iEdg ` G ) = E
11 10 rneqi 
 |-  ran ( iEdg ` G ) = ran E
12 9 11 eqtrdi 
 |-  ( G e. USGraph -> ( Edg ` G ) = ran E )
13 12 adantr 
 |-  ( ( G e. USGraph /\ X e. dom E ) -> ( Edg ` G ) = ran E )
14 7 13 eleqtrrd 
 |-  ( ( G e. USGraph /\ X e. dom E ) -> ( E ` X ) e. ( Edg ` G ) )
15 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
16 1 15 usgredg 
 |-  ( ( G e. USGraph /\ ( E ` X ) e. ( Edg ` G ) ) -> E. x e. V E. y e. V ( x =/= y /\ ( E ` X ) = { x , y } ) )
17 14 16 syldan 
 |-  ( ( G e. USGraph /\ X e. dom E ) -> E. x e. V E. y e. V ( x =/= y /\ ( E ` X ) = { x , y } ) )