frgrncvvdeqlem9

Description: Lemma 9 for frgrncvvdeq . This corresponds to statement 3 in Huneke p. 1: "By symmetry the map is onto". (Contributed by Alexander van der Vekens, 24-Dec-2017) (Revised by AV, 10-May-2021) (Proof shortened by AV, 12-Feb-2022)

	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	$⊢ φ \to X \in V$
	frgrncvvdeq.y	$⊢ φ \to Y \in V$
	frgrncvvdeq.ne	$⊢ φ \to X \neq Y$
	frgrncvvdeq.xy	$⊢ φ \to Y \notin D$
	frgrncvvdeq.f	$⊢ φ \to G \in FriendGraph$
	frgrncvvdeq.a	$⊢ A = (x \in D ⟼ (ι y \in N \| \{x, y\} \in E))$
Assertion	frgrncvvdeqlem9	$⊢ φ \to A : D \underset{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	$⊢ φ \to X \in V$
6		frgrncvvdeq.y	$⊢ φ \to Y \in V$
7		frgrncvvdeq.ne	$⊢ φ \to X \neq Y$
8		frgrncvvdeq.xy	$⊢ φ \to Y \notin D$
9		frgrncvvdeq.f	$⊢ φ \to G \in FriendGraph$
10		frgrncvvdeq.a	$⊢ A = (x \in D ⟼ (ι y \in N \| \{x, y\} \in E))$
11	1 2 3 4 5 6 7 8 9 10	frgrncvvdeqlem4	$⊢ φ \to A : D ⟶ N$
12	9	adantr	$⊢ (φ \land n \in N) \to G \in FriendGraph$
13	4	eleq2i	$⊢ n \in N \leftrightarrow n \in (G NeighbVtx Y)$
14	1	nbgrisvtx	$⊢ n \in (G NeighbVtx Y) \to n \in V$
15	14	a1i	$⊢ φ \to (n \in (G NeighbVtx Y) \to n \in V)$
16	13 15	syl5bi	$⊢ φ \to (n \in N \to n \in V)$
17	16	imp	$⊢ (φ \land n \in N) \to n \in V$
18	5	adantr	$⊢ (φ \land n \in N) \to X \in V$
19	1 2 3 4 5 6 7 8 9 10	frgrncvvdeqlem1	$⊢ φ \to X \notin N$
20		df-nel	$⊢ X \notin N \leftrightarrow \neg X \in N$
21		nelelne	$⊢ \neg X \in N \to (n \in N \to n \neq X)$
22	20 21	sylbi	$⊢ X \notin N \to (n \in N \to n \neq X)$
23	19 22	syl	$⊢ φ \to (n \in N \to n \neq X)$
24	23	imp	$⊢ (φ \land n \in N) \to n \neq X$
25	17 18 24	3jca	$⊢ (φ \land n \in N) \to (n \in V \land X \in V \land n \neq X)$
26	12 25	jca	$⊢ (φ \land n \in N) \to (G \in FriendGraph \land (n \in V \land X \in V \land n \neq X))$
27	1 2	frcond2	$⊢ G \in FriendGraph \to ((n \in V \land X \in V \land n \neq X) \to \exists! m \in V (\{n, m\} \in E \land \{m, X\} \in E))$
28	27	imp	$⊢ (G \in FriendGraph \land (n \in V \land X \in V \land n \neq X)) \to \exists! m \in V (\{n, m\} \in E \land \{m, X\} \in E)$
29		reurex	$⊢ \exists! m \in V (\{n, m\} \in E \land \{m, X\} \in E) \to \exists m \in V (\{n, m\} \in E \land \{m, X\} \in E)$
30		df-rex	$⊢ \exists m \in V (\{n, m\} \in E \land \{m, X\} \in E) \leftrightarrow \exists m (m \in V \land (\{n, m\} \in E \land \{m, X\} \in E))$
31	29 30	sylib	$⊢ \exists! m \in V (\{n, m\} \in E \land \{m, X\} \in E) \to \exists m (m \in V \land (\{n, m\} \in E \land \{m, X\} \in E))$
32	26 28 31	3syl	$⊢ (φ \land n \in N) \to \exists m (m \in V \land (\{n, m\} \in E \land \{m, X\} \in E))$
33		frgrusgr	$⊢ G \in FriendGraph \to G \in USGraph$
34	2	nbusgreledg	$⊢ G \in USGraph \to (m \in (G NeighbVtx X) \leftrightarrow \{m, X\} \in E)$
35	34	bicomd	$⊢ G \in USGraph \to (\{m, X\} \in E \leftrightarrow m \in (G NeighbVtx X))$
36	9 33 35	3syl	$⊢ φ \to (\{m, X\} \in E \leftrightarrow m \in (G NeighbVtx X))$
37	36	biimpa	$⊢ (φ \land \{m, X\} \in E) \to m \in (G NeighbVtx X)$
38	3	eleq2i	$⊢ m \in D \leftrightarrow m \in (G NeighbVtx X)$
39	37 38	sylibr	$⊢ (φ \land \{m, X\} \in E) \to m \in D$
40	39	ad2ant2rl	$⊢ ((φ \land n \in N) \land (\{n, m\} \in E \land \{m, X\} \in E)) \to m \in D$
41	2	nbusgreledg	$⊢ G \in USGraph \to (n \in (G NeighbVtx m) \leftrightarrow \{n, m\} \in E)$
42	41	biimpar	$⊢ (G \in USGraph \land \{n, m\} \in E) \to n \in (G NeighbVtx m)$
43	42	a1d	$⊢ (G \in USGraph \land \{n, m\} \in E) \to (\{m, X\} \in E \to n \in (G NeighbVtx m))$
44	43	expimpd	$⊢ G \in USGraph \to ((\{n, m\} \in E \land \{m, X\} \in E) \to n \in (G NeighbVtx m))$
45	9 33 44	3syl	$⊢ φ \to ((\{n, m\} \in E \land \{m, X\} \in E) \to n \in (G NeighbVtx m))$
46	45	adantr	$⊢ (φ \land n \in N) \to ((\{n, m\} \in E \land \{m, X\} \in E) \to n \in (G NeighbVtx m))$
47	46	imp	$⊢ ((φ \land n \in N) \land (\{n, m\} \in E \land \{m, X\} \in E)) \to n \in (G NeighbVtx m)$
48		elin	$⊢ n \in ((G NeighbVtx m) \cap N) \leftrightarrow (n \in (G NeighbVtx m) \land n \in N)$
49		simpl	$⊢ (φ \land \{m, X\} \in E) \to φ$
50	49 39	jca	$⊢ (φ \land \{m, X\} \in E) \to (φ \land m \in D)$
51		preq1	$⊢ x = m \to \{x, y\} = \{m, y\}$
52	51	eleq1d	$⊢ x = m \to (\{x, y\} \in E \leftrightarrow \{m, y\} \in E)$
53	52	riotabidv	$⊢ x = m \to (ι y \in N \| \{x, y\} \in E) = (ι y \in N \| \{m, y\} \in E)$
54	53	cbvmptv	$⊢ (x \in D ⟼ (ι y \in N \| \{x, y\} \in E)) = (m \in D ⟼ (ι y \in N \| \{m, y\} \in E))$
55	10 54	eqtri	$⊢ A = (m \in D ⟼ (ι y \in N \| \{m, y\} \in E))$
56	1 2 3 4 5 6 7 8 9 55	frgrncvvdeqlem5	$⊢ (φ \land m \in D) \to \{A (m)\} = (G NeighbVtx m) \cap N$
57		eleq2	$⊢ (G NeighbVtx m) \cap N = \{A (m)\} \to (n \in ((G NeighbVtx m) \cap N) \leftrightarrow n \in \{A (m)\})$
58	57	eqcoms	$⊢ \{A (m)\} = (G NeighbVtx m) \cap N \to (n \in ((G NeighbVtx m) \cap N) \leftrightarrow n \in \{A (m)\})$
59		elsni	$⊢ n \in \{A (m)\} \to n = A (m)$
60	58 59	syl6bi	$⊢ \{A (m)\} = (G NeighbVtx m) \cap N \to (n \in ((G NeighbVtx m) \cap N) \to n = A (m))$
61	50 56 60	3syl	$⊢ (φ \land \{m, X\} \in E) \to (n \in ((G NeighbVtx m) \cap N) \to n = A (m))$
62	61	expcom	$⊢ \{m, X\} \in E \to (φ \to (n \in ((G NeighbVtx m) \cap N) \to n = A (m)))$
63	62	com3r	$⊢ n \in ((G NeighbVtx m) \cap N) \to (\{m, X\} \in E \to (φ \to n = A (m)))$
64	48 63	sylbir	$⊢ (n \in (G NeighbVtx m) \land n \in N) \to (\{m, X\} \in E \to (φ \to n = A (m)))$
65	64	ex	$⊢ n \in (G NeighbVtx m) \to (n \in N \to (\{m, X\} \in E \to (φ \to n = A (m))))$
66	65	com14	$⊢ φ \to (n \in N \to (\{m, X\} \in E \to (n \in (G NeighbVtx m) \to n = A (m))))$
67	66	imp	$⊢ (φ \land n \in N) \to (\{m, X\} \in E \to (n \in (G NeighbVtx m) \to n = A (m)))$
68	67	adantld	$⊢ (φ \land n \in N) \to ((\{n, m\} \in E \land \{m, X\} \in E) \to (n \in (G NeighbVtx m) \to n = A (m)))$
69	68	imp	$⊢ ((φ \land n \in N) \land (\{n, m\} \in E \land \{m, X\} \in E)) \to (n \in (G NeighbVtx m) \to n = A (m))$
70	47 69	mpd	$⊢ ((φ \land n \in N) \land (\{n, m\} \in E \land \{m, X\} \in E)) \to n = A (m)$
71	40 70	jca	$⊢ ((φ \land n \in N) \land (\{n, m\} \in E \land \{m, X\} \in E)) \to (m \in D \land n = A (m))$
72	71	ex	$⊢ (φ \land n \in N) \to ((\{n, m\} \in E \land \{m, X\} \in E) \to (m \in D \land n = A (m)))$
73	72	adantld	$⊢ (φ \land n \in N) \to ((m \in V \land (\{n, m\} \in E \land \{m, X\} \in E)) \to (m \in D \land n = A (m)))$
74	73	eximdv	$⊢ (φ \land n \in N) \to (\exists m (m \in V \land (\{n, m\} \in E \land \{m, X\} \in E)) \to \exists m (m \in D \land n = A (m)))$
75	32 74	mpd	$⊢ (φ \land n \in N) \to \exists m (m \in D \land n = A (m))$
76		df-rex	$⊢ \exists m \in D n = A (m) \leftrightarrow \exists m (m \in D \land n = A (m))$
77	75 76	sylibr	$⊢ (φ \land n \in N) \to \exists m \in D n = A (m)$
78	77	ralrimiva	$⊢ φ \to \forall n \in N \exists m \in D n = A (m)$
79		dffo3	$⊢ A : D \underset{onto}{⟶} N \leftrightarrow (A : D ⟶ N \land \forall n \in N \exists m \in D n = A (m))$
80	11 78 79	sylanbrc	$⊢ φ \to A : D \underset{onto}{⟶} N$

Metamath Proof Explorer

Theorem frgrncvvdeqlem9

Proof