clnbgredg

Description: A vertex connected by an edge with another vertex is a neighbor of that vertex. (Contributed by AV, 24-Aug-2025)

	Ref	Expression
Hypotheses	clnbgredg.e	$⊢ E = Edg (G)$
	clnbgredg.n	$⊢ N = G ClNeighbVtx X$
Assertion	clnbgredg	$⊢ (G \in UHGraph \land (K \in E \land X \in K \land Y \in K)) \to Y \in N$

Proof

Step	Hyp	Ref	Expression
1		clnbgredg.e	$⊢ E = Edg (G)$
2		clnbgredg.n	$⊢ N = G ClNeighbVtx X$
3	1	eleq2i	$⊢ K \in E \leftrightarrow K \in Edg (G)$
4	3	biimpi	$⊢ K \in E \to K \in Edg (G)$
5	4	3ad2ant1	$⊢ (K \in E \land X \in K \land Y \in K) \to K \in Edg (G)$
6		simp3	$⊢ (K \in E \land X \in K \land Y \in K) \to Y \in K$
7	5 6	jca	$⊢ (K \in E \land X \in K \land Y \in K) \to (K \in Edg (G) \land Y \in K)$
8	7	anim2i	$⊢ (G \in UHGraph \land (K \in E \land X \in K \land Y \in K)) \to (G \in UHGraph \land (K \in Edg (G) \land Y \in K))$
9		3anass	$⊢ (G \in UHGraph \land K \in Edg (G) \land Y \in K) \leftrightarrow (G \in UHGraph \land (K \in Edg (G) \land Y \in K))$
10	8 9	sylibr	$⊢ (G \in UHGraph \land (K \in E \land X \in K \land Y \in K)) \to (G \in UHGraph \land K \in Edg (G) \land Y \in K)$
11		uhgredgrnv	$⊢ (G \in UHGraph \land K \in Edg (G) \land Y \in K) \to Y \in Vtx (G)$
12	10 11	syl	$⊢ (G \in UHGraph \land (K \in E \land X \in K \land Y \in K)) \to Y \in Vtx (G)$
13		simp2	$⊢ (K \in E \land X \in K \land Y \in K) \to X \in K$
14	5 13	jca	$⊢ (K \in E \land X \in K \land Y \in K) \to (K \in Edg (G) \land X \in K)$
15	14	anim2i	$⊢ (G \in UHGraph \land (K \in E \land X \in K \land Y \in K)) \to (G \in UHGraph \land (K \in Edg (G) \land X \in K))$
16		3anass	$⊢ (G \in UHGraph \land K \in Edg (G) \land X \in K) \leftrightarrow (G \in UHGraph \land (K \in Edg (G) \land X \in K))$
17	15 16	sylibr	$⊢ (G \in UHGraph \land (K \in E \land X \in K \land Y \in K)) \to (G \in UHGraph \land K \in Edg (G) \land X \in K)$
18		uhgredgrnv	$⊢ (G \in UHGraph \land K \in Edg (G) \land X \in K) \to X \in Vtx (G)$
19	17 18	syl	$⊢ (G \in UHGraph \land (K \in E \land X \in K \land Y \in K)) \to X \in Vtx (G)$
20		simpr1	$⊢ (G \in UHGraph \land (K \in E \land X \in K \land Y \in K)) \to K \in E$
21		sseq2	$⊢ e = K \to (\{X, Y\} \subseteq e \leftrightarrow \{X, Y\} \subseteq K)$
22	21	adantl	$⊢ ((G \in UHGraph \land (K \in E \land X \in K \land Y \in K)) \land e = K) \to (\{X, Y\} \subseteq e \leftrightarrow \{X, Y\} \subseteq K)$
23		prssi	$⊢ (X \in K \land Y \in K) \to \{X, Y\} \subseteq K$
24	23	3adant1	$⊢ (K \in E \land X \in K \land Y \in K) \to \{X, Y\} \subseteq K$
25	24	adantl	$⊢ (G \in UHGraph \land (K \in E \land X \in K \land Y \in K)) \to \{X, Y\} \subseteq K$
26	20 22 25	rspcedvd	$⊢ (G \in UHGraph \land (K \in E \land X \in K \land Y \in K)) \to \exists e \in E \{X, Y\} \subseteq e$
27	26	olcd	$⊢ (G \in UHGraph \land (K \in E \land X \in K \land Y \in K)) \to (Y = X \lor \exists e \in E \{X, Y\} \subseteq e)$
28		eqid	$⊢ Vtx (G) = Vtx (G)$
29	28 1	clnbgrel	$⊢ Y \in (G ClNeighbVtx X) \leftrightarrow ((Y \in Vtx (G) \land X \in Vtx (G)) \land (Y = X \lor \exists e \in E \{X, Y\} \subseteq e))$
30	12 19 27 29	syl21anbrc	$⊢ (G \in UHGraph \land (K \in E \land X \in K \land Y \in K)) \to Y \in (G ClNeighbVtx X)$
31	2	eleq2i	$⊢ Y \in N \leftrightarrow Y \in (G ClNeighbVtx X)$
32	30 31	sylibr	$⊢ (G \in UHGraph \land (K \in E \land X \in K \land Y \in K)) \to Y \in N$

Metamath Proof Explorer

Theorem clnbgredg

Proof