Theorem 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	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	frgrncvvdeq.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
	frgrncvvdeq.nx	⊢ 𝐷 = ( 𝐺 NeighbVtx 𝑋 )
	frgrncvvdeq.ny	⊢ 𝑁 = ( 𝐺 NeighbVtx 𝑌 )
	frgrncvvdeq.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
	frgrncvvdeq.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
	frgrncvvdeq.ne	⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
	frgrncvvdeq.xy	⊢ ( 𝜑 → 𝑌 ∉ 𝐷 )
	frgrncvvdeq.f	⊢ ( 𝜑 → 𝐺 ∈ FriendGraph )
	frgrncvvdeq.a	⊢ 𝐴 = ( 𝑥 ∈ 𝐷 ↦ ( ℩ 𝑦 ∈ 𝑁 { 𝑥 , 𝑦 } ∈ 𝐸 ) )
Assertion	frgrncvvdeqlem2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ∃! 𝑦 ∈ 𝑁 { 𝑥 , 𝑦 } ∈ 𝐸 )

Proof

Step	Hyp	Ref	Expression
1		frgrncvvdeq.v1	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		frgrncvvdeq.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
3		frgrncvvdeq.nx	⊢ 𝐷 = ( 𝐺 NeighbVtx 𝑋 )
4		frgrncvvdeq.ny	⊢ 𝑁 = ( 𝐺 NeighbVtx 𝑌 )
5		frgrncvvdeq.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
6		frgrncvvdeq.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
7		frgrncvvdeq.ne	⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
8		frgrncvvdeq.xy	⊢ ( 𝜑 → 𝑌 ∉ 𝐷 )
9		frgrncvvdeq.f	⊢ ( 𝜑 → 𝐺 ∈ FriendGraph )
10		frgrncvvdeq.a	⊢ 𝐴 = ( 𝑥 ∈ 𝐷 ↦ ( ℩ 𝑦 ∈ 𝑁 { 𝑥 , 𝑦 } ∈ 𝐸 ) )
11	9	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝐺 ∈ FriendGraph )
12	3	eleq2i	⊢ ( 𝑥 ∈ 𝐷 ↔ 𝑥 ∈ ( 𝐺 NeighbVtx 𝑋 ) )
13	1	nbgrisvtx	⊢ ( 𝑥 ∈ ( 𝐺 NeighbVtx 𝑋 ) → 𝑥 ∈ 𝑉 )
14	13	a1i	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐺 NeighbVtx 𝑋 ) → 𝑥 ∈ 𝑉 ) )
15	12 14	syl5bi	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐷 → 𝑥 ∈ 𝑉 ) )
16	15	imp	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝑥 ∈ 𝑉 )
17	6	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝑌 ∈ 𝑉 )
18		elnelne2	⊢ ( ( 𝑥 ∈ 𝐷 ∧ 𝑌 ∉ 𝐷 ) → 𝑥 ≠ 𝑌 )
19	18	expcom	⊢ ( 𝑌 ∉ 𝐷 → ( 𝑥 ∈ 𝐷 → 𝑥 ≠ 𝑌 ) )
20	8 19	syl	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐷 → 𝑥 ≠ 𝑌 ) )
21	20	imp	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝑥 ≠ 𝑌 )
22	16 17 21	3jca	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝑥 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑥 ≠ 𝑌 ) )
23	1 2	frcond1	⊢ ( 𝐺 ∈ FriendGraph → ( ( 𝑥 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑥 ≠ 𝑌 ) → ∃! 𝑦 ∈ 𝑉 { { 𝑥 , 𝑦 } , { 𝑦 , 𝑌 } } ⊆ 𝐸 ) )
24	11 22 23	sylc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ∃! 𝑦 ∈ 𝑉 { { 𝑥 , 𝑦 } , { 𝑦 , 𝑌 } } ⊆ 𝐸 )
25		frgrusgr	⊢ ( 𝐺 ∈ FriendGraph → 𝐺 ∈ USGraph )
26		usgrumgr	⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ UMGraph )
27	1 2	umgrpredgv	⊢ ( ( 𝐺 ∈ UMGraph ∧ { 𝑥 , 𝑦 } ∈ 𝐸 ) → ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) )
28	27	simprd	⊢ ( ( 𝐺 ∈ UMGraph ∧ { 𝑥 , 𝑦 } ∈ 𝐸 ) → 𝑦 ∈ 𝑉 )
29	28	ex	⊢ ( 𝐺 ∈ UMGraph → ( { 𝑥 , 𝑦 } ∈ 𝐸 → 𝑦 ∈ 𝑉 ) )
30	26 29	syl	⊢ ( 𝐺 ∈ USGraph → ( { 𝑥 , 𝑦 } ∈ 𝐸 → 𝑦 ∈ 𝑉 ) )
31	30	adantld	⊢ ( 𝐺 ∈ USGraph → ( ( { 𝑦 , 𝑌 } ∈ 𝐸 ∧ { 𝑥 , 𝑦 } ∈ 𝐸 ) → 𝑦 ∈ 𝑉 ) )
32	31	pm4.71rd	⊢ ( 𝐺 ∈ USGraph → ( ( { 𝑦 , 𝑌 } ∈ 𝐸 ∧ { 𝑥 , 𝑦 } ∈ 𝐸 ) ↔ ( 𝑦 ∈ 𝑉 ∧ ( { 𝑦 , 𝑌 } ∈ 𝐸 ∧ { 𝑥 , 𝑦 } ∈ 𝐸 ) ) ) )
33		prex	⊢ { 𝑥 , 𝑦 } ∈ V
34		prex	⊢ { 𝑦 , 𝑌 } ∈ V
35	33 34	prss	⊢ ( ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑌 } ∈ 𝐸 ) ↔ { { 𝑥 , 𝑦 } , { 𝑦 , 𝑌 } } ⊆ 𝐸 )
36		ancom	⊢ ( ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑌 } ∈ 𝐸 ) ↔ ( { 𝑦 , 𝑌 } ∈ 𝐸 ∧ { 𝑥 , 𝑦 } ∈ 𝐸 ) )
37	35 36	bitr3i	⊢ ( { { 𝑥 , 𝑦 } , { 𝑦 , 𝑌 } } ⊆ 𝐸 ↔ ( { 𝑦 , 𝑌 } ∈ 𝐸 ∧ { 𝑥 , 𝑦 } ∈ 𝐸 ) )
38	37	anbi2i	⊢ ( ( 𝑦 ∈ 𝑉 ∧ { { 𝑥 , 𝑦 } , { 𝑦 , 𝑌 } } ⊆ 𝐸 ) ↔ ( 𝑦 ∈ 𝑉 ∧ ( { 𝑦 , 𝑌 } ∈ 𝐸 ∧ { 𝑥 , 𝑦 } ∈ 𝐸 ) ) )
39	32 38	syl6rbbr	⊢ ( 𝐺 ∈ USGraph → ( ( 𝑦 ∈ 𝑉 ∧ { { 𝑥 , 𝑦 } , { 𝑦 , 𝑌 } } ⊆ 𝐸 ) ↔ ( { 𝑦 , 𝑌 } ∈ 𝐸 ∧ { 𝑥 , 𝑦 } ∈ 𝐸 ) ) )
40	4	eleq2i	⊢ ( 𝑦 ∈ 𝑁 ↔ 𝑦 ∈ ( 𝐺 NeighbVtx 𝑌 ) )
41	2	nbusgreledg	⊢ ( 𝐺 ∈ USGraph → ( 𝑦 ∈ ( 𝐺 NeighbVtx 𝑌 ) ↔ { 𝑦 , 𝑌 } ∈ 𝐸 ) )
42	40 41	syl5rbb	⊢ ( 𝐺 ∈ USGraph → ( { 𝑦 , 𝑌 } ∈ 𝐸 ↔ 𝑦 ∈ 𝑁 ) )
43	42	anbi1d	⊢ ( 𝐺 ∈ USGraph → ( ( { 𝑦 , 𝑌 } ∈ 𝐸 ∧ { 𝑥 , 𝑦 } ∈ 𝐸 ) ↔ ( 𝑦 ∈ 𝑁 ∧ { 𝑥 , 𝑦 } ∈ 𝐸 ) ) )
44	39 43	bitrd	⊢ ( 𝐺 ∈ USGraph → ( ( 𝑦 ∈ 𝑉 ∧ { { 𝑥 , 𝑦 } , { 𝑦 , 𝑌 } } ⊆ 𝐸 ) ↔ ( 𝑦 ∈ 𝑁 ∧ { 𝑥 , 𝑦 } ∈ 𝐸 ) ) )
45	44	eubidv	⊢ ( 𝐺 ∈ USGraph → ( ∃! 𝑦 ( 𝑦 ∈ 𝑉 ∧ { { 𝑥 , 𝑦 } , { 𝑦 , 𝑌 } } ⊆ 𝐸 ) ↔ ∃! 𝑦 ( 𝑦 ∈ 𝑁 ∧ { 𝑥 , 𝑦 } ∈ 𝐸 ) ) )
46	45	biimpd	⊢ ( 𝐺 ∈ USGraph → ( ∃! 𝑦 ( 𝑦 ∈ 𝑉 ∧ { { 𝑥 , 𝑦 } , { 𝑦 , 𝑌 } } ⊆ 𝐸 ) → ∃! 𝑦 ( 𝑦 ∈ 𝑁 ∧ { 𝑥 , 𝑦 } ∈ 𝐸 ) ) )
47		df-reu	⊢ ( ∃! 𝑦 ∈ 𝑉 { { 𝑥 , 𝑦 } , { 𝑦 , 𝑌 } } ⊆ 𝐸 ↔ ∃! 𝑦 ( 𝑦 ∈ 𝑉 ∧ { { 𝑥 , 𝑦 } , { 𝑦 , 𝑌 } } ⊆ 𝐸 ) )
48		df-reu	⊢ ( ∃! 𝑦 ∈ 𝑁 { 𝑥 , 𝑦 } ∈ 𝐸 ↔ ∃! 𝑦 ( 𝑦 ∈ 𝑁 ∧ { 𝑥 , 𝑦 } ∈ 𝐸 ) )
49	46 47 48	3imtr4g	⊢ ( 𝐺 ∈ USGraph → ( ∃! 𝑦 ∈ 𝑉 { { 𝑥 , 𝑦 } , { 𝑦 , 𝑌 } } ⊆ 𝐸 → ∃! 𝑦 ∈ 𝑁 { 𝑥 , 𝑦 } ∈ 𝐸 ) )
50	9 25 49	3syl	⊢ ( 𝜑 → ( ∃! 𝑦 ∈ 𝑉 { { 𝑥 , 𝑦 } , { 𝑦 , 𝑌 } } ⊆ 𝐸 → ∃! 𝑦 ∈ 𝑁 { 𝑥 , 𝑦 } ∈ 𝐸 ) )
51	50	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ∃! 𝑦 ∈ 𝑉 { { 𝑥 , 𝑦 } , { 𝑦 , 𝑌 } } ⊆ 𝐸 → ∃! 𝑦 ∈ 𝑁 { 𝑥 , 𝑦 } ∈ 𝐸 ) )
52	24 51	mpd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ∃! 𝑦 ∈ 𝑁 { 𝑥 , 𝑦 } ∈ 𝐸 )