Metamath Proof Explorer

Theorem edgnbusgreu

Description: For each edge incident to a vertex there is exactly one neighbor of the vertex also incident to this edge in a simple graph. (Contributed by AV, 28-Oct-2020) (Revised by AV, 6-Jul-2022)

Ref Expression
Hypotheses edgnbusgreu.e 
|- E = ( Edg ` G )
edgnbusgreu.n 
|- N = ( G NeighbVtx M )
Assertion edgnbusgreu 
|- ( ( ( G e. USGraph /\ M e. V ) /\ ( C e. E /\ M e. C ) ) -> E! n e. N C = { M , n } )

Proof

Step Hyp Ref Expression
1 edgnbusgreu.e 
 |-  E = ( Edg ` G )
2 edgnbusgreu.n 
 |-  N = ( G NeighbVtx M )
3 simpll 
 |-  ( ( ( G e. USGraph /\ M e. V ) /\ ( C e. E /\ M e. C ) ) -> G e. USGraph )
4 1 eleq2i 
 |-  ( C e. E <-> C e. ( Edg ` G ) )
5 4 biimpi 
 |-  ( C e. E -> C e. ( Edg ` G ) )
6 5 ad2antrl 
 |-  ( ( ( G e. USGraph /\ M e. V ) /\ ( C e. E /\ M e. C ) ) -> C e. ( Edg ` G ) )
7 simprr 
 |-  ( ( ( G e. USGraph /\ M e. V ) /\ ( C e. E /\ M e. C ) ) -> M e. C )
8 usgredg2vtxeu 
 |-  ( ( G e. USGraph /\ C e. ( Edg ` G ) /\ M e. C ) -> E! n e. ( Vtx ` G ) C = { M , n } )
9 3 6 7 8 syl3anc 
 |-  ( ( ( G e. USGraph /\ M e. V ) /\ ( C e. E /\ M e. C ) ) -> E! n e. ( Vtx ` G ) C = { M , n } )
10 df-reu 
 |-  ( E! n e. ( Vtx ` G ) C = { M , n } <-> E! n ( n e. ( Vtx ` G ) /\ C = { M , n } ) )
11 prcom 
 |-  { M , n } = { n , M }
12 11 eqeq2i 
 |-  ( C = { M , n } <-> C = { n , M } )
13 12 biimpi 
 |-  ( C = { M , n } -> C = { n , M } )
14 13 eleq1d 
 |-  ( C = { M , n } -> ( C e. E <-> { n , M } e. E ) )
15 14 biimpcd 
 |-  ( C e. E -> ( C = { M , n } -> { n , M } e. E ) )
16 15 ad2antrl 
 |-  ( ( ( G e. USGraph /\ M e. V ) /\ ( C e. E /\ M e. C ) ) -> ( C = { M , n } -> { n , M } e. E ) )
17 16 adantld 
 |-  ( ( ( G e. USGraph /\ M e. V ) /\ ( C e. E /\ M e. C ) ) -> ( ( n e. ( Vtx ` G ) /\ C = { M , n } ) -> { n , M } e. E ) )
18 17 imp 
 |-  ( ( ( ( G e. USGraph /\ M e. V ) /\ ( C e. E /\ M e. C ) ) /\ ( n e. ( Vtx ` G ) /\ C = { M , n } ) ) -> { n , M } e. E )
19 simprr 
 |-  ( ( ( ( G e. USGraph /\ M e. V ) /\ ( C e. E /\ M e. C ) ) /\ ( n e. ( Vtx ` G ) /\ C = { M , n } ) ) -> C = { M , n } )
20 18 19 jca 
 |-  ( ( ( ( G e. USGraph /\ M e. V ) /\ ( C e. E /\ M e. C ) ) /\ ( n e. ( Vtx ` G ) /\ C = { M , n } ) ) -> ( { n , M } e. E /\ C = { M , n } ) )
21 simpl 
 |-  ( ( { n , M } e. E /\ C = { M , n } ) -> { n , M } e. E )
22 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
23 1 22 usgrpredgv 
 |-  ( ( G e. USGraph /\ { n , M } e. E ) -> ( n e. ( Vtx ` G ) /\ M e. ( Vtx ` G ) ) )
