frgrnbnb

Description: If two neighbors U and W of a vertex X have a common neighbor A in a friendship graph, then this common neighbor A must be the vertex X . (Contributed by Alexander van der Vekens, 19-Dec-2017) (Revised by AV, 2-Apr-2021) (Proof shortened by AV, 13-Feb-2022)

	Ref	Expression
Hypotheses	frgrnbnb.e	$⊢ E = Edg (G)$
	frgrnbnb.n	$⊢ D = G NeighbVtx X$
Assertion	frgrnbnb	$⊢ (G \in FriendGraph \land (U \in D \land W \in D) \land U \neq W) \to ((\{U, A\} \in E \land \{W, A\} \in E) \to A = X)$

Proof

Step	Hyp	Ref	Expression
1		frgrnbnb.e	$⊢ E = Edg (G)$
2		frgrnbnb.n	$⊢ D = G NeighbVtx X$
3		frgrusgr	$⊢ G \in FriendGraph \to G \in USGraph$
4	2	eleq2i	$⊢ U \in D \leftrightarrow U \in (G NeighbVtx X)$
5	1	nbusgreledg	$⊢ G \in USGraph \to (U \in (G NeighbVtx X) \leftrightarrow \{U, X\} \in E)$
6	5	biimpd	$⊢ G \in USGraph \to (U \in (G NeighbVtx X) \to \{U, X\} \in E)$
7	4 6	biimtrid	$⊢ G \in USGraph \to (U \in D \to \{U, X\} \in E)$
8	2	eleq2i	$⊢ W \in D \leftrightarrow W \in (G NeighbVtx X)$
9	1	nbusgreledg	$⊢ G \in USGraph \to (W \in (G NeighbVtx X) \leftrightarrow \{W, X\} \in E)$
10	9	biimpd	$⊢ G \in USGraph \to (W \in (G NeighbVtx X) \to \{W, X\} \in E)$
11	8 10	biimtrid	$⊢ G \in USGraph \to (W \in D \to \{W, X\} \in E)$
12	7 11	anim12d	$⊢ G \in USGraph \to ((U \in D \land W \in D) \to (\{U, X\} \in E \land \{W, X\} \in E))$
13	12	imp	$⊢ (G \in USGraph \land (U \in D \land W \in D)) \to (\{U, X\} \in E \land \{W, X\} \in E)$
14		eqid	$⊢ Vtx (G) = Vtx (G)$
15	14	nbgrisvtx	$⊢ U \in (G NeighbVtx X) \to U \in Vtx (G)$
16	15 2	eleq2s	$⊢ U \in D \to U \in Vtx (G)$
17	14	nbgrisvtx	$⊢ W \in (G NeighbVtx X) \to W \in Vtx (G)$
18	17 2	eleq2s	$⊢ W \in D \to W \in Vtx (G)$
19	16 18	anim12i	$⊢ (U \in D \land W \in D) \to (U \in Vtx (G) \land W \in Vtx (G))$
20	19	adantl	$⊢ (G \in USGraph \land (U \in D \land W \in D)) \to (U \in Vtx (G) \land W \in Vtx (G))$
21	1 14	usgrpredgv	$⊢ (G \in USGraph \land \{U, A\} \in E) \to (U \in Vtx (G) \land A \in Vtx (G))$
22	21	ad2ant2r	$⊢ ((G \in USGraph \land (U \in D \land W \in D)) \land (\{U, A\} \in E \land \{W, A\} \in E)) \to (U \in Vtx (G) \land A \in Vtx (G))$
23		ax-1	$⊢ A = X \to (G \in FriendGraph \to A = X)$
24	23	2a1d	$⊢ A = X \to ((\{U, A\} \in E \land \{W, A\} \in E) \to (((X \in Vtx (G) \land A \in Vtx (G)) \land (U \in Vtx (G) \land W \in Vtx (G))) \to (G \in FriendGraph \to A = X)))$
25	24	2a1d	$⊢ A = X \to (U \neq W \to ((\{U, X\} \in E \land \{W, X\} \in E) \to ((\{U, A\} \in E \land \{W, A\} \in E) \to (((X \in Vtx (G) \land A \in Vtx (G)) \land (U \in Vtx (G) \land W \in Vtx (G))) \to (G \in FriendGraph \to A = X)))))$
26		simpll	$⊢ ((G \in USGraph \land ((X \in Vtx (G) \land A \in Vtx (G)) \land (U \in Vtx (G) \land W \in Vtx (G)))) \land (A \neq X \land U \neq W)) \to G \in USGraph$
27		simprrr	$⊢ (G \in USGraph \land ((X \in Vtx (G) \land A \in Vtx (G)) \land (U \in Vtx (G) \land W \in Vtx (G)))) \to W \in Vtx (G)$
28	27	adantr	$⊢ ((G \in USGraph \land ((X \in Vtx (G) \land A \in Vtx (G)) \land (U \in Vtx (G) \land W \in Vtx (G)))) \land (A \neq X \land U \neq W)) \to W \in Vtx (G)$
29		simprrl	$⊢ (G \in USGraph \land ((X \in Vtx (G) \land A \in Vtx (G)) \land (U \in Vtx (G) \land W \in Vtx (G)))) \to U \in Vtx (G)$
30	29	adantr	$⊢ ((G \in USGraph \land ((X \in Vtx (G) \land A \in Vtx (G)) \land (U \in Vtx (G) \land W \in Vtx (G)))) \land (A \neq X \land U \neq W)) \to U \in Vtx (G)$
31		necom	$⊢ U \neq W \leftrightarrow W \neq U$
32	31	biimpi	$⊢ U \neq W \to W \neq U$
33	32	adantl	$⊢ (A \neq X \land U \neq W) \to W \neq U$
34	33	adantl	$⊢ ((G \in USGraph \land ((X \in Vtx (G) \land A \in Vtx (G)) \land (U \in Vtx (G) \land W \in Vtx (G)))) \land (A \neq X \land U \neq W)) \to W \neq U$
35	28 30 34	3jca	$⊢ ((G \in USGraph \land ((X \in Vtx (G) \land A \in Vtx (G)) \land (U \in Vtx (G) \land W \in Vtx (G)))) \land (A \neq X \land U \neq W)) \to (W \in Vtx (G) \land U \in Vtx (G) \land W \neq U)$
36		simprll	$⊢ (G \in USGraph \land ((X \in Vtx (G) \land A \in Vtx (G)) \land (U \in Vtx (G) \land W \in Vtx (G)))) \to X \in Vtx (G)$
37	36	adantr	$⊢ ((G \in USGraph \land ((X \in Vtx (G) \land A \in Vtx (G)) \land (U \in Vtx (G) \land W \in Vtx (G)))) \land (A \neq X \land U \neq W)) \to X \in Vtx (G)$
38		simprlr	$⊢ (G \in USGraph \land ((X \in Vtx (G) \land A \in Vtx (G)) \land (U \in Vtx (G) \land W \in Vtx (G)))) \to A \in Vtx (G)$
39	38	adantr	$⊢ ((G \in USGraph \land ((X \in Vtx (G) \land A \in Vtx (G)) \land (U \in Vtx (G) \land W \in Vtx (G)))) \land (A \neq X \land U \neq W)) \to A \in Vtx (G)$
40		necom	$⊢ A \neq X \leftrightarrow X \neq A$
41	40	biimpi	$⊢ A \neq X \to X \neq A$
42	41	adantr	$⊢ (A \neq X \land U \neq W) \to X \neq A$
43	42	adantl	$⊢ ((G \in USGraph \land ((X \in Vtx (G) \land A \in Vtx (G)) \land (U \in Vtx (G) \land W \in Vtx (G)))) \land (A \neq X \land U \neq W)) \to X \neq A$
44	37 39 43	3jca	$⊢ ((G \in USGraph \land ((X \in Vtx (G) \land A \in Vtx (G)) \land (U \in Vtx (G) \land W \in Vtx (G)))) \land (A \neq X \land U \neq W)) \to (X \in Vtx (G) \land A \in Vtx (G) \land X \neq A)$
45	26 35 44	3jca	$⊢ ((G \in USGraph \land ((X \in Vtx (G) \land A \in Vtx (G)) \land (U \in Vtx (G) \land W \in Vtx (G)))) \land (A \neq X \land U \neq W)) \to (G \in USGraph \land (W \in Vtx (G) \land U \in Vtx (G) \land W \neq U) \land (X \in Vtx (G) \land A \in Vtx (G) \land X \neq A))$
46	45	ad4ant14	$⊢ ((((G \in USGraph \land ((X \in Vtx (G) \land A \in Vtx (G)) \land (U \in Vtx (G) \land W \in Vtx (G)))) \land (\{U, X\} \in E \land \{W, X\} \in E)) \land (\{U, A\} \in E \land \{W, A\} \in E)) \land (A \neq X \land U \neq W)) \to (G \in USGraph \land (W \in Vtx (G) \land U \in Vtx (G) \land W \neq U) \land (X \in Vtx (G) \land A \in Vtx (G) \land X \neq A))$
47		prcom	$⊢ \{U, X\} = \{X, U\}$
48	47	eleq1i	$⊢ \{U, X\} \in E \leftrightarrow \{X, U\} \in E$
49	48	biimpi	$⊢ \{U, X\} \in E \to \{X, U\} \in E$
50	49	anim1ci	$⊢ (\{U, X\} \in E \land \{W, X\} \in E) \to (\{W, X\} \in E \land \{X, U\} \in E)$
51	50	adantl	$⊢ ((G \in USGraph \land ((X \in Vtx (G) \land A \in Vtx (G)) \land (U \in Vtx (G) \land W \in Vtx (G)))) \land (\{U, X\} \in E \land \{W, X\} \in E)) \to (\{W, X\} \in E \land \{X, U\} \in E)$
52		prcom	$⊢ \{W, A\} = \{A, W\}$
53	52	eleq1i	$⊢ \{W, A\} \in E \leftrightarrow \{A, W\} \in E$
54	53	biimpi	$⊢ \{W, A\} \in E \to \{A, W\} \in E$
55	54	anim2i	$⊢ (\{U, A\} \in E \land \{W, A\} \in E) \to (\{U, A\} \in E \land \{A, W\} \in E)$
56	51 55	anim12i	$⊢ (((G \in USGraph \land ((X \in Vtx (G) \land A \in Vtx (G)) \land (U \in Vtx (G) \land W \in Vtx (G)))) \land (\{U, X\} \in E \land \{W, X\} \in E)) \land (\{U, A\} \in E \land \{W, A\} \in E)) \to ((\{W, X\} \in E \land \{X, U\} \in E) \land (\{U, A\} \in E \land \{A, W\} \in E))$
57	56	adantr	$⊢ ((((G \in USGraph \land ((X \in Vtx (G) \land A \in Vtx (G)) \land (U \in Vtx (G) \land W \in Vtx (G)))) \land (\{U, X\} \in E \land \{W, X\} \in E)) \land (\{U, A\} \in E \land \{W, A\} \in E)) \land (A \neq X \land U \neq W)) \to ((\{W, X\} \in E \land \{X, U\} \in E) \land (\{U, A\} \in E \land \{A, W\} \in E))$
58	14 1	4cyclusnfrgr	$⊢ (G \in USGraph \land (W \in Vtx (G) \land U \in Vtx (G) \land W \neq U) \land (X \in Vtx (G) \land A \in Vtx (G) \land X \neq A)) \to (((\{W, X\} \in E \land \{X, U\} \in E) \land (\{U, A\} \in E \land \{A, W\} \in E)) \to G \notin FriendGraph)$
59	46 57 58	sylc	$⊢ ((((G \in USGraph \land ((X \in Vtx (G) \land A \in Vtx (G)) \land (U \in Vtx (G) \land W \in Vtx (G)))) \land (\{U, X\} \in E \land \{W, X\} \in E)) \land (\{U, A\} \in E \land \{W, A\} \in E)) \land (A \neq X \land U \neq W)) \to G \notin FriendGraph$
60		df-nel	$⊢ G \notin FriendGraph \leftrightarrow \neg G \in FriendGraph$
61	59 60	sylib	$⊢ ((((G \in USGraph \land ((X \in Vtx (G) \land A \in Vtx (G)) \land (U \in Vtx (G) \land W \in Vtx (G)))) \land (\{U, X\} \in E \land \{W, X\} \in E)) \land (\{U, A\} \in E \land \{W, A\} \in E)) \land (A \neq X \land U \neq W)) \to \neg G \in FriendGraph$
62	61	pm2.21d	$⊢ ((((G \in USGraph \land ((X \in Vtx (G) \land A \in Vtx (G)) \land (U \in Vtx (G) \land W \in Vtx (G)))) \land (\{U, X\} \in E \land \{W, X\} \in E)) \land (\{U, A\} \in E \land \{W, A\} \in E)) \land (A \neq X \land U \neq W)) \to (G \in FriendGraph \to A = X)$
63	62	ex	$⊢ (((G \in USGraph \land ((X \in Vtx (G) \land A \in Vtx (G)) \land (U \in Vtx (G) \land W \in Vtx (G)))) \land (\{U, X\} \in E \land \{W, X\} \in E)) \land (\{U, A\} \in E \land \{W, A\} \in E)) \to ((A \neq X \land U \neq W) \to (G \in FriendGraph \to A = X))$
64	63	com23	$⊢ (((G \in USGraph \land ((X \in Vtx (G) \land A \in Vtx (G)) \land (U \in Vtx (G) \land W \in Vtx (G)))) \land (\{U, X\} \in E \land \{W, X\} \in E)) \land (\{U, A\} \in E \land \{W, A\} \in E)) \to (G \in FriendGraph \to ((A \neq X \land U \neq W) \to A = X))$
65	64	exp41	$⊢ G \in USGraph \to (((X \in Vtx (G) \land A \in Vtx (G)) \land (U \in Vtx (G) \land W \in Vtx (G))) \to ((\{U, X\} \in E \land \{W, X\} \in E) \to ((\{U, A\} \in E \land \{W, A\} \in E) \to (G \in FriendGraph \to ((A \neq X \land U \neq W) \to A = X)))))$
66	65	com25	$⊢ G \in USGraph \to (G \in FriendGraph \to ((\{U, X\} \in E \land \{W, X\} \in E) \to ((\{U, A\} \in E \land \{W, A\} \in E) \to (((X \in Vtx (G) \land A \in Vtx (G)) \land (U \in Vtx (G) \land W \in Vtx (G))) \to ((A \neq X \land U \neq W) \to A = X)))))$
67	3 66	mpcom	$⊢ G \in FriendGraph \to ((\{U, X\} \in E \land \{W, X\} \in E) \to ((\{U, A\} \in E \land \{W, A\} \in E) \to (((X \in Vtx (G) \land A \in Vtx (G)) \land (U \in Vtx (G) \land W \in Vtx (G))) \to ((A \neq X \land U \neq W) \to A = X))))$
68	67	com15	$⊢ (A \neq X \land U \neq W) \to ((\{U, X\} \in E \land \{W, X\} \in E) \to ((\{U, A\} \in E \land \{W, A\} \in E) \to (((X \in Vtx (G) \land A \in Vtx (G)) \land (U \in Vtx (G) \land W \in Vtx (G))) \to (G \in FriendGraph \to A = X))))$
69	68	ex	$⊢ A \neq X \to (U \neq W \to ((\{U, X\} \in E \land \{W, X\} \in E) \to ((\{U, A\} \in E \land \{W, A\} \in E) \to (((X \in Vtx (G) \land A \in Vtx (G)) \land (U \in Vtx (G) \land W \in Vtx (G))) \to (G \in FriendGraph \to A = X)))))$
70	25 69	pm2.61ine	$⊢ U \neq W \to ((\{U, X\} \in E \land \{W, X\} \in E) \to ((\{U, A\} \in E \land \{W, A\} \in E) \to (((X \in Vtx (G) \land A \in Vtx (G)) \land (U \in Vtx (G) \land W \in Vtx (G))) \to (G \in FriendGraph \to A = X))))$
71	70	imp	$⊢ (U \neq W \land (\{U, X\} \in E \land \{W, X\} \in E)) \to ((\{U, A\} \in E \land \{W, A\} \in E) \to (((X \in Vtx (G) \land A \in Vtx (G)) \land (U \in Vtx (G) \land W \in Vtx (G))) \to (G \in FriendGraph \to A = X)))$
72	71	com13	$⊢ ((X \in Vtx (G) \land A \in Vtx (G)) \land (U \in Vtx (G) \land W \in Vtx (G))) \to ((\{U, A\} \in E \land \{W, A\} \in E) \to ((U \neq W \land (\{U, X\} \in E \land \{W, X\} \in E)) \to (G \in FriendGraph \to A = X)))$
73	72	ex	$⊢ (X \in Vtx (G) \land A \in Vtx (G)) \to ((U \in Vtx (G) \land W \in Vtx (G)) \to ((\{U, A\} \in E \land \{W, A\} \in E) \to ((U \neq W \land (\{U, X\} \in E \land \{W, X\} \in E)) \to (G \in FriendGraph \to A = X))))$
74	73	com25	$⊢ (X \in Vtx (G) \land A \in Vtx (G)) \to (G \in FriendGraph \to ((\{U, A\} \in E \land \{W, A\} \in E) \to ((U \neq W \land (\{U, X\} \in E \land \{W, X\} \in E)) \to ((U \in Vtx (G) \land W \in Vtx (G)) \to A = X))))$
75	74	ex	$⊢ X \in Vtx (G) \to (A \in Vtx (G) \to (G \in FriendGraph \to ((\{U, A\} \in E \land \{W, A\} \in E) \to ((U \neq W \land (\{U, X\} \in E \land \{W, X\} \in E)) \to ((U \in Vtx (G) \land W \in Vtx (G)) \to A = X)))))$
76	14	nbgrcl	$⊢ U \in (G NeighbVtx X) \to X \in Vtx (G)$
77	76 2	eleq2s	$⊢ U \in D \to X \in Vtx (G)$
78	77	adantr	$⊢ (U \in D \land W \in D) \to X \in Vtx (G)$
79	78	adantl	$⊢ (G \in USGraph \land (U \in D \land W \in D)) \to X \in Vtx (G)$
80	75 79	syl11	$⊢ A \in Vtx (G) \to ((G \in USGraph \land (U \in D \land W \in D)) \to (G \in FriendGraph \to ((\{U, A\} \in E \land \{W, A\} \in E) \to ((U \neq W \land (\{U, X\} \in E \land \{W, X\} \in E)) \to ((U \in Vtx (G) \land W \in Vtx (G)) \to A = X)))))$
81	80	com34	$⊢ A \in Vtx (G) \to ((G \in USGraph \land (U \in D \land W \in D)) \to ((\{U, A\} \in E \land \{W, A\} \in E) \to (G \in FriendGraph \to ((U \neq W \land (\{U, X\} \in E \land \{W, X\} \in E)) \to ((U \in Vtx (G) \land W \in Vtx (G)) \to A = X)))))$
82	81	impd	$⊢ A \in Vtx (G) \to (((G \in USGraph \land (U \in D \land W \in D)) \land (\{U, A\} \in E \land \{W, A\} \in E)) \to (G \in FriendGraph \to ((U \neq W \land (\{U, X\} \in E \land \{W, X\} \in E)) \to ((U \in Vtx (G) \land W \in Vtx (G)) \to A = X))))$
83	82	adantl	$⊢ (U \in Vtx (G) \land A \in Vtx (G)) \to (((G \in USGraph \land (U \in D \land W \in D)) \land (\{U, A\} \in E \land \{W, A\} \in E)) \to (G \in FriendGraph \to ((U \neq W \land (\{U, X\} \in E \land \{W, X\} \in E)) \to ((U \in Vtx (G) \land W \in Vtx (G)) \to A = X))))$
84	22 83	mpcom	$⊢ ((G \in USGraph \land (U \in D \land W \in D)) \land (\{U, A\} \in E \land \{W, A\} \in E)) \to (G \in FriendGraph \to ((U \neq W \land (\{U, X\} \in E \land \{W, X\} \in E)) \to ((U \in Vtx (G) \land W \in Vtx (G)) \to A = X)))$
85	84	ex	$⊢ (G \in USGraph \land (U \in D \land W \in D)) \to ((\{U, A\} \in E \land \{W, A\} \in E) \to (G \in FriendGraph \to ((U \neq W \land (\{U, X\} \in E \land \{W, X\} \in E)) \to ((U \in Vtx (G) \land W \in Vtx (G)) \to A = X))))$
86	85	com25	$⊢ (G \in USGraph \land (U \in D \land W \in D)) \to ((U \in Vtx (G) \land W \in Vtx (G)) \to (G \in FriendGraph \to ((U \neq W \land (\{U, X\} \in E \land \{W, X\} \in E)) \to ((\{U, A\} \in E \land \{W, A\} \in E) \to A = X))))$
87	86	com14	$⊢ (U \neq W \land (\{U, X\} \in E \land \{W, X\} \in E)) \to ((U \in Vtx (G) \land W \in Vtx (G)) \to (G \in FriendGraph \to ((G \in USGraph \land (U \in D \land W \in D)) \to ((\{U, A\} \in E \land \{W, A\} \in E) \to A = X))))$
88	87	ex	$⊢ U \neq W \to ((\{U, X\} \in E \land \{W, X\} \in E) \to ((U \in Vtx (G) \land W \in Vtx (G)) \to (G \in FriendGraph \to ((G \in USGraph \land (U \in D \land W \in D)) \to ((\{U, A\} \in E \land \{W, A\} \in E) \to A = X)))))$
89	88	com15	$⊢ (G \in USGraph \land (U \in D \land W \in D)) \to ((\{U, X\} \in E \land \{W, X\} \in E) \to ((U \in Vtx (G) \land W \in Vtx (G)) \to (G \in FriendGraph \to (U \neq W \to ((\{U, A\} \in E \land \{W, A\} \in E) \to A = X)))))$
90	13 20 89	mp2d	$⊢ (G \in USGraph \land (U \in D \land W \in D)) \to (G \in FriendGraph \to (U \neq W \to ((\{U, A\} \in E \land \{W, A\} \in E) \to A = X)))$
91	90	ex	$⊢ G \in USGraph \to ((U \in D \land W \in D) \to (G \in FriendGraph \to (U \neq W \to ((\{U, A\} \in E \land \{W, A\} \in E) \to A = X))))$
92	91	com23	$⊢ G \in USGraph \to (G \in FriendGraph \to ((U \in D \land W \in D) \to (U \neq W \to ((\{U, A\} \in E \land \{W, A\} \in E) \to A = X))))$
93	3 92	mpcom	$⊢ G \in FriendGraph \to ((U \in D \land W \in D) \to (U \neq W \to ((\{U, A\} \in E \land \{W, A\} \in E) \to A = X)))$
94	93	3imp	$⊢ (G \in FriendGraph \land (U \in D \land W \in D) \land U \neq W) \to ((\{U, A\} \in E \land \{W, A\} \in E) \to A = X)$

Metamath Proof Explorer

Theorem frgrnbnb

Proof