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	|- V = ( Vtx ` G )
	frgrncvvdeq.e	|- E = ( Edg ` G )
	frgrncvvdeq.nx	|- D = ( G NeighbVtx X )
	frgrncvvdeq.ny	|- N = ( G NeighbVtx Y )
	frgrncvvdeq.x	|- ( ph -> X e. V )
	frgrncvvdeq.y	|- ( ph -> Y e. V )
	frgrncvvdeq.ne	|- ( ph -> X =/= Y )
	frgrncvvdeq.xy	|- ( ph -> Y e/ D )
	frgrncvvdeq.f	|- ( ph -> G e. FriendGraph )
	frgrncvvdeq.a	|- A = ( x e. D |-> ( iota_ y e. N { x , y } e. E ) )
Assertion	frgrncvvdeqlem4	|- ( ph -> A : D --> 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	|- ( ph -> X e. V )
6		frgrncvvdeq.y	|- ( ph -> Y e. V )
7		frgrncvvdeq.ne	|- ( ph -> X =/= Y )
8		frgrncvvdeq.xy	|- ( ph -> Y e/ D )
9		frgrncvvdeq.f	|- ( ph -> G e. FriendGraph )
10		frgrncvvdeq.a	|- A = ( x e. D |-> ( iota_ y e. N { x , y } e. E ) )
11	1 2 3 4 5 6 7 8 9 10	frgrncvvdeqlem2	|- ( ( ph /\ x e. D ) -> E! y e. N { x , y } e. E )
12		riotacl	|- ( E! y e. N { x , y } e. E -> ( iota_ y e. N { x , y } e. E ) e. N )
13	11 12	syl	|- ( ( ph /\ x e. D ) -> ( iota_ y e. N { x , y } e. E ) e. N )
14	13 10	fmptd	|- ( ph -> A : D --> N )