24 23 simpld 
 |-  ( ( G e. USGraph /\ { n , M } e. E ) -> n e. ( Vtx ` G ) )
25 3 21 24 syl2an 
 |-  ( ( ( ( G e. USGraph /\ M e. V ) /\ ( C e. E /\ M e. C ) ) /\ ( { n , M } e. E /\ C = { M , n } ) ) -> n e. ( Vtx ` G ) )
26 simprr 
 |-  ( ( ( ( G e. USGraph /\ M e. V ) /\ ( C e. E /\ M e. C ) ) /\ ( { n , M } e. E /\ C = { M , n } ) ) -> C = { M , n } )
27 25 26 jca 
 |-  ( ( ( ( G e. USGraph /\ M e. V ) /\ ( C e. E /\ M e. C ) ) /\ ( { n , M } e. E /\ C = { M , n } ) ) -> ( n e. ( Vtx ` G ) /\ C = { M , n } ) )
28 20 27 impbida 
 |-  ( ( ( G e. USGraph /\ M e. V ) /\ ( C e. E /\ M e. C ) ) -> ( ( n e. ( Vtx ` G ) /\ C = { M , n } ) <-> ( { n , M } e. E /\ C = { M , n } ) ) )
29 28 eubidv 
 |-  ( ( ( G e. USGraph /\ M e. V ) /\ ( C e. E /\ M e. C ) ) -> ( E! n ( n e. ( Vtx ` G ) /\ C = { M , n } ) <-> E! n ( { n , M } e. E /\ C = { M , n } ) ) )
30 29 biimpd 
 |-  ( ( ( G e. USGraph /\ M e. V ) /\ ( C e. E /\ M e. C ) ) -> ( E! n ( n e. ( Vtx ` G ) /\ C = { M , n } ) -> E! n ( { n , M } e. E /\ C = { M , n } ) ) )
31 10 30 biimtrid 
 |-  ( ( ( G e. USGraph /\ M e. V ) /\ ( C e. E /\ M e. C ) ) -> ( E! n e. ( Vtx ` G ) C = { M , n } -> E! n ( { n , M } e. E /\ C = { M , n } ) ) )
32 9 31 mpd 
 |-  ( ( ( G e. USGraph /\ M e. V ) /\ ( C e. E /\ M e. C ) ) -> E! n ( { n , M } e. E /\ C = { M , n } ) )
33 2 eleq2i 
 |-  ( n e. N <-> n e. ( G NeighbVtx M ) )
34 1 nbusgreledg 
 |-  ( G e. USGraph -> ( n e. ( G NeighbVtx M ) <-> { n , M } e. E ) )
35 33 34 bitrid 
 |-  ( G e. USGraph -> ( n e. N <-> { n , M } e. E ) )
36 35 anbi1d 
 |-  ( G e. USGraph -> ( ( n e. N /\ C = { M , n } ) <-> ( { n , M } e. E /\ C = { M , n } ) ) )
37 36 ad2antrr 
 |-  ( ( ( G e. USGraph /\ M e. V ) /\ ( C e. E /\ M e. C ) ) -> ( ( n e. N /\ C = { M , n } ) <-> ( { n , M } e. E /\ C = { M , n } ) ) )
38 37 eubidv 
 |-  ( ( ( G e. USGraph /\ M e. V ) /\ ( C e. E /\ M e. C ) ) -> ( E! n ( n e. N /\ C = { M , n } ) <-> E! n ( { n , M } e. E /\ C = { M , n } ) ) )
39 32 38 mpbird 
 |-  ( ( ( G e. USGraph /\ M e. V ) /\ ( C e. E /\ M e. C ) ) -> E! n ( n e. N /\ C = { M , n } ) )
40 df-reu 
 |-  ( E! n e. N C = { M , n } <-> E! n ( n e. N /\ C = { M , n } ) )
41 39 40 sylibr 
 |-  ( ( ( G e. USGraph /\ M e. V ) /\ ( C e. E /\ M e. C ) ) -> E! n e. N C = { M , n } )