Theorem clnbgrel

Description: Characterization of a member N of the closed neighborhood of a vertex X in a graph G . (Contributed by AV, 9-May-2025)

	Ref	Expression
Hypotheses	clnbgrel.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	clnbgrel.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion	clnbgrel	⊢ ( 𝑁 ∈ ( 𝐺 ClNeighbVtx 𝑋 ) ↔ ( ( 𝑁 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑁 = 𝑋 ∨ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) ) )

Proof

Step	Hyp	Ref	Expression
1		clnbgrel.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		clnbgrel.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
3	1	clnbgrcl	⊢ ( 𝑁 ∈ ( 𝐺 ClNeighbVtx 𝑋 ) → 𝑋 ∈ 𝑉 )
4	3	pm4.71ri	⊢ ( 𝑁 ∈ ( 𝐺 ClNeighbVtx 𝑋 ) ↔ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( 𝐺 ClNeighbVtx 𝑋 ) ) )
5	1 2	clnbgrval	⊢ ( 𝑋 ∈ 𝑉 → ( 𝐺 ClNeighbVtx 𝑋 ) = ( { 𝑋 } ∪ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑛 } ⊆ 𝑒 } ) )
6	5	eleq2d	⊢ ( 𝑋 ∈ 𝑉 → ( 𝑁 ∈ ( 𝐺 ClNeighbVtx 𝑋 ) ↔ 𝑁 ∈ ( { 𝑋 } ∪ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑛 } ⊆ 𝑒 } ) ) )
7		elun	⊢ ( 𝑁 ∈ ( { 𝑋 } ∪ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑛 } ⊆ 𝑒 } ) ↔ ( 𝑁 ∈ { 𝑋 } ∨ 𝑁 ∈ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑛 } ⊆ 𝑒 } ) )
8		elsn2g	⊢ ( 𝑋 ∈ 𝑉 → ( 𝑁 ∈ { 𝑋 } ↔ 𝑁 = 𝑋 ) )
9		preq2	⊢ ( 𝑛 = 𝑁 → { 𝑋 , 𝑛 } = { 𝑋 , 𝑁 } )
10	9	sseq1d	⊢ ( 𝑛 = 𝑁 → ( { 𝑋 , 𝑛 } ⊆ 𝑒 ↔ { 𝑋 , 𝑁 } ⊆ 𝑒 ) )
11	10	rexbidv	⊢ ( 𝑛 = 𝑁 → ( ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑛 } ⊆ 𝑒 ↔ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) )
12	11	elrab	⊢ ( 𝑁 ∈ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑛 } ⊆ 𝑒 } ↔ ( 𝑁 ∈ 𝑉 ∧ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) )
13	12	a1i	⊢ ( 𝑋 ∈ 𝑉 → ( 𝑁 ∈ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑛 } ⊆ 𝑒 } ↔ ( 𝑁 ∈ 𝑉 ∧ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) ) )
14	8 13	orbi12d	⊢ ( 𝑋 ∈ 𝑉 → ( ( 𝑁 ∈ { 𝑋 } ∨ 𝑁 ∈ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑛 } ⊆ 𝑒 } ) ↔ ( 𝑁 = 𝑋 ∨ ( 𝑁 ∈ 𝑉 ∧ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) ) ) )
15	7 14	bitrid	⊢ ( 𝑋 ∈ 𝑉 → ( 𝑁 ∈ ( { 𝑋 } ∪ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑛 } ⊆ 𝑒 } ) ↔ ( 𝑁 = 𝑋 ∨ ( 𝑁 ∈ 𝑉 ∧ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) ) ) )
16		eleq1	⊢ ( 𝑁 = 𝑋 → ( 𝑁 ∈ 𝑉 ↔ 𝑋 ∈ 𝑉 ) )
17	16	biimparc	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 = 𝑋 ) → 𝑁 ∈ 𝑉 )
18		orc	⊢ ( 𝑁 = 𝑋 → ( 𝑁 = 𝑋 ∨ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) )
19	18	adantl	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 = 𝑋 ) → ( 𝑁 = 𝑋 ∨ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) )
20	17 19	jca	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 = 𝑋 ) → ( 𝑁 ∈ 𝑉 ∧ ( 𝑁 = 𝑋 ∨ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) ) )
21	20	ex	⊢ ( 𝑋 ∈ 𝑉 → ( 𝑁 = 𝑋 → ( 𝑁 ∈ 𝑉 ∧ ( 𝑁 = 𝑋 ∨ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) ) ) )
22		olc	⊢ ( ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 → ( 𝑁 = 𝑋 ∨ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) )
23	22	anim2i	⊢ ( ( 𝑁 ∈ 𝑉 ∧ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) → ( 𝑁 ∈ 𝑉 ∧ ( 𝑁 = 𝑋 ∨ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) ) )
24	23	a1i	⊢ ( 𝑋 ∈ 𝑉 → ( ( 𝑁 ∈ 𝑉 ∧ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) → ( 𝑁 ∈ 𝑉 ∧ ( 𝑁 = 𝑋 ∨ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) ) ) )
25	21 24	jaod	⊢ ( 𝑋 ∈ 𝑉 → ( ( 𝑁 = 𝑋 ∨ ( 𝑁 ∈ 𝑉 ∧ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) ) → ( 𝑁 ∈ 𝑉 ∧ ( 𝑁 = 𝑋 ∨ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) ) ) )
26		orc	⊢ ( 𝑁 = 𝑋 → ( 𝑁 = 𝑋 ∨ ( 𝑁 ∈ 𝑉 ∧ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) ) )
27	26	a1i	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) → ( 𝑁 = 𝑋 → ( 𝑁 = 𝑋 ∨ ( 𝑁 ∈ 𝑉 ∧ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) ) ) )
28		olc	⊢ ( ( 𝑁 ∈ 𝑉 ∧ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) → ( 𝑁 = 𝑋 ∨ ( 𝑁 ∈ 𝑉 ∧ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) ) )
29	28	ex	⊢ ( 𝑁 ∈ 𝑉 → ( ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 → ( 𝑁 = 𝑋 ∨ ( 𝑁 ∈ 𝑉 ∧ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) ) ) )
30	29	adantl	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) → ( ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 → ( 𝑁 = 𝑋 ∨ ( 𝑁 ∈ 𝑉 ∧ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) ) ) )
31	27 30	jaod	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) → ( ( 𝑁 = 𝑋 ∨ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) → ( 𝑁 = 𝑋 ∨ ( 𝑁 ∈ 𝑉 ∧ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) ) ) )
32	31	expimpd	⊢ ( 𝑋 ∈ 𝑉 → ( ( 𝑁 ∈ 𝑉 ∧ ( 𝑁 = 𝑋 ∨ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) ) → ( 𝑁 = 𝑋 ∨ ( 𝑁 ∈ 𝑉 ∧ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) ) ) )
33	25 32	impbid	⊢ ( 𝑋 ∈ 𝑉 → ( ( 𝑁 = 𝑋 ∨ ( 𝑁 ∈ 𝑉 ∧ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) ) ↔ ( 𝑁 ∈ 𝑉 ∧ ( 𝑁 = 𝑋 ∨ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) ) ) )
34	6 15 33	3bitrd	⊢ ( 𝑋 ∈ 𝑉 → ( 𝑁 ∈ ( 𝐺 ClNeighbVtx 𝑋 ) ↔ ( 𝑁 ∈ 𝑉 ∧ ( 𝑁 = 𝑋 ∨ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) ) ) )
35	34	pm5.32i	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( 𝐺 ClNeighbVtx 𝑋 ) ) ↔ ( 𝑋 ∈ 𝑉 ∧ ( 𝑁 ∈ 𝑉 ∧ ( 𝑁 = 𝑋 ∨ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) ) ) )
36		anass	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑁 = 𝑋 ∨ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) ) ↔ ( 𝑋 ∈ 𝑉 ∧ ( 𝑁 ∈ 𝑉 ∧ ( 𝑁 = 𝑋 ∨ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) ) ) )
37	36	bicomi	⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝑁 ∈ 𝑉 ∧ ( 𝑁 = 𝑋 ∨ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) ) ) ↔ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑁 = 𝑋 ∨ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) ) )
38		ancom	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ↔ ( 𝑁 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) )
39	37 38	bianbi	⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝑁 ∈ 𝑉 ∧ ( 𝑁 = 𝑋 ∨ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) ) ) ↔ ( ( 𝑁 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑁 = 𝑋 ∨ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) ) )
40	4 35 39	3bitri	⊢ ( 𝑁 ∈ ( 𝐺 ClNeighbVtx 𝑋 ) ↔ ( ( 𝑁 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑁 = 𝑋 ∨ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) ) )