Theorem nbusgredgeu0

Description: For each neighbor of a vertex there is exactly one edge between the vertex and its neighbor in a simple graph. (Contributed by Alexander van der Vekens, 17-Dec-2017) (Revised by AV, 27-Oct-2020) (Proof shortened by AV, 13-Feb-2022)

	Ref	Expression
Hypotheses	nbusgrf1o1.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	nbusgrf1o1.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
	nbusgrf1o1.n	⊢ 𝑁 = ( 𝐺 NeighbVtx 𝑈 )
	nbusgrf1o1.i	⊢ 𝐼 = { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 }
Assertion	nbusgredgeu0	⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝑁 ) → ∃! 𝑖 ∈ 𝐼 𝑖 = { 𝑈 , 𝑀 } )

Proof

Step	Hyp	Ref	Expression
1		nbusgrf1o1.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		nbusgrf1o1.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
3		nbusgrf1o1.n	⊢ 𝑁 = ( 𝐺 NeighbVtx 𝑈 )
4		nbusgrf1o1.i	⊢ 𝐼 = { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 }
5		simpll	⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝑁 ) → 𝐺 ∈ USGraph )
6	3	eleq2i	⊢ ( 𝑀 ∈ 𝑁 ↔ 𝑀 ∈ ( 𝐺 NeighbVtx 𝑈 ) )
7		nbgrsym	⊢ ( 𝑀 ∈ ( 𝐺 NeighbVtx 𝑈 ) ↔ 𝑈 ∈ ( 𝐺 NeighbVtx 𝑀 ) )
8	7	a1i	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ( 𝑀 ∈ ( 𝐺 NeighbVtx 𝑈 ) ↔ 𝑈 ∈ ( 𝐺 NeighbVtx 𝑀 ) ) )
9	8	biimpd	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ( 𝑀 ∈ ( 𝐺 NeighbVtx 𝑈 ) → 𝑈 ∈ ( 𝐺 NeighbVtx 𝑀 ) ) )
10	6 9	syl5bi	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ( 𝑀 ∈ 𝑁 → 𝑈 ∈ ( 𝐺 NeighbVtx 𝑀 ) ) )
11	10	imp	⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝑁 ) → 𝑈 ∈ ( 𝐺 NeighbVtx 𝑀 ) )
12	2	nbusgredgeu	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ ( 𝐺 NeighbVtx 𝑀 ) ) → ∃! 𝑖 ∈ 𝐸 𝑖 = { 𝑈 , 𝑀 } )
13	5 11 12	syl2anc	⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝑁 ) → ∃! 𝑖 ∈ 𝐸 𝑖 = { 𝑈 , 𝑀 } )
14		df-reu	⊢ ( ∃! 𝑖 ∈ 𝐸 𝑖 = { 𝑈 , 𝑀 } ↔ ∃! 𝑖 ( 𝑖 ∈ 𝐸 ∧ 𝑖 = { 𝑈 , 𝑀 } ) )
15	13 14	sylib	⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝑁 ) → ∃! 𝑖 ( 𝑖 ∈ 𝐸 ∧ 𝑖 = { 𝑈 , 𝑀 } ) )
16		anass	⊢ ( ( ( 𝑖 ∈ 𝐸 ∧ 𝑈 ∈ 𝑖 ) ∧ 𝑖 = { 𝑈 , 𝑀 } ) ↔ ( 𝑖 ∈ 𝐸 ∧ ( 𝑈 ∈ 𝑖 ∧ 𝑖 = { 𝑈 , 𝑀 } ) ) )
17		prid1g	⊢ ( 𝑈 ∈ 𝑉 → 𝑈 ∈ { 𝑈 , 𝑀 } )
18	17	ad2antlr	⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝑁 ) → 𝑈 ∈ { 𝑈 , 𝑀 } )
19		eleq2	⊢ ( 𝑖 = { 𝑈 , 𝑀 } → ( 𝑈 ∈ 𝑖 ↔ 𝑈 ∈ { 𝑈 , 𝑀 } ) )
20	18 19	syl5ibrcom	⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝑁 ) → ( 𝑖 = { 𝑈 , 𝑀 } → 𝑈 ∈ 𝑖 ) )
21	20	pm4.71rd	⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝑁 ) → ( 𝑖 = { 𝑈 , 𝑀 } ↔ ( 𝑈 ∈ 𝑖 ∧ 𝑖 = { 𝑈 , 𝑀 } ) ) )
22	21	bicomd	⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝑁 ) → ( ( 𝑈 ∈ 𝑖 ∧ 𝑖 = { 𝑈 , 𝑀 } ) ↔ 𝑖 = { 𝑈 , 𝑀 } ) )
23	22	anbi2d	⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝑁 ) → ( ( 𝑖 ∈ 𝐸 ∧ ( 𝑈 ∈ 𝑖 ∧ 𝑖 = { 𝑈 , 𝑀 } ) ) ↔ ( 𝑖 ∈ 𝐸 ∧ 𝑖 = { 𝑈 , 𝑀 } ) ) )
24	16 23	syl5bb	⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝑁 ) → ( ( ( 𝑖 ∈ 𝐸 ∧ 𝑈 ∈ 𝑖 ) ∧ 𝑖 = { 𝑈 , 𝑀 } ) ↔ ( 𝑖 ∈ 𝐸 ∧ 𝑖 = { 𝑈 , 𝑀 } ) ) )
25	24	eubidv	⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝑁 ) → ( ∃! 𝑖 ( ( 𝑖 ∈ 𝐸 ∧ 𝑈 ∈ 𝑖 ) ∧ 𝑖 = { 𝑈 , 𝑀 } ) ↔ ∃! 𝑖 ( 𝑖 ∈ 𝐸 ∧ 𝑖 = { 𝑈 , 𝑀 } ) ) )
26	15 25	mpbird	⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝑁 ) → ∃! 𝑖 ( ( 𝑖 ∈ 𝐸 ∧ 𝑈 ∈ 𝑖 ) ∧ 𝑖 = { 𝑈 , 𝑀 } ) )
27		df-reu	⊢ ( ∃! 𝑖 ∈ 𝐼 𝑖 = { 𝑈 , 𝑀 } ↔ ∃! 𝑖 ( 𝑖 ∈ 𝐼 ∧ 𝑖 = { 𝑈 , 𝑀 } ) )
28		eleq2	⊢ ( 𝑒 = 𝑖 → ( 𝑈 ∈ 𝑒 ↔ 𝑈 ∈ 𝑖 ) )
29	28 4	elrab2	⊢ ( 𝑖 ∈ 𝐼 ↔ ( 𝑖 ∈ 𝐸 ∧ 𝑈 ∈ 𝑖 ) )
30	29	anbi1i	⊢ ( ( 𝑖 ∈ 𝐼 ∧ 𝑖 = { 𝑈 , 𝑀 } ) ↔ ( ( 𝑖 ∈ 𝐸 ∧ 𝑈 ∈ 𝑖 ) ∧ 𝑖 = { 𝑈 , 𝑀 } ) )
31	30	eubii	⊢ ( ∃! 𝑖 ( 𝑖 ∈ 𝐼 ∧ 𝑖 = { 𝑈 , 𝑀 } ) ↔ ∃! 𝑖 ( ( 𝑖 ∈ 𝐸 ∧ 𝑈 ∈ 𝑖 ) ∧ 𝑖 = { 𝑈 , 𝑀 } ) )
32	27 31	bitri	⊢ ( ∃! 𝑖 ∈ 𝐼 𝑖 = { 𝑈 , 𝑀 } ↔ ∃! 𝑖 ( ( 𝑖 ∈ 𝐸 ∧ 𝑈 ∈ 𝑖 ) ∧ 𝑖 = { 𝑈 , 𝑀 } ) )
33	26 32	sylibr	⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝑁 ) → ∃! 𝑖 ∈ 𝐼 𝑖 = { 𝑈 , 𝑀 } )