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 𝐸 = ( Edg ‘ 𝐺 )
edgnbusgreu.n 𝑁 = ( 𝐺 NeighbVtx 𝑀 )
Assertion edgnbusgreu ( ( ( 𝐺 ∈ USGraph ∧ 𝑀𝑉 ) ∧ ( 𝐶𝐸𝑀𝐶 ) ) → ∃! 𝑛𝑁 𝐶 = { 𝑀 , 𝑛 } )

Proof

Step Hyp Ref Expression
1 edgnbusgreu.e 𝐸 = ( Edg ‘ 𝐺 )
2 edgnbusgreu.n 𝑁 = ( 𝐺 NeighbVtx 𝑀 )
3 simpll ( ( ( 𝐺 ∈ USGraph ∧ 𝑀𝑉 ) ∧ ( 𝐶𝐸𝑀𝐶 ) ) → 𝐺 ∈ USGraph )
4 1 eleq2i ( 𝐶𝐸𝐶 ∈ ( Edg ‘ 𝐺 ) )
5 4 biimpi ( 𝐶𝐸𝐶 ∈ ( Edg ‘ 𝐺 ) )
6 5 ad2antrl ( ( ( 𝐺 ∈ USGraph ∧ 𝑀𝑉 ) ∧ ( 𝐶𝐸𝑀𝐶 ) ) → 𝐶 ∈ ( Edg ‘ 𝐺 ) )
7 simprr ( ( ( 𝐺 ∈ USGraph ∧ 𝑀𝑉 ) ∧ ( 𝐶𝐸𝑀𝐶 ) ) → 𝑀𝐶 )
8 usgredg2vtxeu ( ( 𝐺 ∈ USGraph ∧ 𝐶 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑀𝐶 ) → ∃! 𝑛 ∈ ( Vtx ‘ 𝐺 ) 𝐶 = { 𝑀 , 𝑛 } )
9 3 6 7 8 syl3anc ( ( ( 𝐺 ∈ USGraph ∧ 𝑀𝑉 ) ∧ ( 𝐶𝐸𝑀𝐶 ) ) → ∃! 𝑛 ∈ ( Vtx ‘ 𝐺 ) 𝐶 = { 𝑀 , 𝑛 } )
10 df-reu ( ∃! 𝑛 ∈ ( Vtx ‘ 𝐺 ) 𝐶 = { 𝑀 , 𝑛 } ↔ ∃! 𝑛 ( 𝑛 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 = { 𝑀 , 𝑛 } ) )
11 prcom { 𝑀 , 𝑛 } = { 𝑛 , 𝑀 }
12 11 eqeq2i ( 𝐶 = { 𝑀 , 𝑛 } ↔ 𝐶 = { 𝑛 , 𝑀 } )
13 12 biimpi ( 𝐶 = { 𝑀 , 𝑛 } → 𝐶 = { 𝑛 , 𝑀 } )
14 13 eleq1d ( 𝐶 = { 𝑀 , 𝑛 } → ( 𝐶𝐸 ↔ { 𝑛 , 𝑀 } ∈ 𝐸 ) )
15 14 biimpcd ( 𝐶𝐸 → ( 𝐶 = { 𝑀 , 𝑛 } → { 𝑛 , 𝑀 } ∈ 𝐸 ) )
16 15 ad2antrl ( ( ( 𝐺 ∈ USGraph ∧ 𝑀𝑉 ) ∧ ( 𝐶𝐸𝑀𝐶 ) ) → ( 𝐶 = { 𝑀 , 𝑛 } → { 𝑛 , 𝑀 } ∈ 𝐸 ) )
17 16 adantld ( ( ( 𝐺 ∈ USGraph ∧ 𝑀𝑉 ) ∧ ( 𝐶𝐸𝑀𝐶 ) ) → ( ( 𝑛 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 = { 𝑀 , 𝑛 } ) → { 𝑛 , 𝑀 } ∈ 𝐸 ) )
18 17 imp ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑀𝑉 ) ∧ ( 𝐶𝐸𝑀𝐶 ) ) ∧ ( 𝑛 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 = { 𝑀 , 𝑛 } ) ) → { 𝑛 , 𝑀 } ∈ 𝐸 )
19 simprr ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑀𝑉 ) ∧ ( 𝐶𝐸𝑀𝐶 ) ) ∧ ( 𝑛 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 = { 𝑀 , 𝑛 } ) ) → 𝐶 = { 𝑀 , 𝑛 } )
20 18 19 jca ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑀𝑉 ) ∧ ( 𝐶𝐸𝑀𝐶 ) ) ∧ ( 𝑛 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 = { 𝑀 , 𝑛 } ) ) → ( { 𝑛 , 𝑀 } ∈ 𝐸𝐶 = { 𝑀 , 𝑛 } ) )
21 simpl ( ( { 𝑛 , 𝑀 } ∈ 𝐸𝐶 = { 𝑀 , 𝑛 } ) → { 𝑛 , 𝑀 } ∈ 𝐸 )
22 eqid ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
23 1 22 usgrpredgv ( ( 𝐺 ∈ USGraph ∧ { 𝑛 , 𝑀 } ∈ 𝐸 ) → ( 𝑛 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑀 ∈ ( Vtx ‘ 𝐺 ) ) )
24 23 simpld ( ( 𝐺 ∈ USGraph ∧ { 𝑛 , 𝑀 } ∈ 𝐸 ) → 𝑛 ∈ ( Vtx ‘ 𝐺 ) )
25 3 21 24 syl2an ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑀𝑉 ) ∧ ( 𝐶𝐸𝑀𝐶 ) ) ∧ ( { 𝑛 , 𝑀 } ∈ 𝐸𝐶 = { 𝑀 , 𝑛 } ) ) → 𝑛 ∈ ( Vtx ‘ 𝐺 ) )
26 simprr ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑀𝑉 ) ∧ ( 𝐶𝐸𝑀𝐶 ) ) ∧ ( { 𝑛 , 𝑀 } ∈ 𝐸𝐶 = { 𝑀 , 𝑛 } ) ) → 𝐶 = { 𝑀 , 𝑛 } )
27 25 26 jca ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑀𝑉 ) ∧ ( 𝐶𝐸𝑀𝐶 ) ) ∧ ( { 𝑛 , 𝑀 } ∈ 𝐸𝐶 = { 𝑀 , 𝑛 } ) ) → ( 𝑛 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 = { 𝑀 , 𝑛 } ) )
28 20 27 impbida ( ( ( 𝐺 ∈ USGraph ∧ 𝑀𝑉 ) ∧ ( 𝐶𝐸𝑀𝐶 ) ) → ( ( 𝑛 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 = { 𝑀 , 𝑛 } ) ↔ ( { 𝑛 , 𝑀 } ∈ 𝐸𝐶 = { 𝑀 , 𝑛 } ) ) )
29 28 eubidv ( ( ( 𝐺 ∈ USGraph ∧ 𝑀𝑉 ) ∧ ( 𝐶𝐸𝑀𝐶 ) ) → ( ∃! 𝑛 ( 𝑛 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 = { 𝑀 , 𝑛 } ) ↔ ∃! 𝑛 ( { 𝑛 , 𝑀 } ∈ 𝐸𝐶 = { 𝑀 , 𝑛 } ) ) )
30 29 biimpd ( ( ( 𝐺 ∈ USGraph ∧ 𝑀𝑉 ) ∧ ( 𝐶𝐸𝑀𝐶 ) ) → ( ∃! 𝑛 ( 𝑛 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 = { 𝑀 , 𝑛 } ) → ∃! 𝑛 ( { 𝑛 , 𝑀 } ∈ 𝐸𝐶 = { 𝑀 , 𝑛 } ) ) )
31 10 30 syl5bi ( ( ( 𝐺 ∈ USGraph ∧ 𝑀𝑉 ) ∧ ( 𝐶𝐸𝑀𝐶 ) ) → ( ∃! 𝑛 ∈ ( Vtx ‘ 𝐺 ) 𝐶 = { 𝑀 , 𝑛 } → ∃! 𝑛 ( { 𝑛 , 𝑀 } ∈ 𝐸𝐶 = { 𝑀 , 𝑛 } ) ) )
32 9 31 mpd ( ( ( 𝐺 ∈ USGraph ∧ 𝑀𝑉 ) ∧ ( 𝐶𝐸𝑀𝐶 ) ) → ∃! 𝑛 ( { 𝑛 , 𝑀 } ∈ 𝐸𝐶 = { 𝑀 , 𝑛 } ) )
33 2 eleq2i ( 𝑛𝑁𝑛 ∈ ( 𝐺 NeighbVtx 𝑀 ) )
34 1 nbusgreledg ( 𝐺 ∈ USGraph → ( 𝑛 ∈ ( 𝐺 NeighbVtx 𝑀 ) ↔ { 𝑛 , 𝑀 } ∈ 𝐸 ) )
35 33 34 syl5bb ( 𝐺 ∈ USGraph → ( 𝑛𝑁 ↔ { 𝑛 , 𝑀 } ∈ 𝐸 ) )
36 35 anbi1d ( 𝐺 ∈ USGraph → ( ( 𝑛𝑁𝐶 = { 𝑀 , 𝑛 } ) ↔ ( { 𝑛 , 𝑀 } ∈ 𝐸𝐶 = { 𝑀 , 𝑛 } ) ) )
37 36 ad2antrr ( ( ( 𝐺 ∈ USGraph ∧ 𝑀𝑉 ) ∧ ( 𝐶𝐸𝑀𝐶 ) ) → ( ( 𝑛𝑁𝐶 = { 𝑀 , 𝑛 } ) ↔ ( { 𝑛 , 𝑀 } ∈ 𝐸𝐶 = { 𝑀 , 𝑛 } ) ) )
38 37 eubidv ( ( ( 𝐺 ∈ USGraph ∧ 𝑀𝑉 ) ∧ ( 𝐶𝐸𝑀𝐶 ) ) → ( ∃! 𝑛 ( 𝑛𝑁𝐶 = { 𝑀 , 𝑛 } ) ↔ ∃! 𝑛 ( { 𝑛 , 𝑀 } ∈ 𝐸𝐶 = { 𝑀 , 𝑛 } ) ) )
39 32 38 mpbird ( ( ( 𝐺 ∈ USGraph ∧ 𝑀𝑉 ) ∧ ( 𝐶𝐸𝑀𝐶 ) ) → ∃! 𝑛 ( 𝑛𝑁𝐶 = { 𝑀 , 𝑛 } ) )
40 df-reu ( ∃! 𝑛𝑁 𝐶 = { 𝑀 , 𝑛 } ↔ ∃! 𝑛 ( 𝑛𝑁𝐶 = { 𝑀 , 𝑛 } ) )
41 39 40 sylibr ( ( ( 𝐺 ∈ USGraph ∧ 𝑀𝑉 ) ∧ ( 𝐶𝐸𝑀𝐶 ) ) → ∃! 𝑛𝑁 𝐶 = { 𝑀 , 𝑛 } )