Theorem frgrncvvdeqlem3 30393

Description: Lemma 3 for frgrncvvdeq 30401. The unique neighbor of a vertex (expressed by a restricted iota) is the intersection of the corresponding neighborhoods. (Contributed by Alexander van der Vekens, 18-Dec-2017.) (Revised by AV, 10-May-2021.) (Proof shortened by AV, 12-Feb-2022.)

Hypotheses

Ref	Expression
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

Ref	Expression
frgrncvvdeqlem3	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → {(℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)} = ((𝐺 NeighbVtx 𝑥) ∩ 𝑁))

Distinct variable groups:   𝑦,𝐸   𝑦,𝐺   𝑦,𝑉   𝑦,𝑌   𝑥,𝑦   𝑦,𝑁

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐴(𝑥,𝑦)   𝐷(𝑥,𝑦)   𝐸(𝑥)   𝐺(𝑥)   𝑁(𝑥)   𝑉(𝑥)   𝑋(𝑥,𝑦)   𝑌(𝑥)

Proof of Theorem frgrncvvdeqlem3

Dummy variable 𝑛 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		frgrncvvdeq.ny	. . 3 ⊢ 𝑁 = (𝐺 NeighbVtx 𝑌)
2	1	ineq2i 4149	. 2 ⊢ ((𝐺 NeighbVtx 𝑥) ∩ 𝑁) = ((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌))
3		frgrncvvdeq.f	. . . . 5 ⊢ (𝜑 → 𝐺 ∈ FriendGraph )
4	3	adantr 482	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐺 ∈ FriendGraph )
5		frgrncvvdeq.nx	. . . . . . . 8 ⊢ 𝐷 = (𝐺 NeighbVtx 𝑋)
6	5	eleq2i 2833	. . . . . . 7 ⊢ (𝑥 ∈ 𝐷 ↔ 𝑥 ∈ (𝐺 NeighbVtx 𝑋))
7		frgrncvvdeq.v1	. . . . . . . . 9 ⊢ 𝑉 = (Vtx‘𝐺)
8	7	nbgrisvtx 29432	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐺 NeighbVtx 𝑋) → 𝑥 ∈ 𝑉)
9	8	a1i 11	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (𝐺 NeighbVtx 𝑋) → 𝑥 ∈ 𝑉))
10	6, 9	biimtrid 244	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐷 → 𝑥 ∈ 𝑉))
11	10	imp 408	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝑥 ∈ 𝑉)
12		frgrncvvdeq.y	. . . . . 6 ⊢ (𝜑 → 𝑌 ∈ 𝑉)
13	12	adantr 482	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝑌 ∈ 𝑉)
14		frgrncvvdeq.xy	. . . . . . 7 ⊢ (𝜑 → 𝑌 ∉ 𝐷)
15		elnelne2 3052	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐷 ∧ 𝑌 ∉ 𝐷) → 𝑥 ≠ 𝑌)
16	14, 15	sylan2 600	. . . . . 6 ⊢ ((𝑥 ∈ 𝐷 ∧ 𝜑) → 𝑥 ≠ 𝑌)
17	16	ancoms 460	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝑥 ≠ 𝑌)
18	11, 13, 17	3jca 1135	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝑥 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑥 ≠ 𝑌))
19		frgrncvvdeq.e	. . . . 5 ⊢ 𝐸 = (Edg‘𝐺)
20	7, 19	frcond3 30361	. . . 4 ⊢ (𝐺 ∈ FriendGraph → ((𝑥 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑥 ≠ 𝑌) → ∃𝑛 ∈ 𝑉 ((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)) = {𝑛}))
21	4, 18, 20	sylc 65	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ∃𝑛 ∈ 𝑉 ((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)) = {𝑛})
22		vex 3437	. . . . . . . . . 10 ⊢ 𝑛 ∈ V
23		elinsn 4645	. . . . . . . . . 10 ⊢ ((𝑛 ∈ V ∧ ((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)) = {𝑛}) → (𝑛 ∈ (𝐺 NeighbVtx 𝑥) ∧ 𝑛 ∈ (𝐺 NeighbVtx 𝑌)))
24	22, 23	mpan 697	. . . . . . . . 9 ⊢ (((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)) = {𝑛} → (𝑛 ∈ (𝐺 NeighbVtx 𝑥) ∧ 𝑛 ∈ (𝐺 NeighbVtx 𝑌)))
25		frgrusgr 30353	. . . . . . . . . . . . . . 15 ⊢ (𝐺 ∈ FriendGraph → 𝐺 ∈ USGraph)
26	19	nbusgreledg 29444	. . . . . . . . . . . . . . . . 17 ⊢ (𝐺 ∈ USGraph → (𝑛 ∈ (𝐺 NeighbVtx 𝑥) ↔ {𝑛, 𝑥} ∈ 𝐸))
27		prcom 4667	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑛, 𝑥} = {𝑥, 𝑛}
28	27	eleq1i 2832	. . . . . . . . . . . . . . . . 17 ⊢ ({𝑛, 𝑥} ∈ 𝐸 ↔ {𝑥, 𝑛} ∈ 𝐸)
29	26, 28	bitrdi 289	. . . . . . . . . . . . . . . 16 ⊢ (𝐺 ∈ USGraph → (𝑛 ∈ (𝐺 NeighbVtx 𝑥) ↔ {𝑥, 𝑛} ∈ 𝐸))
30	29	biimpd 231	. . . . . . . . . . . . . . 15 ⊢ (𝐺 ∈ USGraph → (𝑛 ∈ (𝐺 NeighbVtx 𝑥) → {𝑥, 𝑛} ∈ 𝐸))
31	3, 25, 30	3syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑛 ∈ (𝐺 NeighbVtx 𝑥) → {𝑥, 𝑛} ∈ 𝐸))
32	31	adantr 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝑛 ∈ (𝐺 NeighbVtx 𝑥) → {𝑥, 𝑛} ∈ 𝐸))
33	32	com12 32	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ (𝐺 NeighbVtx 𝑥) → ((𝜑 ∧ 𝑥 ∈ 𝐷) → {𝑥, 𝑛} ∈ 𝐸))
34	33	adantr 482	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ (𝐺 NeighbVtx 𝑥) ∧ 𝑛 ∈ (𝐺 NeighbVtx 𝑌)) → ((𝜑 ∧ 𝑥 ∈ 𝐷) → {𝑥, 𝑛} ∈ 𝐸))
35	34	imp 408	. . . . . . . . . 10 ⊢ (((𝑛 ∈ (𝐺 NeighbVtx 𝑥) ∧ 𝑛 ∈ (𝐺 NeighbVtx 𝑌)) ∧ (𝜑 ∧ 𝑥 ∈ 𝐷)) → {𝑥, 𝑛} ∈ 𝐸)
36	1	eqcomi 2750	. . . . . . . . . . . . 13 ⊢ (𝐺 NeighbVtx 𝑌) = 𝑁
37	36	eleq2i 2833	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ (𝐺 NeighbVtx 𝑌) ↔ 𝑛 ∈ 𝑁)
38	37	bilani 506	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ (𝐺 NeighbVtx 𝑥) ∧ 𝑛 ∈ (𝐺 NeighbVtx 𝑌)) → 𝑛 ∈ 𝑁)
39		frgrncvvdeq.x	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑋 ∈ 𝑉)
40		frgrncvvdeq.ne	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑋 ≠ 𝑌)
41		frgrncvvdeq.a	. . . . . . . . . . . 12 ⊢ 𝐴 = (𝑥 ∈ 𝐷 ↦ (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸))
42	7, 19, 5, 1, 39, 12, 40, 14, 3, 41	frgrncvvdeqlem2 30392	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ∃!𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)
43		preq2 4669	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑛 → {𝑥, 𝑦} = {𝑥, 𝑛})
44	43	eleq1d 2826	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑛 → ({𝑥, 𝑦} ∈ 𝐸 ↔ {𝑥, 𝑛} ∈ 𝐸))
45	44	riota2 7342	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ 𝑁 ∧ ∃!𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸) → ({𝑥, 𝑛} ∈ 𝐸 ↔ (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸) = 𝑛))
46	38, 42, 45	syl2an 603	. . . . . . . . . 10 ⊢ (((𝑛 ∈ (𝐺 NeighbVtx 𝑥) ∧ 𝑛 ∈ (𝐺 NeighbVtx 𝑌)) ∧ (𝜑 ∧ 𝑥 ∈ 𝐷)) → ({𝑥, 𝑛} ∈ 𝐸 ↔ (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸) = 𝑛))
47	35, 46	mpbid 234	. . . . . . . . 9 ⊢ (((𝑛 ∈ (𝐺 NeighbVtx 𝑥) ∧ 𝑛 ∈ (𝐺 NeighbVtx 𝑌)) ∧ (𝜑 ∧ 𝑥 ∈ 𝐷)) → (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸) = 𝑛)
48	24, 47	sylan 587	. . . . . . . 8 ⊢ ((((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)) = {𝑛} ∧ (𝜑 ∧ 𝑥 ∈ 𝐷)) → (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸) = 𝑛)
49	48	eqcomd 2747	. . . . . . 7 ⊢ ((((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)) = {𝑛} ∧ (𝜑 ∧ 𝑥 ∈ 𝐷)) → 𝑛 = (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸))
50	49	sneqd 4570	. . . . . 6 ⊢ ((((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)) = {𝑛} ∧ (𝜑 ∧ 𝑥 ∈ 𝐷)) → {𝑛} = {(℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)})
51		eqeq1 2745	. . . . . . 7 ⊢ (((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)) = {𝑛} → (((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)) = {(℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)} ↔ {𝑛} = {(℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)}))
52	51	adantr 482	. . . . . 6 ⊢ ((((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)) = {𝑛} ∧ (𝜑 ∧ 𝑥 ∈ 𝐷)) → (((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)) = {(℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)} ↔ {𝑛} = {(℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)}))
53	50, 52	mpbird 259	. . . . 5 ⊢ ((((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)) = {𝑛} ∧ (𝜑 ∧ 𝑥 ∈ 𝐷)) → ((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)) = {(℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)})
54	53	ex 414	. . . 4 ⊢ (((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)) = {𝑛} → ((𝜑 ∧ 𝑥 ∈ 𝐷) → ((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)) = {(℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)}))
55	54	rexlimivw 3138	. . 3 ⊢ (∃𝑛 ∈ 𝑉 ((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)) = {𝑛} → ((𝜑 ∧ 𝑥 ∈ 𝐷) → ((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)) = {(℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)}))
56	21, 55	mpcom 38	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)) = {(℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)})
57	2, 56	eqtr2id 2789	1 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → {(℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)} = ((𝐺 NeighbVtx 𝑥) ∩ 𝑁))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 397   ∧ w3a 1093   = wceq 1548   ∈ wcel 2121   ≠ wne 2936   ∉ wnel 3040  ∃wrex 3065  ∃!wreu 3344  Vcvv 3433   ∩ cin 3884  {csn 4558  {cpr 4560   ↦ cmpt 5156  ‘cfv 6489  ℩crio 7316  (class class class)co 7360  Vtxcvtx 29087  Edgcedg 29138  USGraphcusgr 29240   NeighbVtx cnbgr 29423   FriendGraph cfrgr 30350

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-ext 2713  ax-sep 5221  ax-nul 5231  ax-pow 5297  ax-pr 5365  ax-un 7682  ax-cnex 11089  ax-resscn 11090  ax-1cn 11091  ax-icn 11092  ax-addcl 11093  ax-addrcl 11094  ax-mulcl 11095  ax-mulrcl 11096  ax-mulcom 11097  ax-addass 11098  ax-mulass 11099  ax-distr 11100  ax-i2m1 11101  ax-1ne0 11102  ax-1rid 11103  ax-rnegex 11104  ax-rrecex 11105  ax-cnre 11106  ax-pre-lttri 11107  ax-pre-lttrn 11108  ax-pre-ltadd 11109  ax-pre-mulgt0 11110

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3or 1094  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-nf 1792  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-ne 2937  df-nel 3041  df-ral 3056  df-rex 3066  df-rmo 3346  df-reu 3347  df-rab 3394  df-v 3435  df-sbc 3726  df-csb 3834  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-pss 3905  df-nul 4265  df-if 4458  df-pw 4534  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4842  df-int 4881  df-iun 4926  df-br 5076  df-opab 5138  df-mpt 5157  df-tr 5183  df-id 5516  df-eprel 5521  df-po 5529  df-so 5530  df-fr 5574  df-we 5576  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-pred 6256  df-ord 6317  df-on 6318  df-lim 6319  df-suc 6320  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-riota 7317  df-ov 7363  df-oprab 7364  df-mpo 7365  df-om 7811  df-1st 7935  df-2nd 7936  df-frecs 8225  df-wrecs 8256  df-recs 8305  df-rdg 8343  df-1o 8399  df-2o 8400  df-oadd 8403  df-er 8637  df-en 8888  df-dom 8889  df-sdom 8890  df-fin 8891  df-dju 9820  df-card 9858  df-pnf 11176  df-mnf 11177  df-xr 11178  df-ltxr 11179  df-le 11180  df-sub 11374  df-neg 11375  df-nn 12170  df-2 12239  df-n0 12433  df-xnn0 12506  df-z 12520  df-uz 12784  df-fz 13457  df-hash 14288  df-edg 29139  df-upgr 29173  df-umgr 29174  df-usgr 29242  df-nbgr 29424  df-frgr 30351

This theorem is referenced by:  frgrncvvdeqlem5  30395