Theorem 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	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	nbgrel.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion	nbgrel	⊢ ( 𝑁 ∈ ( 𝐺 NeighbVtx 𝑋 ) ↔ ( ( 𝑁 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑁 ≠ 𝑋 ∧ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) )

Proof

Step	Hyp	Ref	Expression
1		nbgrel.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		nbgrel.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
3	1	nbgrcl	⊢ ( 𝑁 ∈ ( 𝐺 NeighbVtx 𝑋 ) → 𝑋 ∈ 𝑉 )
4	3	pm4.71ri	⊢ ( 𝑁 ∈ ( 𝐺 NeighbVtx 𝑋 ) ↔ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( 𝐺 NeighbVtx 𝑋 ) ) )
5	1 2	nbgrval	⊢ ( 𝑋 ∈ 𝑉 → ( 𝐺 NeighbVtx 𝑋 ) = { 𝑛 ∈ ( 𝑉 ∖ { 𝑋 } ) ∣ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑛 } ⊆ 𝑒 } )
6	5	eleq2d	⊢ ( 𝑋 ∈ 𝑉 → ( 𝑁 ∈ ( 𝐺 NeighbVtx 𝑋 ) ↔ 𝑁 ∈ { 𝑛 ∈ ( 𝑉 ∖ { 𝑋 } ) ∣ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑛 } ⊆ 𝑒 } ) )
7		preq2	⊢ ( 𝑛 = 𝑁 → { 𝑋 , 𝑛 } = { 𝑋 , 𝑁 } )
8	7	sseq1d	⊢ ( 𝑛 = 𝑁 → ( { 𝑋 , 𝑛 } ⊆ 𝑒 ↔ { 𝑋 , 𝑁 } ⊆ 𝑒 ) )
9	8	rexbidv	⊢ ( 𝑛 = 𝑁 → ( ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑛 } ⊆ 𝑒 ↔ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) )
10	9	elrab	⊢ ( 𝑁 ∈ { 𝑛 ∈ ( 𝑉 ∖ { 𝑋 } ) ∣ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑛 } ⊆ 𝑒 } ↔ ( 𝑁 ∈ ( 𝑉 ∖ { 𝑋 } ) ∧ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) )
11		eldifsn	⊢ ( 𝑁 ∈ ( 𝑉 ∖ { 𝑋 } ) ↔ ( 𝑁 ∈ 𝑉 ∧ 𝑁 ≠ 𝑋 ) )
12	11	anbi1i	⊢ ( ( 𝑁 ∈ ( 𝑉 ∖ { 𝑋 } ) ∧ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) ↔ ( ( 𝑁 ∈ 𝑉 ∧ 𝑁 ≠ 𝑋 ) ∧ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) )
13	10 12	bitri	⊢ ( 𝑁 ∈ { 𝑛 ∈ ( 𝑉 ∖ { 𝑋 } ) ∣ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑛 } ⊆ 𝑒 } ↔ ( ( 𝑁 ∈ 𝑉 ∧ 𝑁 ≠ 𝑋 ) ∧ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) )
14	6 13	syl6bb	⊢ ( 𝑋 ∈ 𝑉 → ( 𝑁 ∈ ( 𝐺 NeighbVtx 𝑋 ) ↔ ( ( 𝑁 ∈ 𝑉 ∧ 𝑁 ≠ 𝑋 ) ∧ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) ) )
15	14	pm5.32i	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( 𝐺 NeighbVtx 𝑋 ) ) ↔ ( 𝑋 ∈ 𝑉 ∧ ( ( 𝑁 ∈ 𝑉 ∧ 𝑁 ≠ 𝑋 ) ∧ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) ) )
16		df-3an	⊢ ( ( ( 𝑁 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑁 ≠ 𝑋 ∧ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) ↔ ( ( ( 𝑁 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑁 ≠ 𝑋 ) ∧ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) )
17		anass	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑁 ≠ 𝑋 ) ↔ ( 𝑋 ∈ 𝑉 ∧ ( 𝑁 ∈ 𝑉 ∧ 𝑁 ≠ 𝑋 ) ) )
18		ancom	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ↔ ( 𝑁 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) )
19	18	anbi1i	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑁 ≠ 𝑋 ) ↔ ( ( 𝑁 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑁 ≠ 𝑋 ) )
20	17 19	bitr3i	⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝑁 ∈ 𝑉 ∧ 𝑁 ≠ 𝑋 ) ) ↔ ( ( 𝑁 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑁 ≠ 𝑋 ) )
21	20	anbi1i	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ ( 𝑁 ∈ 𝑉 ∧ 𝑁 ≠ 𝑋 ) ) ∧ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) ↔ ( ( ( 𝑁 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑁 ≠ 𝑋 ) ∧ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) )
22		anass	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ ( 𝑁 ∈ 𝑉 ∧ 𝑁 ≠ 𝑋 ) ) ∧ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) ↔ ( 𝑋 ∈ 𝑉 ∧ ( ( 𝑁 ∈ 𝑉 ∧ 𝑁 ≠ 𝑋 ) ∧ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) ) )
23	16 21 22	3bitr2ri	⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( ( 𝑁 ∈ 𝑉 ∧ 𝑁 ≠ 𝑋 ) ∧ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) ) ↔ ( ( 𝑁 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑁 ≠ 𝑋 ∧ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) )
24	15 23	bitri	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( 𝐺 NeighbVtx 𝑋 ) ) ↔ ( ( 𝑁 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑁 ≠ 𝑋 ∧ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) )
25	4 24	bitri	⊢ ( 𝑁 ∈ ( 𝐺 NeighbVtx 𝑋 ) ↔ ( ( 𝑁 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑁 ≠ 𝑋 ∧ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) )