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 \in USGraph \land X \in dom E) \to \exists x \in V \exists y \in V (x \neq y \land E (X) = \{x, y\})$

Proof

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