Metamath Proof Explorer

Theorem uspgredg2vlem

Description: Lemma for uspgredg2v . (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
Assertion uspgredg2vlem ⊢ G ∈ USHGraph ∧ Y ∈ A → ι z ∈ V | Y = N z ∈ 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 eleq2 ⊢ e = Y → N ∈ e ↔ N ∈ Y
5 4 3 elrab2 ⊢ Y ∈ A ↔ Y ∈ E ∧ N ∈ Y
6 simpl ⊢ G ∈ USHGraph ∧ Y ∈ E ∧ N ∈ Y → G ∈ USHGraph
7 2 eleq2i ⊢ Y ∈ E ↔ Y ∈ Edg ⁡ G
8 7 biimpi ⊢ Y ∈ E → Y ∈ Edg ⁡ G
9 8 ad2antrl ⊢ G ∈ USHGraph ∧ Y ∈ E ∧ N ∈ Y → Y ∈ Edg ⁡ G
10 simprr ⊢ G ∈ USHGraph ∧ Y ∈ E ∧ N ∈ Y → N ∈ Y
11 6 9 10 3jca ⊢ G ∈ USHGraph ∧ Y ∈ E ∧ N ∈ Y → G ∈ USHGraph ∧ Y ∈ Edg ⁡ G ∧ N ∈ Y
12 uspgredg2vtxeu ⊢ G ∈ USHGraph ∧ Y ∈ Edg ⁡ G ∧ N ∈ Y → ∃! z ∈ Vtx ⁡ G Y = N z
13 reueq1 ⊢ V = Vtx ⁡ G → ∃! z ∈ V Y = N z ↔ ∃! z ∈ Vtx ⁡ G Y = N z
14 1 13 ax-mp ⊢ ∃! z ∈ V Y = N z ↔ ∃! z ∈ Vtx ⁡ G Y = N z
15 12 14 sylibr ⊢ G ∈ USHGraph ∧ Y ∈ Edg ⁡ G ∧ N ∈ Y → ∃! z ∈ V Y = N z
16 riotacl ⊢ ∃! z ∈ V Y = N z → ι z ∈ V | Y = N z ∈ V
17 11 15 16 3syl ⊢ G ∈ USHGraph ∧ Y ∈ E ∧ N ∈ Y → ι z ∈ V | Y = N z ∈ V
18 5 17 sylan2b ⊢ G ∈ USHGraph ∧ Y ∈ A → ι z ∈ V | Y = N z ∈ V