Metamath Proof Explorer

Theorem nbusgredgeu0

Description: For each neighbor of a vertex there is exactly one edge between the vertex and its neighbor in a simple graph. (Contributed by Alexander van der Vekens, 17-Dec-2017) (Revised by AV, 27-Oct-2020) (Proof shortened by AV, 13-Feb-2022)

Ref Expression
Hypotheses nbusgrf1o1.v 
|- V = ( Vtx ` G )
nbusgrf1o1.e 
|- E = ( Edg ` G )
nbusgrf1o1.n 
|- N = ( G NeighbVtx U )
nbusgrf1o1.i 
|- I = { e e. E | U e. e }
Assertion nbusgredgeu0 
|- ( ( ( G e. USGraph /\ U e. V ) /\ M e. N ) -> E! i e. I i = { U , M } )

Proof

Step Hyp Ref Expression
1 nbusgrf1o1.v 
 |-  V = ( Vtx ` G )
2 nbusgrf1o1.e 
 |-  E = ( Edg ` G )
3 nbusgrf1o1.n 
 |-  N = ( G NeighbVtx U )
4 nbusgrf1o1.i 
 |-  I = { e e. E | U e. e }
5 simpll 
 |-  ( ( ( G e. USGraph /\ U e. V ) /\ M e. N ) -> G e. USGraph )
6 3 eleq2i 
 |-  ( M e. N <-> M e. ( G NeighbVtx U ) )
7 nbgrsym 
 |-  ( M e. ( G NeighbVtx U ) <-> U e. ( G NeighbVtx M ) )
8 7 a1i 
 |-  ( ( G e. USGraph /\ U e. V ) -> ( M e. ( G NeighbVtx U ) <-> U e. ( G NeighbVtx M ) ) )
9 8 biimpd 
 |-  ( ( G e. USGraph /\ U e. V ) -> ( M e. ( G NeighbVtx U ) -> U e. ( G NeighbVtx M ) ) )
10 6 9 syl5bi 
 |-  ( ( G e. USGraph /\ U e. V ) -> ( M e. N -> U e. ( G NeighbVtx M ) ) )
11 10 imp 
 |-  ( ( ( G e. USGraph /\ U e. V ) /\ M e. N ) -> U e. ( G NeighbVtx M ) )
12 2 nbusgredgeu 
 |-  ( ( G e. USGraph /\ U e. ( G NeighbVtx M ) ) -> E! i e. E i = { U , M } )
13 5 11 12 syl2anc 
 |-  ( ( ( G e. USGraph /\ U e. V ) /\ M e. N ) -> E! i e. E i = { U , M } )
14 df-reu 
 |-  ( E! i e. E i = { U , M } <-> E! i ( i e. E /\ i = { U , M } ) )
15 13 14 sylib 
 |-  ( ( ( G e. USGraph /\ U e. V ) /\ M e. N ) -> E! i ( i e. E /\ i = { U , M } ) )
16 anass 
 |-  ( ( ( i e. E /\ U e. i ) /\ i = { U , M } ) <-> ( i e. E /\ ( U e. i /\ i = { U , M } ) ) )
17 prid1g 
 |-  ( U e. V -> U e. { U , M } )
18 17 ad2antlr 
 |-  ( ( ( G e. USGraph /\ U e. V ) /\ M e. N ) -> U e. { U , M } )
19 eleq2 
 |-  ( i = { U , M } -> ( U e. i <-> U e. { U , M } ) )
20 18 19 syl5ibrcom 
 |-  ( ( ( G e. USGraph /\ U e. V ) /\ M e. N ) -> ( i = { U , M } -> U e. i ) )
21 20 pm4.71rd 
 |-  ( ( ( G e. USGraph /\ U e. V ) /\ M e. N ) -> ( i = { U , M } <-> ( U e. i /\ i = { U , M } ) ) )
22 21 bicomd 
 |-  ( ( ( G e. USGraph /\ U e. V ) /\ M e. N ) -> ( ( U e. i /\ i = { U , M } ) <-> i = { U , M } ) )
23 22 anbi2d 
 |-  ( ( ( G e. USGraph /\ U e. V ) /\ M e. N ) -> ( ( i e. E /\ ( U e. i /\ i = { U , M } ) ) <-> ( i e. E /\ i = { U , M } ) ) )
24 16 23 syl5bb 
 |-  ( ( ( G e. USGraph /\ U e. V ) /\ M e. N ) -> ( ( ( i e. E /\ U e. i ) /\ i = { U , M } ) <-> ( i e. E /\ i = { U , M } ) ) )
25 24 eubidv 
 |-  ( ( ( G e. USGraph /\ U e. V ) /\ M e. N ) -> ( E! i ( ( i e. E /\ U e. i ) /\ i = { U , M } ) <-> E! i ( i e. E /\ i = { U , M } ) ) )
26 15 25 mpbird 
 |-  ( ( ( G e. USGraph /\ U e. V ) /\ M e. N ) -> E! i ( ( i e. E /\ U e. i ) /\ i = { U , M } ) )
27 df-reu 
 |-  ( E! i e. I i = { U , M } <-> E! i ( i e. I /\ i = { U , M } ) )
28 eleq2 
 |-  ( e = i -> ( U e. e <-> U e. i ) )
29 28 4 elrab2 
 |-  ( i e. I <-> ( i e. E /\ U e. i ) )
30 29 anbi1i 
 |-  ( ( i e. I /\ i = { U , M } ) <-> ( ( i e. E /\ U e. i ) /\ i = { U , M } ) )
31 30 eubii 
 |-  ( E! i ( i e. I /\ i = { U , M } ) <-> E! i ( ( i e. E /\ U e. i ) /\ i = { U , M } ) )
32 27 31 bitri 
 |-  ( E! i e. I i = { U , M } <-> E! i ( ( i e. E /\ U e. i ) /\ i = { U , M } ) )
33 26 32 sylibr 
 |-  ( ( ( G e. USGraph /\ U e. V ) /\ M e. N ) -> E! i e. I i = { U , M } )