uspgredg2v

Description: In a simple pseudograph, the mapping of edges having a fixed endpoint to the "other" vertex of the edge (which may be the fixed vertex itself in the case of a loop) is a one-to-one function into the set of vertices. (Contributed by Alexander van der Vekens, 4-Jan-2018) (Revised by AV, 6-Dec-2020)

	Ref	Expression
Hypotheses	uspgredg2v.v	$⊢ V = Vtx (G)$
	uspgredg2v.e	$⊢ E = Edg (G)$
	uspgredg2v.a	$⊢ A = \{e \in E \| N \in e\}$
	uspgredg2v.f	$⊢ F = (y \in A ⟼ (ι z \in V \| y = \{N, z\}))$
Assertion	uspgredg2v	$⊢ (G \in USHGraph \land N \in V) \to F : A \underset{1-1}{⟶} V$

Proof

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		uspgredg2v.f	$⊢ F = (y \in A ⟼ (ι z \in V \| y = \{N, z\}))$
5	1 2 3	uspgredg2vlem	$⊢ (G \in USHGraph \land y \in A) \to (ι z \in V \| y = \{N, z\}) \in V$
6	5	ralrimiva	$⊢ G \in USHGraph \to \forall y \in A (ι z \in V \| y = \{N, z\}) \in V$
7	6	adantr	$⊢ (G \in USHGraph \land N \in V) \to \forall y \in A (ι z \in V \| y = \{N, z\}) \in V$
8		preq2	$⊢ z = n \to \{N, z\} = \{N, n\}$
9	8	eqeq2d	$⊢ z = n \to (y = \{N, z\} \leftrightarrow y = \{N, n\})$
10	9	cbvriotavw	$⊢ (ι z \in V \| y = \{N, z\}) = (ι n \in V \| y = \{N, n\})$
11	8	eqeq2d	$⊢ z = n \to (x = \{N, z\} \leftrightarrow x = \{N, n\})$
12	11	cbvriotavw	$⊢ (ι z \in V \| x = \{N, z\}) = (ι n \in V \| x = \{N, n\})$
13		simpl	$⊢ (G \in USHGraph \land N \in V) \to G \in USHGraph$
14		eleq2w	$⊢ e = y \to (N \in e \leftrightarrow N \in y)$
15	14 3	elrab2	$⊢ y \in A \leftrightarrow (y \in E \land N \in y)$
16	2	eleq2i	$⊢ y \in E \leftrightarrow y \in Edg (G)$
17	16	biimpi	$⊢ y \in E \to y \in Edg (G)$
18	17	anim1i	$⊢ (y \in E \land N \in y) \to (y \in Edg (G) \land N \in y)$
19	15 18	sylbi	$⊢ y \in A \to (y \in Edg (G) \land N \in y)$
20	19	adantr	$⊢ (y \in A \land x \in A) \to (y \in Edg (G) \land N \in y)$
21	13 20	anim12i	$⊢ ((G \in USHGraph \land N \in V) \land (y \in A \land x \in A)) \to (G \in USHGraph \land (y \in Edg (G) \land N \in y))$
22		3anass	$⊢ (G \in USHGraph \land y \in Edg (G) \land N \in y) \leftrightarrow (G \in USHGraph \land (y \in Edg (G) \land N \in y))$
23	21 22	sylibr	$⊢ ((G \in USHGraph \land N \in V) \land (y \in A \land x \in A)) \to (G \in USHGraph \land y \in Edg (G) \land N \in y)$
24		uspgredg2vtxeu	$⊢ (G \in USHGraph \land y \in Edg (G) \land N \in y) \to \exists! n \in Vtx (G) y = \{N, n\}$
25		reueq1	$⊢ V = Vtx (G) \to (\exists! n \in V y = \{N, n\} \leftrightarrow \exists! n \in Vtx (G) y = \{N, n\})$
26	1 25	ax-mp	$⊢ \exists! n \in V y = \{N, n\} \leftrightarrow \exists! n \in Vtx (G) y = \{N, n\}$
27	24 26	sylibr	$⊢ (G \in USHGraph \land y \in Edg (G) \land N \in y) \to \exists! n \in V y = \{N, n\}$
28	23 27	syl	$⊢ ((G \in USHGraph \land N \in V) \land (y \in A \land x \in A)) \to \exists! n \in V y = \{N, n\}$
29		eleq2w	$⊢ e = x \to (N \in e \leftrightarrow N \in x)$
30	29 3	elrab2	$⊢ x \in A \leftrightarrow (x \in E \land N \in x)$
31	2	eleq2i	$⊢ x \in E \leftrightarrow x \in Edg (G)$
32	31	biimpi	$⊢ x \in E \to x \in Edg (G)$
33	32	anim1i	$⊢ (x \in E \land N \in x) \to (x \in Edg (G) \land N \in x)$
34	30 33	sylbi	$⊢ x \in A \to (x \in Edg (G) \land N \in x)$
35	34	adantl	$⊢ (y \in A \land x \in A) \to (x \in Edg (G) \land N \in x)$
36	13 35	anim12i	$⊢ ((G \in USHGraph \land N \in V) \land (y \in A \land x \in A)) \to (G \in USHGraph \land (x \in Edg (G) \land N \in x))$
37		3anass	$⊢ (G \in USHGraph \land x \in Edg (G) \land N \in x) \leftrightarrow (G \in USHGraph \land (x \in Edg (G) \land N \in x))$
38	36 37	sylibr	$⊢ ((G \in USHGraph \land N \in V) \land (y \in A \land x \in A)) \to (G \in USHGraph \land x \in Edg (G) \land N \in x)$
39		uspgredg2vtxeu	$⊢ (G \in USHGraph \land x \in Edg (G) \land N \in x) \to \exists! n \in Vtx (G) x = \{N, n\}$
40		reueq1	$⊢ V = Vtx (G) \to (\exists! n \in V x = \{N, n\} \leftrightarrow \exists! n \in Vtx (G) x = \{N, n\})$
41	1 40	ax-mp	$⊢ \exists! n \in V x = \{N, n\} \leftrightarrow \exists! n \in Vtx (G) x = \{N, n\}$
42	39 41	sylibr	$⊢ (G \in USHGraph \land x \in Edg (G) \land N \in x) \to \exists! n \in V x = \{N, n\}$
43	38 42	syl	$⊢ ((G \in USHGraph \land N \in V) \land (y \in A \land x \in A)) \to \exists! n \in V x = \{N, n\}$
44	10 12 28 43	riotaeqimp	$⊢ (((G \in USHGraph \land N \in V) \land (y \in A \land x \in A)) \land (ι z \in V \| y = \{N, z\}) = (ι z \in V \| x = \{N, z\})) \to y = x$
45	44	ex	$⊢ ((G \in USHGraph \land N \in V) \land (y \in A \land x \in A)) \to ((ι z \in V \| y = \{N, z\}) = (ι z \in V \| x = \{N, z\}) \to y = x)$
46	45	ralrimivva	$⊢ (G \in USHGraph \land N \in V) \to \forall y \in A \forall x \in A ((ι z \in V \| y = \{N, z\}) = (ι z \in V \| x = \{N, z\}) \to y = x)$
47		eqeq1	$⊢ y = x \to (y = \{N, z\} \leftrightarrow x = \{N, z\})$
48	47	riotabidv	$⊢ y = x \to (ι z \in V \| y = \{N, z\}) = (ι z \in V \| x = \{N, z\})$
49	4 48	f1mpt	$⊢ F : A \underset{1-1}{⟶} V \leftrightarrow (\forall y \in A (ι z \in V \| y = \{N, z\}) \in V \land \forall y \in A \forall x \in A ((ι z \in V \| y = \{N, z\}) = (ι z \in V \| x = \{N, z\}) \to y = x))$
50	7 46 49	sylanbrc	$⊢ (G \in USHGraph \land N \in V) \to F : A \underset{1-1}{⟶} V$

Metamath Proof Explorer

Theorem uspgredg2v

Proof