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 𝑉 = ( Vtx ‘ 𝐺 )
frgrncvvdeq.e 𝐸 = ( Edg ‘ 𝐺 )
frgrncvvdeq.nx 𝐷 = ( 𝐺 NeighbVtx 𝑋 )
frgrncvvdeq.ny 𝑁 = ( 𝐺 NeighbVtx 𝑌 )
frgrncvvdeq.x ( 𝜑𝑋𝑉 )
frgrncvvdeq.y ( 𝜑𝑌𝑉 )
frgrncvvdeq.ne ( 𝜑𝑋𝑌 )
frgrncvvdeq.xy ( 𝜑𝑌𝐷 )
frgrncvvdeq.f ( 𝜑𝐺 ∈ FriendGraph )
frgrncvvdeq.a 𝐴 = ( 𝑥𝐷 ↦ ( 𝑦𝑁 { 𝑥 , 𝑦 } ∈ 𝐸 ) )
Assertion frgrncvvdeqlem5 ( ( 𝜑𝑥𝐷 ) → { ( 𝐴𝑥 ) } = ( ( 𝐺 NeighbVtx 𝑥 ) ∩ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 frgrncvvdeq.v1 𝑉 = ( Vtx ‘ 𝐺 )
2 frgrncvvdeq.e 𝐸 = ( Edg ‘ 𝐺 )
3 frgrncvvdeq.nx 𝐷 = ( 𝐺 NeighbVtx 𝑋 )
4 frgrncvvdeq.ny 𝑁 = ( 𝐺 NeighbVtx 𝑌 )
5 frgrncvvdeq.x ( 𝜑𝑋𝑉 )
6 frgrncvvdeq.y ( 𝜑𝑌𝑉 )
7 frgrncvvdeq.ne ( 𝜑𝑋𝑌 )
8 frgrncvvdeq.xy ( 𝜑𝑌𝐷 )
9 frgrncvvdeq.f ( 𝜑𝐺 ∈ FriendGraph )
10 frgrncvvdeq.a 𝐴 = ( 𝑥𝐷 ↦ ( 𝑦𝑁 { 𝑥 , 𝑦 } ∈ 𝐸 ) )
11 simpr ( ( 𝜑𝑥𝐷 ) → 𝑥𝐷 )
12 riotaex ( 𝑦𝑁 { 𝑥 , 𝑦 } ∈ 𝐸 ) ∈ V
13 10 fvmpt2 ( ( 𝑥𝐷 ∧ ( 𝑦𝑁 { 𝑥 , 𝑦 } ∈ 𝐸 ) ∈ V ) → ( 𝐴𝑥 ) = ( 𝑦𝑁 { 𝑥 , 𝑦 } ∈ 𝐸 ) )
14 11 12 13 sylancl ( ( 𝜑𝑥𝐷 ) → ( 𝐴𝑥 ) = ( 𝑦𝑁 { 𝑥 , 𝑦 } ∈ 𝐸 ) )
15 14 sneqd ( ( 𝜑𝑥𝐷 ) → { ( 𝐴𝑥 ) } = { ( 𝑦𝑁 { 𝑥 , 𝑦 } ∈ 𝐸 ) } )
16 1 2 3 4 5 6 7 8 9 10 frgrncvvdeqlem3 ( ( 𝜑𝑥𝐷 ) → { ( 𝑦𝑁 { 𝑥 , 𝑦 } ∈ 𝐸 ) } = ( ( 𝐺 NeighbVtx 𝑥 ) ∩ 𝑁 ) )
17 15 16 eqtrd ( ( 𝜑𝑥𝐷 ) → { ( 𝐴𝑥 ) } = ( ( 𝐺 NeighbVtx 𝑥 ) ∩ 𝑁 ) )