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	|- 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	frgrncvvdeqlem10	|- ( ph -> A : D -1-1-onto-> 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	frgrncvvdeqlem8	|- ( ph -> A : D -1-1-> N )
12	1 2 3 4 5 6 7 8 9 10	frgrncvvdeqlem9	|- ( ph -> A : D -onto-> N )
13		df-f1o	|- ( A : D -1-1-onto-> N <-> ( A : D -1-1-> N /\ A : D -onto-> N ) )
14	11 12 13	sylanbrc	|- ( ph -> A : D -1-1-onto-> N )