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 e. UHGraph /\ J e. dom I /\ ( I ` J ) = { A } ) -> A e. ( Vtx ` G ) )

Proof

Step Hyp Ref Expression
1 lpvtx.i 
 |-  I = ( iEdg ` G )
2 simp1 
 |-  ( ( G e. UHGraph /\ J e. dom I /\ ( I ` J ) = { A } ) -> G e. UHGraph )
3 1 uhgrfun 
 |-  ( G e. UHGraph -> Fun I )
4 3 funfnd 
 |-  ( G e. UHGraph -> I Fn dom I )
5 4 3ad2ant1 
 |-  ( ( G e. UHGraph /\ J e. dom I /\ ( I ` J ) = { A } ) -> I Fn dom I )
6 simp2 
 |-  ( ( G e. UHGraph /\ J e. dom I /\ ( I ` J ) = { A } ) -> J e. dom I )
7 1 uhgrn0 
 |-  ( ( G e. UHGraph /\ I Fn dom I /\ J e. dom I ) -> ( I ` J ) =/= (/) )
8 2 5 6 7 syl3anc 
 |-  ( ( G e. UHGraph /\ J e. 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 e. UHGraph /\ J e. dom I /\ ( I ` J ) = { A } ) -> ( ( I ` J ) =/= (/) -> { A } =/= (/) ) )
12 8 11 mpd 
 |-  ( ( G e. UHGraph /\ J e. dom I /\ ( I ` J ) = { A } ) -> { A } =/= (/) )
13 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
14 13 1 uhgrss 
 |-  ( ( G e. UHGraph /\ J e. dom I ) -> ( I ` J ) C_ ( Vtx ` G ) )
15 14 3adant3 
 |-  ( ( G e. UHGraph /\ J e. dom I /\ ( I ` J ) = { A } ) -> ( I ` J ) C_ ( Vtx ` G ) )
16 sseq1 
 |-  ( ( I ` J ) = { A } -> ( ( I ` J ) C_ ( Vtx ` G ) <-> { A } C_ ( Vtx ` G ) ) )
17 16 3ad2ant3 
 |-  ( ( G e. UHGraph /\ J e. dom I /\ ( I ` J ) = { A } ) -> ( ( I ` J ) C_ ( Vtx ` G ) <-> { A } C_ ( Vtx ` G ) ) )
18 15 17 mpbid 
 |-  ( ( G e. UHGraph /\ J e. dom I /\ ( I ` J ) = { A } ) -> { A } C_ ( Vtx ` G ) )
19 snnzb 
 |-  ( A e. _V <-> { A } =/= (/) )
20 snssg 
 |-  ( A e. _V -> ( A e. ( Vtx ` G ) <-> { A } C_ ( Vtx ` G ) ) )
21 19 20 sylbir 
 |-  ( { A } =/= (/) -> ( A e. ( Vtx ` G ) <-> { A } C_ ( Vtx ` G ) ) )
22 18 21 syl5ibrcom 
 |-  ( ( G e. UHGraph /\ J e. dom I /\ ( I ` J ) = { A } ) -> ( { A } =/= (/) -> A e. ( Vtx ` G ) ) )
23 12 22 mpd 
 |-  ( ( G e. UHGraph /\ J e. dom I /\ ( I ` J ) = { A } ) -> A e. ( Vtx ` G ) )