Metamath Proof Explorer

Theorem dfclnbgr3

Description: Alternate definition of the closed neighborhood of a vertex using the edge function instead of the edges themselves (see also clnbgrval ). (Contributed by AV, 8-May-2025)

Ref Expression
Hypotheses dfclnbgr3.v ⊢ V = Vtx ⁡ G
dfclnbgr3.i ⊢ I = iEdg ⁡ G
Assertion dfclnbgr3 ⊢ N ∈ V ∧ Fun ⁡ I → G ClNeighbVtx N = N ∪ n ∈ V | ∃ i ∈ dom ⁡ I N n ⊆ I ⁡ i

Proof

Step Hyp Ref Expression
1 dfclnbgr3.v ⊢ V = Vtx ⁡ G
2 dfclnbgr3.i ⊢ I = iEdg ⁡ G
3 edgval ⊢ Edg ⁡ G = ran ⁡ iEdg ⁡ G
4 3 eqcomi ⊢ ran ⁡ iEdg ⁡ G = Edg ⁡ G
5 1 4 clnbgrval ⊢ N ∈ V → G ClNeighbVtx N = N ∪ n ∈ V | ∃ e ∈ ran ⁡ iEdg ⁡ G N n ⊆ e
6 5 adantr ⊢ N ∈ V ∧ Fun ⁡ I → G ClNeighbVtx N = N ∪ n ∈ V | ∃ e ∈ ran ⁡ iEdg ⁡ G N n ⊆ e
7 2 eqcomi ⊢ iEdg ⁡ G = I
8 7 rneqi ⊢ ran ⁡ iEdg ⁡ G = ran ⁡ I
9 8 rexeqi ⊢ ∃ e ∈ ran ⁡ iEdg ⁡ G N n ⊆ e ↔ ∃ e ∈ ran ⁡ I N n ⊆ e
10 funfn ⊢ Fun ⁡ I ↔ I Fn dom ⁡ I
11 10 biimpi ⊢ Fun ⁡ I → I Fn dom ⁡ I
12 11 adantl ⊢ N ∈ V ∧ Fun ⁡ I → I Fn dom ⁡ I
13 sseq2 ⊢ e = I ⁡ i → N n ⊆ e ↔ N n ⊆ I ⁡ i
14 13 rexrn ⊢ I Fn dom ⁡ I → ∃ e ∈ ran ⁡ I N n ⊆ e ↔ ∃ i ∈ dom ⁡ I N n ⊆ I ⁡ i
15 12 14 syl ⊢ N ∈ V ∧ Fun ⁡ I → ∃ e ∈ ran ⁡ I N n ⊆ e ↔ ∃ i ∈ dom ⁡ I N n ⊆ I ⁡ i
16 9 15 bitrid ⊢ N ∈ V ∧ Fun ⁡ I → ∃ e ∈ ran ⁡ iEdg ⁡ G N n ⊆ e ↔ ∃ i ∈ dom ⁡ I N n ⊆ I ⁡ i
17 16 rabbidv ⊢ N ∈ V ∧ Fun ⁡ I → n ∈ V | ∃ e ∈ ran ⁡ iEdg ⁡ G N n ⊆ e = n ∈ V | ∃ i ∈ dom ⁡ I N n ⊆ I ⁡ i
18 17 uneq2d ⊢ N ∈ V ∧ Fun ⁡ I → N ∪ n ∈ V | ∃ e ∈ ran ⁡ iEdg ⁡ G N n ⊆ e = N ∪ n ∈ V | ∃ i ∈ dom ⁡ I N n ⊆ I ⁡ i
19 6 18 eqtrd ⊢ N ∈ V ∧ Fun ⁡ I → G ClNeighbVtx N = N ∪ n ∈ V | ∃ i ∈ dom ⁡ I N n ⊆ I ⁡ i