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

Metamath Proof Explorer

Theorem 1loopgrnb0

Description: In a graph (simple pseudograph) with one edge which is a loop, the vertex connected with itself by the loop has no neighbors. (Contributed by AV, 17-Dec-2020) (Revised by AV, 21-Feb-2021)

Ref Expression
Hypotheses 1loopgruspgr.v ⊢ ( 𝜑 → ( Vtx ‘ 𝐺 ) = 𝑉 )
1loopgruspgr.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
1loopgruspgr.n ⊢ ( 𝜑 → 𝑁 ∈ 𝑉 )
1loopgruspgr.i ⊢ ( 𝜑 → ( iEdg ‘ 𝐺 ) = { ⟨ 𝐴 , { 𝑁 } ⟩ } )
Assertion 1loopgrnb0 ( 𝜑 → ( 𝐺 NeighbVtx 𝑁 ) = ∅ )

Proof

Step Hyp Ref Expression
1 1loopgruspgr.v ⊢ ( 𝜑 → ( Vtx ‘ 𝐺 ) = 𝑉 )
2 1loopgruspgr.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
3 1loopgruspgr.n ⊢ ( 𝜑 → 𝑁 ∈ 𝑉 )
4 1loopgruspgr.i ⊢ ( 𝜑 → ( iEdg ‘ 𝐺 ) = { ⟨ 𝐴 , { 𝑁 } ⟩ } )
5 1 2 3 4 1loopgruspgr ⊢ ( 𝜑 → 𝐺 ∈ USPGraph )
6 uspgrupgr ⊢ ( 𝐺 ∈ USPGraph → 𝐺 ∈ UPGraph )
7 5 6 syl ⊢ ( 𝜑 → 𝐺 ∈ UPGraph )
8 1 eleq2d ⊢ ( 𝜑 → ( 𝑁 ∈ ( Vtx ‘ 𝐺 ) ↔ 𝑁 ∈ 𝑉 ) )
9 3 8 mpbird ⊢ ( 𝜑 → 𝑁 ∈ ( Vtx ‘ 𝐺 ) )
10 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
11 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
12 10 11 nbupgr ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ ( Vtx ‘ 𝐺 ) ) → ( 𝐺 NeighbVtx 𝑁 ) = { 𝑣 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑁 } ) ∣ { 𝑁 , 𝑣 } ∈ ( Edg ‘ 𝐺 ) } )
13 7 9 12 syl2anc ⊢ ( 𝜑 → ( 𝐺 NeighbVtx 𝑁 ) = { 𝑣 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑁 } ) ∣ { 𝑁 , 𝑣 } ∈ ( Edg ‘ 𝐺 ) } )
14 1 difeq1d ⊢ ( 𝜑 → ( ( Vtx ‘ 𝐺 ) ∖ { 𝑁 } ) = ( 𝑉 ∖ { 𝑁 } ) )
15 14 eleq2d ⊢ ( 𝜑 → ( 𝑣 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑁 } ) ↔ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ) )
16 eldifsn ⊢ ( 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ↔ ( 𝑣 ∈ 𝑉 ∧ 𝑣 ≠ 𝑁 ) )
17 3 adantr ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → 𝑁 ∈ 𝑉 )
18 simpr ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → 𝑣 ∈ 𝑉 )
19 17 18 preqsnd ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → ( { 𝑁 , 𝑣 } = { 𝑁 } ↔ ( 𝑁 = 𝑁 ∧ 𝑣 = 𝑁 ) ) )
20 simpr ⊢ ( ( 𝑁 = 𝑁 ∧ 𝑣 = 𝑁 ) → 𝑣 = 𝑁 )
21 19 20 biimtrdi ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → ( { 𝑁 , 𝑣 } = { 𝑁 } → 𝑣 = 𝑁 ) )
22 21 necon3ad ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → ( 𝑣 ≠ 𝑁 → ¬ { 𝑁 , 𝑣 } = { 𝑁 } ) )
23 22 expimpd ⊢ ( 𝜑 → ( ( 𝑣 ∈ 𝑉 ∧ 𝑣 ≠ 𝑁 ) → ¬ { 𝑁 , 𝑣 } = { 𝑁 } ) )
24 16 23 biimtrid ⊢ ( 𝜑 → ( 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) → ¬ { 𝑁 , 𝑣 } = { 𝑁 } ) )
25 15 24 sylbid ⊢ ( 𝜑 → ( 𝑣 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑁 } ) → ¬ { 𝑁 , 𝑣 } = { 𝑁 } ) )
26 25 imp ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑁 } ) ) → ¬ { 𝑁 , 𝑣 } = { 𝑁 } )
27 1 2 3 4 1loopgredg ⊢ ( 𝜑 → ( Edg ‘ 𝐺 ) = { { 𝑁 } } )
28 27 eleq2d ⊢ ( 𝜑 → ( { 𝑁 , 𝑣 } ∈ ( Edg ‘ 𝐺 ) ↔ { 𝑁 , 𝑣 } ∈ { { 𝑁 } } ) )
29 prex ⊢ { 𝑁 , 𝑣 } ∈ V
30 29 elsn ⊢ ( { 𝑁 , 𝑣 } ∈ { { 𝑁 } } ↔ { 𝑁 , 𝑣 } = { 𝑁 } )
31 28 30 bitrdi ⊢ ( 𝜑 → ( { 𝑁 , 𝑣 } ∈ ( Edg ‘ 𝐺 ) ↔ { 𝑁 , 𝑣 } = { 𝑁 } ) )
32 31 notbid ⊢ ( 𝜑 → ( ¬ { 𝑁 , 𝑣 } ∈ ( Edg ‘ 𝐺 ) ↔ ¬ { 𝑁 , 𝑣 } = { 𝑁 } ) )
33 32 adantr ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑁 } ) ) → ( ¬ { 𝑁 , 𝑣 } ∈ ( Edg ‘ 𝐺 ) ↔ ¬ { 𝑁 , 𝑣 } = { 𝑁 } ) )
34 26 33 mpbird ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑁 } ) ) → ¬ { 𝑁 , 𝑣 } ∈ ( Edg ‘ 𝐺 ) )
35 34 ralrimiva ⊢ ( 𝜑 → ∀ 𝑣 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑁 } ) ¬ { 𝑁 , 𝑣 } ∈ ( Edg ‘ 𝐺 ) )
36 rabeq0 ⊢ ( { 𝑣 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑁 } ) ∣ { 𝑁 , 𝑣 } ∈ ( Edg ‘ 𝐺 ) } = ∅ ↔ ∀ 𝑣 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑁 } ) ¬ { 𝑁 , 𝑣 } ∈ ( Edg ‘ 𝐺 ) )
37 35 36 sylibr ⊢ ( 𝜑 → { 𝑣 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑁 } ) ∣ { 𝑁 , 𝑣 } ∈ ( Edg ‘ 𝐺 ) } = ∅ )
38 13 37 eqtrd ⊢ ( 𝜑 → ( 𝐺 NeighbVtx 𝑁 ) = ∅ )