nbgrel

Description: Characterization of a neighbor N of a vertex X in a graph G . (Contributed by Alexander van der Vekens and Mario Carneiro, 9-Oct-2017) (Revised by AV, 26-Oct-2020) (Revised by AV, 12-Feb-2022)

	Ref	Expression
Hypotheses	nbgrel.v	$⊢ V = Vtx (G)$
	nbgrel.e	$⊢ E = Edg (G)$
Assertion	nbgrel	$⊢ N \in (G NeighbVtx X) \leftrightarrow ((N \in V \land X \in V) \land N \neq X \land \exists e \in E \{X, N\} \subseteq e)$

Proof

Step	Hyp	Ref	Expression
1		nbgrel.v	$⊢ V = Vtx (G)$
2		nbgrel.e	$⊢ E = Edg (G)$
3	1	nbgrcl	$⊢ N \in (G NeighbVtx X) \to X \in V$
4	3	pm4.71ri	$⊢ N \in (G NeighbVtx X) \leftrightarrow (X \in V \land N \in (G NeighbVtx X))$
5	1 2	nbgrval	$⊢ X \in V \to G NeighbVtx X = \{n \in (V ∖ \{X\}) \| \exists e \in E \{X, n\} \subseteq e\}$
6	5	eleq2d	$⊢ X \in V \to (N \in (G NeighbVtx X) \leftrightarrow N \in \{n \in (V ∖ \{X\}) \| \exists e \in E \{X, n\} \subseteq e\})$
7		preq2	$⊢ n = N \to \{X, n\} = \{X, N\}$
8	7	sseq1d	$⊢ n = N \to (\{X, n\} \subseteq e \leftrightarrow \{X, N\} \subseteq e)$
9	8	rexbidv	$⊢ n = N \to (\exists e \in E \{X, n\} \subseteq e \leftrightarrow \exists e \in E \{X, N\} \subseteq e)$
10	9	elrab	$⊢ N \in \{n \in (V ∖ \{X\}) \| \exists e \in E \{X, n\} \subseteq e\} \leftrightarrow (N \in (V ∖ \{X\}) \land \exists e \in E \{X, N\} \subseteq e)$
11		eldifsn	$⊢ N \in (V ∖ \{X\}) \leftrightarrow (N \in V \land N \neq X)$
12	11	anbi1i	$⊢ (N \in (V ∖ \{X\}) \land \exists e \in E \{X, N\} \subseteq e) \leftrightarrow ((N \in V \land N \neq X) \land \exists e \in E \{X, N\} \subseteq e)$
13	10 12	bitri	$⊢ N \in \{n \in (V ∖ \{X\}) \| \exists e \in E \{X, n\} \subseteq e\} \leftrightarrow ((N \in V \land N \neq X) \land \exists e \in E \{X, N\} \subseteq e)$
14	6 13	syl6bb	$⊢ X \in V \to (N \in (G NeighbVtx X) \leftrightarrow ((N \in V \land N \neq X) \land \exists e \in E \{X, N\} \subseteq e))$
15	14	pm5.32i	$⊢ (X \in V \land N \in (G NeighbVtx X)) \leftrightarrow (X \in V \land ((N \in V \land N \neq X) \land \exists e \in E \{X, N\} \subseteq e))$
16		df-3an	$⊢ ((N \in V \land X \in V) \land N \neq X \land \exists e \in E \{X, N\} \subseteq e) \leftrightarrow (((N \in V \land X \in V) \land N \neq X) \land \exists e \in E \{X, N\} \subseteq e)$
17		anass	$⊢ ((X \in V \land N \in V) \land N \neq X) \leftrightarrow (X \in V \land (N \in V \land N \neq X))$
18		ancom	$⊢ (X \in V \land N \in V) \leftrightarrow (N \in V \land X \in V)$
19	18	anbi1i	$⊢ ((X \in V \land N \in V) \land N \neq X) \leftrightarrow ((N \in V \land X \in V) \land N \neq X)$
20	17 19	bitr3i	$⊢ (X \in V \land (N \in V \land N \neq X)) \leftrightarrow ((N \in V \land X \in V) \land N \neq X)$
21	20	anbi1i	$⊢ ((X \in V \land (N \in V \land N \neq X)) \land \exists e \in E \{X, N\} \subseteq e) \leftrightarrow (((N \in V \land X \in V) \land N \neq X) \land \exists e \in E \{X, N\} \subseteq e)$
22		anass	$⊢ ((X \in V \land (N \in V \land N \neq X)) \land \exists e \in E \{X, N\} \subseteq e) \leftrightarrow (X \in V \land ((N \in V \land N \neq X) \land \exists e \in E \{X, N\} \subseteq e))$
23	16 21 22	3bitr2ri	$⊢ (X \in V \land ((N \in V \land N \neq X) \land \exists e \in E \{X, N\} \subseteq e)) \leftrightarrow ((N \in V \land X \in V) \land N \neq X \land \exists e \in E \{X, N\} \subseteq e)$
24	15 23	bitri	$⊢ (X \in V \land N \in (G NeighbVtx X)) \leftrightarrow ((N \in V \land X \in V) \land N \neq X \land \exists e \in E \{X, N\} \subseteq e)$
25	4 24	bitri	$⊢ N \in (G NeighbVtx X) \leftrightarrow ((N \in V \land X \in V) \land N \neq X \land \exists e \in E \{X, N\} \subseteq e)$

Metamath Proof Explorer

Theorem nbgrel

Proof