usgredgop

Description: An edge of a simple graph as second component of an ordered pair. (Contributed by Alexander van der Vekens, 17-Aug-2017) (Proof shortened by Alexander van der Vekens, 16-Dec-2017) (Revised by AV, 15-Oct-2020)

		Ref	Expression
	Assertion	usgredgop	$⊢ (G \in USGraph \land E = iEdg (G) \land X \in dom E) \to (E (X) = \{M, N\} \leftrightarrow ⟨X, \{M, N\}⟩ \in E)$

Proof

Step	Hyp	Ref	Expression
1		usgrfun	$⊢ G \in USGraph \to Fun iEdg (G)$
2		funeq	$⊢ E = iEdg (G) \to (Fun E \leftrightarrow Fun iEdg (G))$
3	1 2	syl5ibrcom	$⊢ G \in USGraph \to (E = iEdg (G) \to Fun E)$
4	3	imp	$⊢ (G \in USGraph \land E = iEdg (G)) \to Fun E$
5		funopfvb	$⊢ (Fun E \land X \in dom E) \to (E (X) = \{M, N\} \leftrightarrow ⟨X, \{M, N\}⟩ \in E)$
6	4 5	stoic3	$⊢ (G \in USGraph \land E = iEdg (G) \land X \in dom E) \to (E (X) = \{M, N\} \leftrightarrow ⟨X, \{M, N\}⟩ \in E)$

Metamath Proof Explorer

Theorem usgredgop

Proof