uspgredg2vlem

	Ref	Expression
Hypotheses	uspgredg2v.v	$⊢ V = Vtx (G)$
	uspgredg2v.e	$⊢ E = Edg (G)$
	uspgredg2v.a	$⊢ A = \{e \in E \| N \in e\}$
Assertion	uspgredg2vlem	$⊢ (G \in USHGraph \land Y \in A) \to (ι z \in V \| Y = \{N, z\}) \in V$

Step	Hyp	Ref	Expression
1		uspgredg2v.v	$⊢ V = Vtx (G)$
2		uspgredg2v.e	$⊢ E = Edg (G)$
3		uspgredg2v.a	$⊢ A = \{e \in E \| N \in e\}$
4		eleq2	$⊢ e = Y \to (N \in e \leftrightarrow N \in Y)$
5	4 3	elrab2	$⊢ Y \in A \leftrightarrow (Y \in E \land N \in Y)$
6		simpl	$⊢ (G \in USHGraph \land (Y \in E \land N \in Y)) \to G \in USHGraph$
7	2	eleq2i	$⊢ Y \in E \leftrightarrow Y \in Edg (G)$
8	7	biimpi	$⊢ Y \in E \to Y \in Edg (G)$
9	8	ad2antrl	$⊢ (G \in USHGraph \land (Y \in E \land N \in Y)) \to Y \in Edg (G)$
10		simprr	$⊢ (G \in USHGraph \land (Y \in E \land N \in Y)) \to N \in Y$
11	6 9 10	3jca	$⊢ (G \in USHGraph \land (Y \in E \land N \in Y)) \to (G \in USHGraph \land Y \in Edg (G) \land N \in Y)$
12		uspgredg2vtxeu	$⊢ (G \in USHGraph \land Y \in Edg (G) \land N \in Y) \to \exists! z \in Vtx (G) Y = \{N, z\}$
13		reueq1	$⊢ V = Vtx (G) \to (\exists! z \in V Y = \{N, z\} \leftrightarrow \exists! z \in Vtx (G) Y = \{N, z\})$
14	1 13	ax-mp	$⊢ \exists! z \in V Y = \{N, z\} \leftrightarrow \exists! z \in Vtx (G) Y = \{N, z\}$
15	12 14	sylibr	$⊢ (G \in USHGraph \land Y \in Edg (G) \land N \in Y) \to \exists! z \in V Y = \{N, z\}$
16		riotacl	$⊢ \exists! z \in V Y = \{N, z\} \to (ι z \in V \| Y = \{N, z\}) \in V$
17	11 15 16	3syl	$⊢ (G \in USHGraph \land (Y \in E \land N \in Y)) \to (ι z \in V \| Y = \{N, z\}) \in V$
18	5 17	sylan2b	$⊢ (G \in USHGraph \land Y \in A) \to (ι z \in V \| Y = \{N, z\}) \in V$

Metamath Proof Explorer