This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
Assertion lpvtx ( ( 𝐺 ∈ UHGraph ∧ 𝐽 ∈ dom 𝐼 ∧ ( 𝐼 ‘ 𝐽 ) = { 𝐴 } ) → 𝐴 ∈ ( Vtx ‘ 𝐺 ) )

Proof

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