Metamath Proof Explorer

Theorem usgredg2vtxeuALT

Description: Alternate proof of usgredg2vtxeu , using edgiedgb , the general translation from ( iEdgG ) to ( EdgG ) . (Contributed by AV, 18-Oct-2020) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	usgredg2vtxeuALT	$⊢ (G \in USGraph \land E \in Edg (G) \land Y \in E) \to \exists! y \in Vtx (G) E = \{Y, y\}$

Proof

Step	Hyp	Ref	Expression
1		usgruhgr	$⊢ G \in USGraph \to G \in UHGraph$
2		eqid	$⊢ iEdg (G) = iEdg (G)$
3	2	uhgredgiedgb	$⊢ G \in UHGraph \to (E \in Edg (G) \leftrightarrow \exists x \in dom iEdg (G) E = iEdg (G) (x))$
4	1 3	syl	$⊢ G \in USGraph \to (E \in Edg (G) \leftrightarrow \exists x \in dom iEdg (G) E = iEdg (G) (x))$
5		eqid	$⊢ Vtx (G) = Vtx (G)$
6	5 2	usgredgreu	$⊢ (G \in USGraph \land x \in dom iEdg (G) \land Y \in iEdg (G) (x)) \to \exists! y \in Vtx (G) iEdg (G) (x) = \{Y, y\}$
7	6	3expia	$⊢ (G \in USGraph \land x \in dom iEdg (G)) \to (Y \in iEdg (G) (x) \to \exists! y \in Vtx (G) iEdg (G) (x) = \{Y, y\})$
8	7	3adant3	$⊢ (G \in USGraph \land x \in dom iEdg (G) \land E = iEdg (G) (x)) \to (Y \in iEdg (G) (x) \to \exists! y \in Vtx (G) iEdg (G) (x) = \{Y, y\})$
9		eleq2	$⊢ E = iEdg (G) (x) \to (Y \in E \leftrightarrow Y \in iEdg (G) (x))$
10		eqeq1	$⊢ E = iEdg (G) (x) \to (E = \{Y, y\} \leftrightarrow iEdg (G) (x) = \{Y, y\})$
11	10	reubidv	$⊢ E = iEdg (G) (x) \to (\exists! y \in Vtx (G) E = \{Y, y\} \leftrightarrow \exists! y \in Vtx (G) iEdg (G) (x) = \{Y, y\})$
12	9 11	imbi12d	$⊢ E = iEdg (G) (x) \to ((Y \in E \to \exists! y \in Vtx (G) E = \{Y, y\}) \leftrightarrow (Y \in iEdg (G) (x) \to \exists! y \in Vtx (G) iEdg (G) (x) = \{Y, y\}))$
13	12	3ad2ant3	$⊢ (G \in USGraph \land x \in dom iEdg (G) \land E = iEdg (G) (x)) \to ((Y \in E \to \exists! y \in Vtx (G) E = \{Y, y\}) \leftrightarrow (Y \in iEdg (G) (x) \to \exists! y \in Vtx (G) iEdg (G) (x) = \{Y, y\}))$
14	8 13	mpbird	$⊢ (G \in USGraph \land x \in dom iEdg (G) \land E = iEdg (G) (x)) \to (Y \in E \to \exists! y \in Vtx (G) E = \{Y, y\})$
15	14	3exp	$⊢ G \in USGraph \to (x \in dom iEdg (G) \to (E = iEdg (G) (x) \to (Y \in E \to \exists! y \in Vtx (G) E = \{Y, y\})))$
16	15	rexlimdv	$⊢ G \in USGraph \to (\exists x \in dom iEdg (G) E = iEdg (G) (x) \to (Y \in E \to \exists! y \in Vtx (G) E = \{Y, y\}))$
17	4 16	sylbid	$⊢ G \in USGraph \to (E \in Edg (G) \to (Y \in E \to \exists! y \in Vtx (G) E = \{Y, y\}))$
18	17	3imp	$⊢ (G \in USGraph \land E \in Edg (G) \land Y \in E) \to \exists! y \in Vtx (G) E = \{Y, y\}$