frgrncvvdeqlem2

Description: Lemma 2 for frgrncvvdeq . In a friendship graph, for each neighbor of a vertex there is exactly one neighbor of another vertex so that there is an edge between these two neighbors. (Contributed by Alexander van der Vekens, 22-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	frgrncvvdeqlem2	$⊢ (φ \land x \in D) \to \exists! y \in N \{x, y\} \in E$

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	9	adantr	$⊢ (φ \land x \in D) \to G \in FriendGraph$
12	3	eleq2i	$⊢ x \in D \leftrightarrow x \in (G NeighbVtx X)$
13	1	nbgrisvtx	$⊢ x \in (G NeighbVtx X) \to x \in V$
14	13	a1i	$⊢ φ \to (x \in (G NeighbVtx X) \to x \in V)$
15	12 14	biimtrid	$⊢ φ \to (x \in D \to x \in V)$
16	15	imp	$⊢ (φ \land x \in D) \to x \in V$
17	6	adantr	$⊢ (φ \land x \in D) \to Y \in V$
18		elnelne2	$⊢ (x \in D \land Y \notin D) \to x \neq Y$
19	18	expcom	$⊢ Y \notin D \to (x \in D \to x \neq Y)$
20	8 19	syl	$⊢ φ \to (x \in D \to x \neq Y)$
21	20	imp	$⊢ (φ \land x \in D) \to x \neq Y$
22	16 17 21	3jca	$⊢ (φ \land x \in D) \to (x \in V \land Y \in V \land x \neq Y)$
23	1 2	frcond1	$⊢ G \in FriendGraph \to ((x \in V \land Y \in V \land x \neq Y) \to \exists! y \in V \{\{x, y\}, \{y, Y\}\} \subseteq E)$
24	11 22 23	sylc	$⊢ (φ \land x \in D) \to \exists! y \in V \{\{x, y\}, \{y, Y\}\} \subseteq E$
25		frgrusgr	$⊢ G \in FriendGraph \to G \in USGraph$
26		prex	$⊢ \{x, y\} \in V$
27		prex	$⊢ \{y, Y\} \in V$
28	26 27	prss	$⊢ (\{x, y\} \in E \land \{y, Y\} \in E) \leftrightarrow \{\{x, y\}, \{y, Y\}\} \subseteq E$
29		ancom	$⊢ (\{x, y\} \in E \land \{y, Y\} \in E) \leftrightarrow (\{y, Y\} \in E \land \{x, y\} \in E)$
30	28 29	bitr3i	$⊢ \{\{x, y\}, \{y, Y\}\} \subseteq E \leftrightarrow (\{y, Y\} \in E \land \{x, y\} \in E)$
31	30	anbi2i	$⊢ (y \in V \land \{\{x, y\}, \{y, Y\}\} \subseteq E) \leftrightarrow (y \in V \land (\{y, Y\} \in E \land \{x, y\} \in E))$
32		usgrumgr	$⊢ G \in USGraph \to G \in UMGraph$
33	1 2	umgrpredgv	$⊢ (G \in UMGraph \land \{x, y\} \in E) \to (x \in V \land y \in V)$
34	33	simprd	$⊢ (G \in UMGraph \land \{x, y\} \in E) \to y \in V$
35	34	ex	$⊢ G \in UMGraph \to (\{x, y\} \in E \to y \in V)$
36	32 35	syl	$⊢ G \in USGraph \to (\{x, y\} \in E \to y \in V)$
37	36	adantld	$⊢ G \in USGraph \to ((\{y, Y\} \in E \land \{x, y\} \in E) \to y \in V)$
38	37	pm4.71rd	$⊢ G \in USGraph \to ((\{y, Y\} \in E \land \{x, y\} \in E) \leftrightarrow (y \in V \land (\{y, Y\} \in E \land \{x, y\} \in E)))$
39	31 38	bitr4id	$⊢ G \in USGraph \to ((y \in V \land \{\{x, y\}, \{y, Y\}\} \subseteq E) \leftrightarrow (\{y, Y\} \in E \land \{x, y\} \in E))$
40	4	eleq2i	$⊢ y \in N \leftrightarrow y \in (G NeighbVtx Y)$
41	2	nbusgreledg	$⊢ G \in USGraph \to (y \in (G NeighbVtx Y) \leftrightarrow \{y, Y\} \in E)$
42	40 41	bitr2id	$⊢ G \in USGraph \to (\{y, Y\} \in E \leftrightarrow y \in N)$
43	42	anbi1d	$⊢ G \in USGraph \to ((\{y, Y\} \in E \land \{x, y\} \in E) \leftrightarrow (y \in N \land \{x, y\} \in E))$
44	39 43	bitrd	$⊢ G \in USGraph \to ((y \in V \land \{\{x, y\}, \{y, Y\}\} \subseteq E) \leftrightarrow (y \in N \land \{x, y\} \in E))$
45	44	eubidv	$⊢ G \in USGraph \to (\exists! y (y \in V \land \{\{x, y\}, \{y, Y\}\} \subseteq E) \leftrightarrow \exists! y (y \in N \land \{x, y\} \in E))$
46	45	biimpd	$⊢ G \in USGraph \to (\exists! y (y \in V \land \{\{x, y\}, \{y, Y\}\} \subseteq E) \to \exists! y (y \in N \land \{x, y\} \in E))$
47		df-reu	$⊢ \exists! y \in V \{\{x, y\}, \{y, Y\}\} \subseteq E \leftrightarrow \exists! y (y \in V \land \{\{x, y\}, \{y, Y\}\} \subseteq E)$
48		df-reu	$⊢ \exists! y \in N \{x, y\} \in E \leftrightarrow \exists! y (y \in N \land \{x, y\} \in E)$
49	46 47 48	3imtr4g	$⊢ G \in USGraph \to (\exists! y \in V \{\{x, y\}, \{y, Y\}\} \subseteq E \to \exists! y \in N \{x, y\} \in E)$
50	9 25 49	3syl	$⊢ φ \to (\exists! y \in V \{\{x, y\}, \{y, Y\}\} \subseteq E \to \exists! y \in N \{x, y\} \in E)$
51	50	adantr	$⊢ (φ \land x \in D) \to (\exists! y \in V \{\{x, y\}, \{y, Y\}\} \subseteq E \to \exists! y \in N \{x, y\} \in E)$
52	24 51	mpd	$⊢ (φ \land x \in D) \to \exists! y \in N \{x, y\} \in E$

Metamath Proof Explorer

Theorem frgrncvvdeqlem2

Proof