Metamath Proof Explorer

Theorem uspgredg2vtxeu

Description: For a vertex incident to an edge there is exactly one other vertex incident to the edge in a simple pseudograph. (Contributed by AV, 18-Oct-2020) (Revised by AV, 6-Dec-2020)

Ref Expression
Assertion uspgredg2vtxeu ⊢ G ∈ USHGraph ∧ E ∈ Edg ⁡ G ∧ Y ∈ E → ∃! y ∈ Vtx ⁡ G E = Y y

Proof

Step Hyp Ref Expression
1 uspgrupgr ⊢ G ∈ USHGraph → G ∈ UPGraph
2 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
3 eqid ⊢ Edg ⁡ G = Edg ⁡ G
4 2 3 upgredg2vtx ⊢ G ∈ UPGraph ∧ E ∈ Edg ⁡ G ∧ Y ∈ E → ∃ y ∈ Vtx ⁡ G E = Y y
5 1 4 syl3an1 ⊢ G ∈ USHGraph ∧ E ∈ Edg ⁡ G ∧ Y ∈ E → ∃ y ∈ Vtx ⁡ G E = Y y
6 eqtr2 ⊢ E = Y y ∧ E = Y x → Y y = Y x
7 vex ⊢ y ∈ V
8 vex ⊢ x ∈ V
9 7 8 preqr2 ⊢ Y y = Y x → y = x
10 6 9 syl ⊢ E = Y y ∧ E = Y x → y = x
11 10 a1i ⊢ G ∈ USHGraph ∧ E ∈ Edg ⁡ G ∧ Y ∈ E ∧ y ∈ Vtx ⁡ G ∧ x ∈ Vtx ⁡ G → E = Y y ∧ E = Y x → y = x
12 11 ralrimivva ⊢ G ∈ USHGraph ∧ E ∈ Edg ⁡ G ∧ Y ∈ E → ∀ y ∈ Vtx ⁡ G ∀ x ∈ Vtx ⁡ G E = Y y ∧ E = Y x → y = x
13 preq2 ⊢ y = x → Y y = Y x
14 13 eqeq2d ⊢ y = x → E = Y y ↔ E = Y x
15 14 reu4 ⊢ ∃! y ∈ Vtx ⁡ G E = Y y ↔ ∃ y ∈ Vtx ⁡ G E = Y y ∧ ∀ y ∈ Vtx ⁡ G ∀ x ∈ Vtx ⁡ G E = Y y ∧ E = Y x → y = x
16 5 12 15 sylanbrc ⊢ G ∈ USHGraph ∧ E ∈ Edg ⁡ G ∧ Y ∈ E → ∃! y ∈ Vtx ⁡ G E = Y y