Metamath Proof Explorer

Theorem frgrncvvdeqlem5

Description: Lemma 5 for frgrncvvdeq . The mapping of neighbors to neighbors applied on a vertex is the intersection of the corresponding neighborhoods. (Contributed by Alexander van der Vekens, 23-Dec-2017) (Revised by AV, 10-May-2021)

Ref Expression
Hypotheses frgrncvvdeq.v1 ⊢ V = Vtx ⁡ G
frgrncvvdeq.e ⊢ E = Edg ⁡ G
frgrncvvdeq.nx ⊢ D = G NeighbVtx X
frgrncvvdeq.ny ⊢ N = G NeighbVtx Y
frgrncvvdeq.x ⊢ φ → X ∈ V
frgrncvvdeq.y ⊢ φ → Y ∈ V
frgrncvvdeq.ne ⊢ φ → X ≠ Y
frgrncvvdeq.xy ⊢ φ → Y ∉ D
frgrncvvdeq.f ⊢ φ → G ∈ FriendGraph
frgrncvvdeq.a ⊢ A = x ∈ D ⟼ ι y ∈ N | x y ∈ E
Assertion frgrncvvdeqlem5 ⊢ φ ∧ x ∈ D → A ⁡ x = G NeighbVtx x ∩ N

Proof

Step Hyp Ref Expression
1 frgrncvvdeq.v1 ⊢ V = Vtx ⁡ G
2 frgrncvvdeq.e ⊢ E = Edg ⁡ G
3 frgrncvvdeq.nx ⊢ D = G NeighbVtx X
4 frgrncvvdeq.ny ⊢ N = G NeighbVtx Y
5 frgrncvvdeq.x ⊢ φ → X ∈ V
6 frgrncvvdeq.y ⊢ φ → Y ∈ V
7 frgrncvvdeq.ne ⊢ φ → X ≠ Y
8 frgrncvvdeq.xy ⊢ φ → Y ∉ D
9 frgrncvvdeq.f ⊢ φ → G ∈ FriendGraph
10 frgrncvvdeq.a ⊢ A = x ∈ D ⟼ ι y ∈ N | x y ∈ E
11 simpr ⊢ φ ∧ x ∈ D → x ∈ D
12 riotaex ⊢ ι y ∈ N | x y ∈ E ∈ V
13 10 fvmpt2 ⊢ x ∈ D ∧ ι y ∈ N | x y ∈ E ∈ V → A ⁡ x = ι y ∈ N | x y ∈ E
14 11 12 13 sylancl ⊢ φ ∧ x ∈ D → A ⁡ x = ι y ∈ N | x y ∈ E
15 14 sneqd ⊢ φ ∧ x ∈ D → A ⁡ x = ι y ∈ N | x y ∈ E
16 1 2 3 4 5 6 7 8 9 10 frgrncvvdeqlem3 ⊢ φ ∧ x ∈ D → ι y ∈ N | x y ∈ E = G NeighbVtx x ∩ N
17 15 16 eqtrd ⊢ φ ∧ x ∈ D → A ⁡ x = G NeighbVtx x ∩ N