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	syl6bi	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → ( { 𝑁 , 𝑣 } = { 𝑁 } → 𝑣 = 𝑁 ) )
22	21	necon3ad	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → ( 𝑣 ≠ 𝑁 → ¬ { 𝑁 , 𝑣 } = { 𝑁 } ) )
23	22	expimpd	⊢ ( 𝜑 → ( ( 𝑣 ∈ 𝑉 ∧ 𝑣 ≠ 𝑁 ) → ¬ { 𝑁 , 𝑣 } = { 𝑁 } ) )
24	16 23	syl5bi	⊢ ( 𝜑 → ( 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) → ¬ { 𝑁 , 𝑣 } = { 𝑁 } ) )
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 𝑁 ) = ∅ )