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 } ) )