Metamath Proof Explorer


Theorem frgrncvvdeqlem4

Description: Lemma 4 for frgrncvvdeq . The mapping of neighbors to neighbors is a function. (Contributed by Alexander van der Vekens, 22-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 frgrncvvdeqlem4 ( 𝜑𝐴 : 𝐷𝑁 )

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 1 2 3 4 5 6 7 8 9 10 frgrncvvdeqlem2 ( ( 𝜑𝑥𝐷 ) → ∃! 𝑦𝑁 { 𝑥 , 𝑦 } ∈ 𝐸 )
12 riotacl ( ∃! 𝑦𝑁 { 𝑥 , 𝑦 } ∈ 𝐸 → ( 𝑦𝑁 { 𝑥 , 𝑦 } ∈ 𝐸 ) ∈ 𝑁 )
13 11 12 syl ( ( 𝜑𝑥𝐷 ) → ( 𝑦𝑁 { 𝑥 , 𝑦 } ∈ 𝐸 ) ∈ 𝑁 )
14 13 10 fmptd ( 𝜑𝐴 : 𝐷𝑁 )