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

Metamath Proof Explorer

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 biimtrid ⊢ ( ( 𝐺 ∈ 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 bitrid ⊢ ( ( ( 𝐺 ∈ 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 ∧ 𝑈 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝑁 ) → ∃! 𝑖 ∈ 𝐼 𝑖 = { 𝑈 , 𝑀 } )