Theorem nbupgruvtxres 27819

Description: The neighborhood of a universal vertex in a restricted pseudograph. (Contributed by Alexander van der Vekens, 2-Jan-2018.) (Revised by AV, 8-Nov-2020.) (Proof shortened by AV, 13-Feb-2022.)

Hypotheses

Ref	Expression
nbupgruvtxres.v	⊢ 𝑉 = (Vtx‘𝐺)
nbupgruvtxres.e	⊢ 𝐸 = (Edg‘𝐺)
nbupgruvtxres.f	⊢ 𝐹 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒}
nbupgruvtxres.s	⊢ 𝑆 = ⟨(𝑉 ∖ {𝑁}), ( I ↾ 𝐹)⟩

Assertion

Ref	Expression
nbupgruvtxres	⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁})) → ((𝐺 NeighbVtx 𝐾) = (𝑉 ∖ {𝐾}) → (𝑆 NeighbVtx 𝐾) = (𝑉 ∖ {𝑁, 𝐾})))

Distinct variable groups:   𝑒,𝐸   𝑒,𝐺   𝑒,𝐾   𝑒,𝑁   𝑒,𝑉

Allowed substitution hints:   𝑆(𝑒)   𝐹(𝑒)

Proof of Theorem nbupgruvtxres

Dummy variable 𝑛 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2736	. . . . . 6 ⊢ (Vtx‘𝑆) = (Vtx‘𝑆)
2	1	nbgrssovtx 27773	. . . . 5 ⊢ (𝑆 NeighbVtx 𝐾) ⊆ ((Vtx‘𝑆) ∖ {𝐾})
3		difpr 4742	. . . . . 6 ⊢ (𝑉 ∖ {𝑁, 𝐾}) = ((𝑉 ∖ {𝑁}) ∖ {𝐾})
4		nbupgruvtxres.v	. . . . . . . . . 10 ⊢ 𝑉 = (Vtx‘𝐺)
5		nbupgruvtxres.e	. . . . . . . . . 10 ⊢ 𝐸 = (Edg‘𝐺)
6		nbupgruvtxres.f	. . . . . . . . . 10 ⊢ 𝐹 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒}
7		nbupgruvtxres.s	. . . . . . . . . 10 ⊢ 𝑆 = ⟨(𝑉 ∖ {𝑁}), ( I ↾ 𝐹)⟩
8	4, 5, 6, 7	upgrres1lem2 27723	. . . . . . . . 9 ⊢ (Vtx‘𝑆) = (𝑉 ∖ {𝑁})
9	8	eqcomi 2745	. . . . . . . 8 ⊢ (𝑉 ∖ {𝑁}) = (Vtx‘𝑆)
10	9	a1i 11	. . . . . . 7 ⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁})) → (𝑉 ∖ {𝑁}) = (Vtx‘𝑆))
11	10	difeq1d 4062	. . . . . 6 ⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁})) → ((𝑉 ∖ {𝑁}) ∖ {𝐾}) = ((Vtx‘𝑆) ∖ {𝐾}))
12	3, 11	eqtrid 2788	. . . . 5 ⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁})) → (𝑉 ∖ {𝑁, 𝐾}) = ((Vtx‘𝑆) ∖ {𝐾}))
13	2, 12	sseqtrrid 3979	. . . 4 ⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁})) → (𝑆 NeighbVtx 𝐾) ⊆ (𝑉 ∖ {𝑁, 𝐾}))
14	13	adantr 482	. . 3 ⊢ ((((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁})) ∧ (𝐺 NeighbVtx 𝐾) = (𝑉 ∖ {𝐾})) → (𝑆 NeighbVtx 𝐾) ⊆ (𝑉 ∖ {𝑁, 𝐾}))
15		simpl 484	. . . . . 6 ⊢ ((((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁})) ∧ (𝐺 NeighbVtx 𝐾) = (𝑉 ∖ {𝐾})) → ((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁})))
16	15	anim1i 616	. . . . 5 ⊢ (((((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁})) ∧ (𝐺 NeighbVtx 𝐾) = (𝑉 ∖ {𝐾})) ∧ 𝑛 ∈ (𝑉 ∖ {𝑁, 𝐾})) → (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁})) ∧ 𝑛 ∈ (𝑉 ∖ {𝑁, 𝐾})))
17		df-3an 1089	. . . . 5 ⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁}) ∧ 𝑛 ∈ (𝑉 ∖ {𝑁, 𝐾})) ↔ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁})) ∧ 𝑛 ∈ (𝑉 ∖ {𝑁, 𝐾})))
18	16, 17	sylibr 233	. . . 4 ⊢ (((((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁})) ∧ (𝐺 NeighbVtx 𝐾) = (𝑉 ∖ {𝐾})) ∧ 𝑛 ∈ (𝑉 ∖ {𝑁, 𝐾})) → ((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁}) ∧ 𝑛 ∈ (𝑉 ∖ {𝑁, 𝐾})))
19		dif32 4232	. . . . . . . . . . 11 ⊢ ((𝑉 ∖ {𝑁}) ∖ {𝐾}) = ((𝑉 ∖ {𝐾}) ∖ {𝑁})
20	3, 19	eqtri 2764	. . . . . . . . . 10 ⊢ (𝑉 ∖ {𝑁, 𝐾}) = ((𝑉 ∖ {𝐾}) ∖ {𝑁})
21	20	eleq2i 2828	. . . . . . . . 9 ⊢ (𝑛 ∈ (𝑉 ∖ {𝑁, 𝐾}) ↔ 𝑛 ∈ ((𝑉 ∖ {𝐾}) ∖ {𝑁}))
22		eldifsn 4726	. . . . . . . . 9 ⊢ (𝑛 ∈ ((𝑉 ∖ {𝐾}) ∖ {𝑁}) ↔ (𝑛 ∈ (𝑉 ∖ {𝐾}) ∧ 𝑛 ≠ 𝑁))
23	21, 22	bitri 275	. . . . . . . 8 ⊢ (𝑛 ∈ (𝑉 ∖ {𝑁, 𝐾}) ↔ (𝑛 ∈ (𝑉 ∖ {𝐾}) ∧ 𝑛 ≠ 𝑁))
24	23	simplbi 499	. . . . . . 7 ⊢ (𝑛 ∈ (𝑉 ∖ {𝑁, 𝐾}) → 𝑛 ∈ (𝑉 ∖ {𝐾}))
25		eleq2 2825	. . . . . . 7 ⊢ ((𝐺 NeighbVtx 𝐾) = (𝑉 ∖ {𝐾}) → (𝑛 ∈ (𝐺 NeighbVtx 𝐾) ↔ 𝑛 ∈ (𝑉 ∖ {𝐾})))
26	24, 25	syl5ibr 246	. . . . . 6 ⊢ ((𝐺 NeighbVtx 𝐾) = (𝑉 ∖ {𝐾}) → (𝑛 ∈ (𝑉 ∖ {𝑁, 𝐾}) → 𝑛 ∈ (𝐺 NeighbVtx 𝐾)))
27	26	adantl 483	. . . . 5 ⊢ ((((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁})) ∧ (𝐺 NeighbVtx 𝐾) = (𝑉 ∖ {𝐾})) → (𝑛 ∈ (𝑉 ∖ {𝑁, 𝐾}) → 𝑛 ∈ (𝐺 NeighbVtx 𝐾)))
28	27	imp 408	. . . 4 ⊢ (((((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁})) ∧ (𝐺 NeighbVtx 𝐾) = (𝑉 ∖ {𝐾})) ∧ 𝑛 ∈ (𝑉 ∖ {𝑁, 𝐾})) → 𝑛 ∈ (𝐺 NeighbVtx 𝐾))
29	4, 5, 6, 7	nbupgrres 27776	. . . 4 ⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁}) ∧ 𝑛 ∈ (𝑉 ∖ {𝑁, 𝐾})) → (𝑛 ∈ (𝐺 NeighbVtx 𝐾) → 𝑛 ∈ (𝑆 NeighbVtx 𝐾)))
30	18, 28, 29	sylc 65	. . 3 ⊢ (((((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁})) ∧ (𝐺 NeighbVtx 𝐾) = (𝑉 ∖ {𝐾})) ∧ 𝑛 ∈ (𝑉 ∖ {𝑁, 𝐾})) → 𝑛 ∈ (𝑆 NeighbVtx 𝐾))
31	14, 30	eqelssd 3947	. 2 ⊢ ((((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁})) ∧ (𝐺 NeighbVtx 𝐾) = (𝑉 ∖ {𝐾})) → (𝑆 NeighbVtx 𝐾) = (𝑉 ∖ {𝑁, 𝐾}))
32	31	ex 414	1 ⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁})) → ((𝐺 NeighbVtx 𝐾) = (𝑉 ∖ {𝐾}) → (𝑆 NeighbVtx 𝐾) = (𝑉 ∖ {𝑁, 𝐾})))

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1087   = wceq 1539   ∈ wcel 2104   ≠ wne 2941   ∉ wnel 3047  {crab 3284   ∖ cdif 3889   ⊆ wss 3892  {csn 4565  {cpr 4567  ⟨cop 4571   I cid 5499   ↾ cres 5602  ‘cfv 6458  (class class class)co 7307  Vtxcvtx 27411  Edgcedg 27462  UPGraphcupgr 27495   NeighbVtx cnbgr 27744

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2707  ax-sep 5232  ax-nul 5239  ax-pow 5297  ax-pr 5361  ax-un 7620  ax-cnex 10973  ax-resscn 10974  ax-1cn 10975  ax-icn 10976  ax-addcl 10977  ax-addrcl 10978  ax-mulcl 10979  ax-mulrcl 10980  ax-mulcom 10981  ax-addass 10982  ax-mulass 10983  ax-distr 10984  ax-i2m1 10985  ax-1ne0 10986  ax-1rid 10987  ax-rnegex 10988  ax-rrecex 10989  ax-cnre 10990  ax-pre-lttri 10991  ax-pre-lttrn 10992  ax-pre-ltadd 10993  ax-pre-mulgt0 10994

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3or 1088  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-reu 3286  df-rab 3287  df-v 3439  df-sbc 3722  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-pss 3911  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4566  df-pr 4568  df-op 4572  df-uni 4845  df-int 4887  df-iun 4933  df-br 5082  df-opab 5144  df-mpt 5165  df-tr 5199  df-id 5500  df-eprel 5506  df-po 5514  df-so 5515  df-fr 5555  df-we 5557  df-xp 5606  df-rel 5607  df-cnv 5608  df-co 5609  df-dm 5610  df-rn 5611  df-res 5612  df-ima 5613  df-pred 6217  df-ord 6284  df-on 6285  df-lim 6286  df-suc 6287  df-iota 6410  df-fun 6460  df-fn 6461  df-f 6462  df-f1 6463  df-fo 6464  df-f1o 6465  df-fv 6466  df-riota 7264  df-ov 7310  df-oprab 7311  df-mpo 7312  df-om 7745  df-1st 7863  df-2nd 7864  df-frecs 8128  df-wrecs 8159  df-recs 8233  df-rdg 8272  df-1o 8328  df-2o 8329  df-oadd 8332  df-er 8529  df-en 8765  df-dom 8766  df-sdom 8767  df-fin 8768  df-dju 9703  df-card 9741  df-pnf 11057  df-mnf 11058  df-xr 11059  df-ltxr 11060  df-le 11061  df-sub 11253  df-neg 11254  df-nn 12020  df-2 12082  df-n0 12280  df-xnn0 12352  df-z 12366  df-uz 12629  df-fz 13286  df-hash 14091  df-vtx 27413  df-iedg 27414  df-edg 27463  df-upgr 27497  df-nbgr 27745

This theorem is referenced by:  uvtxupgrres  27820