Metamath Proof Explorer

Theorem lpvtx

Description: The endpoints of a loop (which is an edge at index J ) are two (identical) vertices A . (Contributed by AV, 1-Feb-2021)

Ref Expression
Hypothesis lpvtx.i ⊢ I = iEdg ⁡ G
Assertion lpvtx ⊢ G ∈ UHGraph ∧ J ∈ dom ⁡ I ∧ I ⁡ J = A → A ∈ Vtx ⁡ G

Proof

Step Hyp Ref Expression
1 lpvtx.i ⊢ I = iEdg ⁡ G
2 simp1 ⊢ G ∈ UHGraph ∧ J ∈ dom ⁡ I ∧ I ⁡ J = A → G ∈ UHGraph
3 1 uhgrfun ⊢ G ∈ UHGraph → Fun ⁡ I
4 3 funfnd ⊢ G ∈ UHGraph → I Fn dom ⁡ I
5 4 3ad2ant1 ⊢ G ∈ UHGraph ∧ J ∈ dom ⁡ I ∧ I ⁡ J = A → I Fn dom ⁡ I
6 simp2 ⊢ G ∈ UHGraph ∧ J ∈ dom ⁡ I ∧ I ⁡ J = A → J ∈ dom ⁡ I
7 1 uhgrn0 ⊢ G ∈ UHGraph ∧ I Fn dom ⁡ I ∧ J ∈ dom ⁡ I → I ⁡ J ≠ ∅
8 2 5 6 7 syl3anc ⊢ G ∈ UHGraph ∧ J ∈ dom ⁡ I ∧ I ⁡ J = A → I ⁡ J ≠ ∅
9 neeq1 ⊢ I ⁡ J = A → I ⁡ J ≠ ∅ ↔ A ≠ ∅
10 9 biimpd ⊢ I ⁡ J = A → I ⁡ J ≠ ∅ → A ≠ ∅
11 10 3ad2ant3 ⊢ G ∈ UHGraph ∧ J ∈ dom ⁡ I ∧ I ⁡ J = A → I ⁡ J ≠ ∅ → A ≠ ∅
12 8 11 mpd ⊢ G ∈ UHGraph ∧ J ∈ dom ⁡ I ∧ I ⁡ J = A → A ≠ ∅
13 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
14 13 1 uhgrss ⊢ G ∈ UHGraph ∧ J ∈ dom ⁡ I → I ⁡ J ⊆ Vtx ⁡ G
15 14 3adant3 ⊢ G ∈ UHGraph ∧ J ∈ dom ⁡ I ∧ I ⁡ J = A → I ⁡ J ⊆ Vtx ⁡ G
16 sseq1 ⊢ I ⁡ J = A → I ⁡ J ⊆ Vtx ⁡ G ↔ A ⊆ Vtx ⁡ G
17 16 3ad2ant3 ⊢ G ∈ UHGraph ∧ J ∈ dom ⁡ I ∧ I ⁡ J = A → I ⁡ J ⊆ Vtx ⁡ G ↔ A ⊆ Vtx ⁡ G
18 15 17 mpbid ⊢ G ∈ UHGraph ∧ J ∈ dom ⁡ I ∧ I ⁡ J = A → A ⊆ Vtx ⁡ G
19 snnzb ⊢ A ∈ V ↔ A ≠ ∅
20 snssg ⊢ A ∈ V → A ∈ Vtx ⁡ G ↔ A ⊆ Vtx ⁡ G
21 19 20 sylbir ⊢ A ≠ ∅ → A ∈ Vtx ⁡ G ↔ A ⊆ Vtx ⁡ G
22 18 21 syl5ibrcom ⊢ G ∈ UHGraph ∧ J ∈ dom ⁡ I ∧ I ⁡ J = A → A ≠ ∅ → A ∈ Vtx ⁡ G
23 12 22 mpd ⊢ G ∈ UHGraph ∧ J ∈ dom ⁡ I ∧ I ⁡ J = A → A ∈ Vtx ⁡ G