usgredg2v

Description: In a simple graph, the mapping of edges having a fixed endpoint to the other vertex of the edge is a one-to-one function into the set of vertices. (Contributed by Alexander van der Vekens, 4-Jan-2018) (Revised by AV, 18-Oct-2020)

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

Proof

Step	Hyp	Ref	Expression
1		usgredg2v.v	$⊢ V = Vtx (G)$
2		usgredg2v.e	$⊢ E = iEdg (G)$
3		usgredg2v.a	$⊢ A = \{x \in dom E \| N \in E (x)\}$
4		usgredg2v.f	$⊢ F = (y \in A ⟼ (ι z \in V \| E (y) = \{z, N\}))$
5	1 2 3	usgredg2vlem1	$⊢ (G \in USGraph \land y \in A) \to (ι z \in V \| E (y) = \{z, N\}) \in V$
6	5	ralrimiva	$⊢ G \in USGraph \to \forall y \in A (ι z \in V \| E (y) = \{z, N\}) \in V$
7	6	adantr	$⊢ (G \in USGraph \land N \in V) \to \forall y \in A (ι z \in V \| E (y) = \{z, N\}) \in V$
8	2	usgrf1	$⊢ G \in USGraph \to E : dom E \underset{1-1}{⟶} ran E$
9	8	adantr	$⊢ (G \in USGraph \land N \in V) \to E : dom E \underset{1-1}{⟶} ran E$
10		elrabi	$⊢ y \in \{x \in dom E \| N \in E (x)\} \to y \in dom E$
11	10 3	eleq2s	$⊢ y \in A \to y \in dom E$
12		elrabi	$⊢ w \in \{x \in dom E \| N \in E (x)\} \to w \in dom E$
13	12 3	eleq2s	$⊢ w \in A \to w \in dom E$
14	11 13	anim12i	$⊢ (y \in A \land w \in A) \to (y \in dom E \land w \in dom E)$
15		f1fveq	$⊢ (E : dom E \underset{1-1}{⟶} ran E \land (y \in dom E \land w \in dom E)) \to (E (y) = E (w) \leftrightarrow y = w)$
16	9 14 15	syl2an	$⊢ ((G \in USGraph \land N \in V) \land (y \in A \land w \in A)) \to (E (y) = E (w) \leftrightarrow y = w)$
17	16	bicomd	$⊢ ((G \in USGraph \land N \in V) \land (y \in A \land w \in A)) \to (y = w \leftrightarrow E (y) = E (w))$
18	17	notbid	$⊢ ((G \in USGraph \land N \in V) \land (y \in A \land w \in A)) \to (\neg y = w \leftrightarrow \neg E (y) = E (w))$
19		simpl	$⊢ (G \in USGraph \land N \in V) \to G \in USGraph$
20		simpl	$⊢ (y \in A \land w \in A) \to y \in A$
21	19 20	anim12i	$⊢ ((G \in USGraph \land N \in V) \land (y \in A \land w \in A)) \to (G \in USGraph \land y \in A)$
22		preq1	$⊢ u = z \to \{u, N\} = \{z, N\}$
23	22	eqeq2d	$⊢ u = z \to (E (y) = \{u, N\} \leftrightarrow E (y) = \{z, N\})$
24	23	cbvriotavw	$⊢ (ι u \in V \| E (y) = \{u, N\}) = (ι z \in V \| E (y) = \{z, N\})$
25	1 2 3	usgredg2vlem2	$⊢ (G \in USGraph \land y \in A) \to ((ι u \in V \| E (y) = \{u, N\}) = (ι z \in V \| E (y) = \{z, N\}) \to E (y) = \{(ι u \in V \| E (y) = \{u, N\}), N\})$
26	21 24 25	mpisyl	$⊢ ((G \in USGraph \land N \in V) \land (y \in A \land w \in A)) \to E (y) = \{(ι u \in V \| E (y) = \{u, N\}), N\}$
27		an3	$⊢ ((G \in USGraph \land N \in V) \land (y \in A \land w \in A)) \to (G \in USGraph \land w \in A)$
28	22	eqeq2d	$⊢ u = z \to (E (w) = \{u, N\} \leftrightarrow E (w) = \{z, N\})$
29	28	cbvriotavw	$⊢ (ι u \in V \| E (w) = \{u, N\}) = (ι z \in V \| E (w) = \{z, N\})$
30	1 2 3	usgredg2vlem2	$⊢ (G \in USGraph \land w \in A) \to ((ι u \in V \| E (w) = \{u, N\}) = (ι z \in V \| E (w) = \{z, N\}) \to E (w) = \{(ι u \in V \| E (w) = \{u, N\}), N\})$
31	27 29 30	mpisyl	$⊢ ((G \in USGraph \land N \in V) \land (y \in A \land w \in A)) \to E (w) = \{(ι u \in V \| E (w) = \{u, N\}), N\}$
32	26 31	eqeq12d	$⊢ ((G \in USGraph \land N \in V) \land (y \in A \land w \in A)) \to (E (y) = E (w) \leftrightarrow \{(ι u \in V \| E (y) = \{u, N\}), N\} = \{(ι u \in V \| E (w) = \{u, N\}), N\})$
33	32	notbid	$⊢ ((G \in USGraph \land N \in V) \land (y \in A \land w \in A)) \to (\neg E (y) = E (w) \leftrightarrow \neg \{(ι u \in V \| E (y) = \{u, N\}), N\} = \{(ι u \in V \| E (w) = \{u, N\}), N\})$
34		riotaex	$⊢ (ι u \in V \| E (y) = \{u, N\}) \in V$
35	34	a1i	$⊢ N \in V \to (ι u \in V \| E (y) = \{u, N\}) \in V$
36		id	$⊢ N \in V \to N \in V$
37		riotaex	$⊢ (ι u \in V \| E (w) = \{u, N\}) \in V$
38	37	a1i	$⊢ N \in V \to (ι u \in V \| E (w) = \{u, N\}) \in V$
39		preq12bg	$⊢ (((ι u \in V \| E (y) = \{u, N\}) \in V \land N \in V) \land ((ι u \in V \| E (w) = \{u, N\}) \in V \land N \in V)) \to (\{(ι u \in V \| E (y) = \{u, N\}), N\} = \{(ι u \in V \| E (w) = \{u, N\}), N\} \leftrightarrow (((ι u \in V \| E (y) = \{u, N\}) = (ι u \in V \| E (w) = \{u, N\}) \land N = N) \lor ((ι u \in V \| E (y) = \{u, N\}) = N \land N = (ι u \in V \| E (w) = \{u, N\}))))$
40	35 36 38 36 39	syl22anc	$⊢ N \in V \to (\{(ι u \in V \| E (y) = \{u, N\}), N\} = \{(ι u \in V \| E (w) = \{u, N\}), N\} \leftrightarrow (((ι u \in V \| E (y) = \{u, N\}) = (ι u \in V \| E (w) = \{u, N\}) \land N = N) \lor ((ι u \in V \| E (y) = \{u, N\}) = N \land N = (ι u \in V \| E (w) = \{u, N\}))))$
41	40	notbid	$⊢ N \in V \to (\neg \{(ι u \in V \| E (y) = \{u, N\}), N\} = \{(ι u \in V \| E (w) = \{u, N\}), N\} \leftrightarrow \neg (((ι u \in V \| E (y) = \{u, N\}) = (ι u \in V \| E (w) = \{u, N\}) \land N = N) \lor ((ι u \in V \| E (y) = \{u, N\}) = N \land N = (ι u \in V \| E (w) = \{u, N\}))))$
42	41	adantl	$⊢ (G \in USGraph \land N \in V) \to (\neg \{(ι u \in V \| E (y) = \{u, N\}), N\} = \{(ι u \in V \| E (w) = \{u, N\}), N\} \leftrightarrow \neg (((ι u \in V \| E (y) = \{u, N\}) = (ι u \in V \| E (w) = \{u, N\}) \land N = N) \lor ((ι u \in V \| E (y) = \{u, N\}) = N \land N = (ι u \in V \| E (w) = \{u, N\}))))$
43		ioran	$⊢ \neg (((ι u \in V \| E (y) = \{u, N\}) = (ι u \in V \| E (w) = \{u, N\}) \land N = N) \lor ((ι u \in V \| E (y) = \{u, N\}) = N \land N = (ι u \in V \| E (w) = \{u, N\}))) \leftrightarrow (\neg ((ι u \in V \| E (y) = \{u, N\}) = (ι u \in V \| E (w) = \{u, N\}) \land N = N) \land \neg ((ι u \in V \| E (y) = \{u, N\}) = N \land N = (ι u \in V \| E (w) = \{u, N\})))$
44		ianor	$⊢ \neg ((ι u \in V \| E (y) = \{u, N\}) = (ι u \in V \| E (w) = \{u, N\}) \land N = N) \leftrightarrow (\neg (ι u \in V \| E (y) = \{u, N\}) = (ι u \in V \| E (w) = \{u, N\}) \lor \neg N = N)$
45	24 29	eqeq12i	$⊢ (ι u \in V \| E (y) = \{u, N\}) = (ι u \in V \| E (w) = \{u, N\}) \leftrightarrow (ι z \in V \| E (y) = \{z, N\}) = (ι z \in V \| E (w) = \{z, N\})$
46	45	notbii	$⊢ \neg (ι u \in V \| E (y) = \{u, N\}) = (ι u \in V \| E (w) = \{u, N\}) \leftrightarrow \neg (ι z \in V \| E (y) = \{z, N\}) = (ι z \in V \| E (w) = \{z, N\})$
47	46	biimpi	$⊢ \neg (ι u \in V \| E (y) = \{u, N\}) = (ι u \in V \| E (w) = \{u, N\}) \to \neg (ι z \in V \| E (y) = \{z, N\}) = (ι z \in V \| E (w) = \{z, N\})$
48	47	a1d	$⊢ \neg (ι u \in V \| E (y) = \{u, N\}) = (ι u \in V \| E (w) = \{u, N\}) \to (G \in USGraph \to \neg (ι z \in V \| E (y) = \{z, N\}) = (ι z \in V \| E (w) = \{z, N\}))$
49		eqid	$⊢ N = N$
50	49	pm2.24i	$⊢ \neg N = N \to (G \in USGraph \to \neg (ι z \in V \| E (y) = \{z, N\}) = (ι z \in V \| E (w) = \{z, N\}))$
51	48 50	jaoi	$⊢ (\neg (ι u \in V \| E (y) = \{u, N\}) = (ι u \in V \| E (w) = \{u, N\}) \lor \neg N = N) \to (G \in USGraph \to \neg (ι z \in V \| E (y) = \{z, N\}) = (ι z \in V \| E (w) = \{z, N\}))$
52	44 51	sylbi	$⊢ \neg ((ι u \in V \| E (y) = \{u, N\}) = (ι u \in V \| E (w) = \{u, N\}) \land N = N) \to (G \in USGraph \to \neg (ι z \in V \| E (y) = \{z, N\}) = (ι z \in V \| E (w) = \{z, N\}))$
53	52	adantr	$⊢ (\neg ((ι u \in V \| E (y) = \{u, N\}) = (ι u \in V \| E (w) = \{u, N\}) \land N = N) \land \neg ((ι u \in V \| E (y) = \{u, N\}) = N \land N = (ι u \in V \| E (w) = \{u, N\}))) \to (G \in USGraph \to \neg (ι z \in V \| E (y) = \{z, N\}) = (ι z \in V \| E (w) = \{z, N\}))$
54	43 53	sylbi	$⊢ \neg (((ι u \in V \| E (y) = \{u, N\}) = (ι u \in V \| E (w) = \{u, N\}) \land N = N) \lor ((ι u \in V \| E (y) = \{u, N\}) = N \land N = (ι u \in V \| E (w) = \{u, N\}))) \to (G \in USGraph \to \neg (ι z \in V \| E (y) = \{z, N\}) = (ι z \in V \| E (w) = \{z, N\}))$
55	54	com12	$⊢ G \in USGraph \to (\neg (((ι u \in V \| E (y) = \{u, N\}) = (ι u \in V \| E (w) = \{u, N\}) \land N = N) \lor ((ι u \in V \| E (y) = \{u, N\}) = N \land N = (ι u \in V \| E (w) = \{u, N\}))) \to \neg (ι z \in V \| E (y) = \{z, N\}) = (ι z \in V \| E (w) = \{z, N\}))$
56	55	adantr	$⊢ (G \in USGraph \land N \in V) \to (\neg (((ι u \in V \| E (y) = \{u, N\}) = (ι u \in V \| E (w) = \{u, N\}) \land N = N) \lor ((ι u \in V \| E (y) = \{u, N\}) = N \land N = (ι u \in V \| E (w) = \{u, N\}))) \to \neg (ι z \in V \| E (y) = \{z, N\}) = (ι z \in V \| E (w) = \{z, N\}))$
57	42 56	sylbid	$⊢ (G \in USGraph \land N \in V) \to (\neg \{(ι u \in V \| E (y) = \{u, N\}), N\} = \{(ι u \in V \| E (w) = \{u, N\}), N\} \to \neg (ι z \in V \| E (y) = \{z, N\}) = (ι z \in V \| E (w) = \{z, N\}))$
58	57	adantr	$⊢ ((G \in USGraph \land N \in V) \land (y \in A \land w \in A)) \to (\neg \{(ι u \in V \| E (y) = \{u, N\}), N\} = \{(ι u \in V \| E (w) = \{u, N\}), N\} \to \neg (ι z \in V \| E (y) = \{z, N\}) = (ι z \in V \| E (w) = \{z, N\}))$
59	33 58	sylbid	$⊢ ((G \in USGraph \land N \in V) \land (y \in A \land w \in A)) \to (\neg E (y) = E (w) \to \neg (ι z \in V \| E (y) = \{z, N\}) = (ι z \in V \| E (w) = \{z, N\}))$
60	18 59	sylbid	$⊢ ((G \in USGraph \land N \in V) \land (y \in A \land w \in A)) \to (\neg y = w \to \neg (ι z \in V \| E (y) = \{z, N\}) = (ι z \in V \| E (w) = \{z, N\}))$
61	60	con4d	$⊢ ((G \in USGraph \land N \in V) \land (y \in A \land w \in A)) \to ((ι z \in V \| E (y) = \{z, N\}) = (ι z \in V \| E (w) = \{z, N\}) \to y = w)$
62	61	ralrimivva	$⊢ (G \in USGraph \land N \in V) \to \forall y \in A \forall w \in A ((ι z \in V \| E (y) = \{z, N\}) = (ι z \in V \| E (w) = \{z, N\}) \to y = w)$
63		fveqeq2	$⊢ y = w \to (E (y) = \{z, N\} \leftrightarrow E (w) = \{z, N\})$
64	63	riotabidv	$⊢ y = w \to (ι z \in V \| E (y) = \{z, N\}) = (ι z \in V \| E (w) = \{z, N\})$
65	4 64	f1mpt	$⊢ F : A \underset{1-1}{⟶} V \leftrightarrow (\forall y \in A (ι z \in V \| E (y) = \{z, N\}) \in V \land \forall y \in A \forall w \in A ((ι z \in V \| E (y) = \{z, N\}) = (ι z \in V \| E (w) = \{z, N\}) \to y = w))$
66	7 62 65	sylanbrc	$⊢ (G \in USGraph \land N \in V) \to F : A \underset{1-1}{⟶} V$

Metamath Proof Explorer

Theorem usgredg2v

Proof