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 ‘ 𝐺 ) )