Metamath Proof Explorer


Theorem frgrncvvdeqlem10

Description: Lemma 10 for frgrncvvdeq . (Contributed by Alexander van der Vekens, 24-Dec-2017) (Revised by AV, 10-May-2021) (Proof shortened by AV, 30-Dec-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 frgrncvvdeqlem10 ( 𝜑𝐴 : 𝐷1-1-onto𝑁 )

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 frgrncvvdeqlem8 ( 𝜑𝐴 : 𝐷1-1𝑁 )
12 1 2 3 4 5 6 7 8 9 10 frgrncvvdeqlem9 ( 𝜑𝐴 : 𝐷onto𝑁 )
13 df-f1o ( 𝐴 : 𝐷1-1-onto𝑁 ↔ ( 𝐴 : 𝐷1-1𝑁𝐴 : 𝐷onto𝑁 ) )
14 11 12 13 sylanbrc ( 𝜑𝐴 : 𝐷1-1-onto𝑁 )