Metamath Proof Explorer


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