This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 biimtrid ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑀 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝐸 ∧ 𝑀 ∈ 𝐶 ) ) → ( ∃! 𝑛 ∈ ( Vtx ‘ 𝐺 ) 𝐶 = { 𝑀 , 𝑛 } → ∃! 𝑛 ( { 𝑛 , 𝑀 } ∈ 𝐸 ∧ 𝐶 = { 𝑀 , 𝑛 } ) ) )
32 9 31 mpd ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑀 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝐸 ∧ 𝑀 ∈ 𝐶 ) ) → ∃! 𝑛 ( { 𝑛 , 𝑀 } ∈ 𝐸 ∧ 𝐶 = { 𝑀 , 𝑛 } ) )
33 2 eleq2i ⊢ ( 𝑛 ∈ 𝑁 ↔ 𝑛 ∈ ( 𝐺 NeighbVtx 𝑀 ) )
34 1 nbusgreledg ⊢ ( 𝐺 ∈ USGraph → ( 𝑛 ∈ ( 𝐺 NeighbVtx 𝑀 ) ↔ { 𝑛 , 𝑀 } ∈ 𝐸 ) )
35 33 34 bitrid ⊢ ( 𝐺 ∈ 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 ∧ 𝑀 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝐸 ∧ 𝑀 ∈ 𝐶 ) ) → ∃! 𝑛 ∈ 𝑁 𝐶 = { 𝑀 , 𝑛 } )