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=\mathrm{Vtx}\left(G\right)$$
	frgrncvvdeq.e	$$⊢E=\mathrm{Edg}\left(G\right)$$
	frgrncvvdeq.nx	$$⊢D=G\mathrm{NeighbVtx}X$$
	frgrncvvdeq.ny	$$⊢N=G\mathrm{NeighbVtx}Y$$
	frgrncvvdeq.x	$$⊢\phi \to X\in V$$
	frgrncvvdeq.y	$$⊢\phi \to Y\in V$$
	frgrncvvdeq.ne	$$⊢\phi \to X\ne Y$$
	frgrncvvdeq.xy	$$⊢\phi \to Y\notin D$$
	frgrncvvdeq.f	$$⊢\phi \to G\in \mathrm{FriendGraph}$$
	frgrncvvdeq.a	$$⊢A=\left(x\in D⟼\left(\iota y\in N|\left\{x,y\right\}\in E\right)\right)$$
Assertion	frgrncvvdeqlem10	$$⊢\phi \to A:D\underset{1-1\; onto}{⟶}N$$

Proof

Step	Hyp	Ref	Expression
1		frgrncvvdeq.v1	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		frgrncvvdeq.e	$$⊢E=\mathrm{Edg}\left(G\right)$$
3		frgrncvvdeq.nx	$$⊢D=G\mathrm{NeighbVtx}X$$
4		frgrncvvdeq.ny	$$⊢N=G\mathrm{NeighbVtx}Y$$
5		frgrncvvdeq.x	$$⊢\phi \to X\in V$$
6		frgrncvvdeq.y	$$⊢\phi \to Y\in V$$
7		frgrncvvdeq.ne	$$⊢\phi \to X\ne Y$$
8		frgrncvvdeq.xy	$$⊢\phi \to Y\notin D$$
9		frgrncvvdeq.f	$$⊢\phi \to G\in \mathrm{FriendGraph}$$
10		frgrncvvdeq.a	$$⊢A=\left(x\in D⟼\left(\iota y\in N|\left\{x,y\right\}\in E\right)\right)$$
11	1 2 3 4 5 6 7 8 9 10	frgrncvvdeqlem8	$$⊢\phi \to A:D\underset{1-1}{⟶}N$$
12	1 2 3 4 5 6 7 8 9 10	frgrncvvdeqlem9	$$⊢\phi \to A:D\underset{onto}{⟶}N$$
13		df-f1o	$$⊢A:D\underset{1-1\; onto}{⟶}N\leftrightarrow \left(A:D\underset{1-1}{⟶}N\wedge A:D\underset{onto}{⟶}N\right)$$
14	11 12 13	sylanbrc	$$⊢\phi \to A:D\underset{1-1\; onto}{⟶}N$$