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	$⊢ φ \to Vtx (G) = V$
	1loopgruspgr.a	$⊢ φ \to A \in X$
	1loopgruspgr.n	$⊢ φ \to N \in V$
	1loopgruspgr.i	$⊢ φ \to iEdg (G) = \{⟨A, \{N\}⟩\}$
Assertion	1loopgrnb0	$⊢ φ \to G NeighbVtx N = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		1loopgruspgr.v	$⊢ φ \to Vtx (G) = V$
2		1loopgruspgr.a	$⊢ φ \to A \in X$
3		1loopgruspgr.n	$⊢ φ \to N \in V$
4		1loopgruspgr.i	$⊢ φ \to iEdg (G) = \{⟨A, \{N\}⟩\}$
5	1 2 3 4	1loopgruspgr	$⊢ φ \to G \in USHGraph$
6		uspgrupgr	$⊢ G \in USHGraph \to G \in UPGraph$
7	5 6	syl	$⊢ φ \to G \in UPGraph$
8	1	eleq2d	$⊢ φ \to (N \in Vtx (G) \leftrightarrow N \in V)$
9	3 8	mpbird	$⊢ φ \to N \in Vtx (G)$
10		eqid	$⊢ Vtx (G) = Vtx (G)$
11		eqid	$⊢ Edg (G) = Edg (G)$
12	10 11	nbupgr	$⊢ (G \in UPGraph \land N \in Vtx (G)) \to G NeighbVtx N = \{v \in (Vtx (G) ∖ \{N\}) \| \{N, v\} \in Edg (G)\}$
13	7 9 12	syl2anc	$⊢ φ \to G NeighbVtx N = \{v \in (Vtx (G) ∖ \{N\}) \| \{N, v\} \in Edg (G)\}$
14	1	difeq1d	$⊢ φ \to Vtx (G) ∖ \{N\} = V ∖ \{N\}$
15	14	eleq2d	$⊢ φ \to (v \in (Vtx (G) ∖ \{N\}) \leftrightarrow v \in (V ∖ \{N\}))$
16		eldifsn	$⊢ v \in (V ∖ \{N\}) \leftrightarrow (v \in V \land v \neq N)$
17	3	adantr	$⊢ (φ \land v \in V) \to N \in V$
18		simpr	$⊢ (φ \land v \in V) \to v \in V$
19	17 18	preqsnd	$⊢ (φ \land v \in V) \to (\{N, v\} = \{N\} \leftrightarrow (N = N \land v = N))$
20		simpr	$⊢ (N = N \land v = N) \to v = N$
21	19 20	biimtrdi	$⊢ (φ \land v \in V) \to (\{N, v\} = \{N\} \to v = N)$
22	21	necon3ad	$⊢ (φ \land v \in V) \to (v \neq N \to \neg \{N, v\} = \{N\})$
23	22	expimpd	$⊢ φ \to ((v \in V \land v \neq N) \to \neg \{N, v\} = \{N\})$
24	16 23	biimtrid	$⊢ φ \to (v \in (V ∖ \{N\}) \to \neg \{N, v\} = \{N\})$
25	15 24	sylbid	$⊢ φ \to (v \in (Vtx (G) ∖ \{N\}) \to \neg \{N, v\} = \{N\})$
26	25	imp	$⊢ (φ \land v \in (Vtx (G) ∖ \{N\})) \to \neg \{N, v\} = \{N\}$
27	1 2 3 4	1loopgredg	$⊢ φ \to Edg (G) = \{\{N\}\}$
28	27	eleq2d	$⊢ φ \to (\{N, v\} \in Edg (G) \leftrightarrow \{N, v\} \in \{\{N\}\})$
29		prex	$⊢ \{N, v\} \in V$
30	29	elsn	$⊢ \{N, v\} \in \{\{N\}\} \leftrightarrow \{N, v\} = \{N\}$
31	28 30	bitrdi	$⊢ φ \to (\{N, v\} \in Edg (G) \leftrightarrow \{N, v\} = \{N\})$
32	31	notbid	$⊢ φ \to (\neg \{N, v\} \in Edg (G) \leftrightarrow \neg \{N, v\} = \{N\})$
33	32	adantr	$⊢ (φ \land v \in (Vtx (G) ∖ \{N\})) \to (\neg \{N, v\} \in Edg (G) \leftrightarrow \neg \{N, v\} = \{N\})$
34	26 33	mpbird	$⊢ (φ \land v \in (Vtx (G) ∖ \{N\})) \to \neg \{N, v\} \in Edg (G)$
35	34	ralrimiva	$⊢ φ \to \forall v \in (Vtx (G) ∖ \{N\}) \neg \{N, v\} \in Edg (G)$
36		rabeq0	$⊢ \{v \in (Vtx (G) ∖ \{N\}) \| \{N, v\} \in Edg (G)\} = \emptyset \leftrightarrow \forall v \in (Vtx (G) ∖ \{N\}) \neg \{N, v\} \in Edg (G)$
37	35 36	sylibr	$⊢ φ \to \{v \in (Vtx (G) ∖ \{N\}) \| \{N, v\} \in Edg (G)\} = \emptyset$
38	13 37	eqtrd	$⊢ φ \to G NeighbVtx N = \emptyset$

Metamath Proof Explorer

Theorem 1loopgrnb0

Proof