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	|- ( 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	frgrncvvdeqlem5	|- ( ( ph /\ x e. D ) -> { ( A ` x ) } = ( ( G NeighbVtx x ) i^i 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		simpr	|- ( ( ph /\ x e. D ) -> x e. D )
12		riotaex	|- ( iota_ y e. N { x , y } e. E ) e. _V
13	10	fvmpt2	|- ( ( x e. D /\ ( iota_ y e. N { x , y } e. E ) e. _V ) -> ( A ` x ) = ( iota_ y e. N { x , y } e. E ) )
14	11 12 13	sylancl	|- ( ( ph /\ x e. D ) -> ( A ` x ) = ( iota_ y e. N { x , y } e. E ) )
15	14	sneqd	|- ( ( ph /\ x e. D ) -> { ( A ` x ) } = { ( iota_ y e. N { x , y } e. E ) } )
16	1 2 3 4 5 6 7 8 9 10	frgrncvvdeqlem3	|- ( ( ph /\ x e. D ) -> { ( iota_ y e. N { x , y } e. E ) } = ( ( G NeighbVtx x ) i^i N ) )
17	15 16	eqtrd	|- ( ( ph /\ x e. D ) -> { ( A ` x ) } = ( ( G NeighbVtx x ) i^i N ) )