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 ∧ 𝑀 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝐸 ∧ 𝑀 ∈ 𝐶 ) ) → ∃! 𝑛 ∈ 𝑁 𝐶 = { 𝑀 , 𝑛 } )