Metamath Proof Explorer

Theorem nbusgrf1o0

Description: The mapping of neighbors of a vertex to edges incident to the vertex is a bijection ( 1-1 onto function) in a simple graph. (Contributed by Alexander van der Vekens, 17-Dec-2017) (Revised by AV, 28-Oct-2020)

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 }
nbusgrf1o.f 
|- F = ( n e. N |-> { U , n } )
Assertion nbusgrf1o0 
|- ( ( G e. USGraph /\ U e. V ) -> F : N -1-1-onto-> I )

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 nbusgrf1o.f 
 |-  F = ( n e. N |-> { U , n } )
6 3 eleq2i 
 |-  ( n e. N <-> n e. ( G NeighbVtx U ) )
7 2 nbusgreledg 
 |-  ( G e. USGraph -> ( n e. ( G NeighbVtx U ) <-> { n , U } e. E ) )
8 7 adantr 
 |-  ( ( G e. USGraph /\ U e. V ) -> ( n e. ( G NeighbVtx U ) <-> { n , U } e. E ) )
9 prcom 
 |-  { n , U } = { U , n }
10 9 eleq1i 
 |-  ( { n , U } e. E <-> { U , n } e. E )
11 10 biimpi 
 |-  ( { n , U } e. E -> { U , n } e. E )
12 11 adantl 
 |-  ( ( ( G e. USGraph /\ U e. V ) /\ { n , U } e. E ) -> { U , n } e. E )
13 prid1g 
 |-  ( U e. V -> U e. { U , n } )
14 13 adantl 
 |-  ( ( G e. USGraph /\ U e. V ) -> U e. { U , n } )
15 14 adantr 
 |-  ( ( ( G e. USGraph /\ U e. V ) /\ { n , U } e. E ) -> U e. { U , n } )
16 eleq2 
 |-  ( e = { U , n } -> ( U e. e <-> U e. { U , n } ) )
17 16 4 elrab2 
 |-  ( { U , n } e. I <-> ( { U , n } e. E /\ U e. { U , n } ) )
18 12 15 17 sylanbrc 
 |-  ( ( ( G e. USGraph /\ U e. V ) /\ { n , U } e. E ) -> { U , n } e. I )
19 18 ex 
 |-  ( ( G e. USGraph /\ U e. V ) -> ( { n , U } e. E -> { U , n } e. I ) )
20 8 19 sylbid 
 |-  ( ( G e. USGraph /\ U e. V ) -> ( n e. ( G NeighbVtx U ) -> { U , n } e. I ) )
21 6 20 syl5bi 
 |-  ( ( G e. USGraph /\ U e. V ) -> ( n e. N -> { U , n } e. I ) )
22 21 ralrimiv 
 |-  ( ( G e. USGraph /\ U e. V ) -> A. n e. N { U , n } e. I )
23 4 rabeq2i 
 |-  ( e e. I <-> ( e e. E /\ U e. e ) )
24 2 3 edgnbusgreu 
 |-  ( ( ( G e. USGraph /\ U e. V ) /\ ( e e. E /\ U e. e ) ) -> E! n e. N e = { U , n } )
25 23 24 sylan2b 
 |-  ( ( ( G e. USGraph /\ U e. V ) /\ e e. I ) -> E! n e. N e = { U , n } )
26 25 ralrimiva 
 |-  ( ( G e. USGraph /\ U e. V ) -> A. e e. I E! n e. N e = { U , n } )
27 5 f1ompt 
 |-  ( F : N -1-1-onto-> I <-> ( A. n e. N { U , n } e. I /\ A. e e. I E! n e. N e = { U , n } ) )
28 22 26 27 sylanbrc 
 |-  ( ( G e. USGraph /\ U e. V ) -> F : N -1-1-onto-> I )