Metamath Proof Explorer

Theorem 1loopgrnb0

Description: In a graph (simple pseudograph) with one edge which is a loop, the vertex connected with itself by the loop has no neighbors. (Contributed by AV, 17-Dec-2020) (Revised by AV, 21-Feb-2021)

Ref Expression
Hypotheses 1loopgruspgr.v 
|- ( ph -> ( Vtx ` G ) = V )
1loopgruspgr.a 
|- ( ph -> A e. X )
1loopgruspgr.n 
|- ( ph -> N e. V )
1loopgruspgr.i 
|- ( ph -> ( iEdg ` G ) = { <. A , { N } >. } )
Assertion 1loopgrnb0 
|- ( ph -> ( G NeighbVtx N ) = (/) )

Proof

Step Hyp Ref Expression
1 1loopgruspgr.v 
 |-  ( ph -> ( Vtx ` G ) = V )
2 1loopgruspgr.a 
 |-  ( ph -> A e. X )
3 1loopgruspgr.n 
 |-  ( ph -> N e. V )
4 1loopgruspgr.i 
 |-  ( ph -> ( iEdg ` G ) = { <. A , { N } >. } )
5 1 2 3 4 1loopgruspgr 
 |-  ( ph -> G e. USPGraph )
6 uspgrupgr 
 |-  ( G e. USPGraph -> G e. UPGraph )
7 5 6 syl 
 |-  ( ph -> G e. UPGraph )
8 1 eleq2d 
 |-  ( ph -> ( N e. ( Vtx ` G ) <-> N e. V ) )
9 3 8 mpbird 
 |-  ( ph -> N e. ( Vtx ` G ) )
10 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
11 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
12 10 11 nbupgr 
 |-  ( ( G e. UPGraph /\ N e. ( Vtx ` G ) ) -> ( G NeighbVtx N ) = { v e. ( ( Vtx ` G ) \ { N } ) | { N , v } e. ( Edg ` G ) } )
13 7 9 12 syl2anc 
 |-  ( ph -> ( G NeighbVtx N ) = { v e. ( ( Vtx ` G ) \ { N } ) | { N , v } e. ( Edg ` G ) } )
14 1 difeq1d 
 |-  ( ph -> ( ( Vtx ` G ) \ { N } ) = ( V \ { N } ) )
15 14 eleq2d 
 |-  ( ph -> ( v e. ( ( Vtx ` G ) \ { N } ) <-> v e. ( V \ { N } ) ) )
16 eldifsn 
 |-  ( v e. ( V \ { N } ) <-> ( v e. V /\ v =/= N ) )
17 3 adantr 
 |-  ( ( ph /\ v e. V ) -> N e. V )
18 simpr 
 |-  ( ( ph /\ v e. V ) -> v e. V )
19 17 18 preqsnd 
 |-  ( ( ph /\ v e. V ) -> ( { N , v } = { N } <-> ( N = N /\ v = N ) ) )
20 simpr 
 |-  ( ( N = N /\ v = N ) -> v = N )
21 19 20 syl6bi 
 |-  ( ( ph /\ v e. V ) -> ( { N , v } = { N } -> v = N ) )
22 21 necon3ad 
 |-  ( ( ph /\ v e. V ) -> ( v =/= N -> -. { N , v } = { N } ) )
23 22 expimpd 
 |-  ( ph -> ( ( v e. V /\ v =/= N ) -> -. { N , v } = { N } ) )
24 16 23 syl5bi 
 |-  ( ph -> ( v e. ( V \ { N } ) -> -. { N , v } = { N } ) )
25 15 24 sylbid 
 |-  ( ph -> ( v e. ( ( Vtx ` G ) \ { N } ) -> -. { N , v } = { N } ) )
26 25 imp 
 |-  ( ( ph /\ v e. ( ( Vtx ` G ) \ { N } ) ) -> -. { N , v } = { N } )
27 1 2 3 4 1loopgredg 
 |-  ( ph -> ( Edg ` G ) = { { N } } )
28 27 eleq2d 
 |-  ( ph -> ( { N , v } e. ( Edg ` G ) <-> { N , v } e. { { N } } ) )
29 prex 
 |-  { N , v } e. _V
30 29 elsn 
 |-  ( { N , v } e. { { N } } <-> { N , v } = { N } )
31 28 30 bitrdi 
 |-  ( ph -> ( { N , v } e. ( Edg ` G ) <-> { N , v } = { N } ) )
32 31 notbid 
 |-  ( ph -> ( -. { N , v } e. ( Edg ` G ) <-> -. { N , v } = { N } ) )
33 32 adantr 
 |-  ( ( ph /\ v e. ( ( Vtx ` G ) \ { N } ) ) -> ( -. { N , v } e. ( Edg ` G ) <-> -. { N , v } = { N } ) )
34 26 33 mpbird 
 |-  ( ( ph /\ v e. ( ( Vtx ` G ) \ { N } ) ) -> -. { N , v } e. ( Edg ` G ) )
35 34 ralrimiva 
 |-  ( ph -> A. v e. ( ( Vtx ` G ) \ { N } ) -. { N , v } e. ( Edg ` G ) )
36 rabeq0 
 |-  ( { v e. ( ( Vtx ` G ) \ { N } ) | { N , v } e. ( Edg ` G ) } = (/) <-> A. v e. ( ( Vtx ` G ) \ { N } ) -. { N , v } e. ( Edg ` G ) )
37 35 36 sylibr 
 |-  ( ph -> { v e. ( ( Vtx ` G ) \ { N } ) | { N , v } e. ( Edg ` G ) } = (/) )
38 13 37 eqtrd 
 |-  ( ph -> ( G NeighbVtx N ) = (/) )