Theorem frgraunss 26522

Description: Any two (different) vertices in a friendship graph have a unique common neighbor. (Contributed by Alexander van der Vekens, 19-Dec-2017.)

Assertion

Ref	Expression
frgraunss	⊢ (𝑉 FriendGrph 𝐸 → ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶) → ∃!𝑏 ∈ 𝑉 {{𝐴, 𝑏}, {𝑏, 𝐶}} ⊆ ran 𝐸))

Distinct variable groups:   𝐴,𝑏   𝐶,𝑏   𝐸,𝑏   𝑉,𝑏

Proof of Theorem frgraunss

Dummy variables 𝑎 𝑐 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		frisusgrapr 26518	. 2 ⊢ (𝑉 FriendGrph 𝐸 → (𝑉 USGrph 𝐸 ∧ ∀𝑎 ∈ 𝑉 ∀𝑐 ∈ (𝑉 ∖ {𝑎})∃!𝑏 ∈ 𝑉 {{𝑏, 𝑎}, {𝑏, 𝑐}} ⊆ ran 𝐸))
2		sneq 4135	. . . . . . . . . . 11 ⊢ (𝑎 = 𝐴 → {𝑎} = {𝐴})
3	2	difeq2d 3690	. . . . . . . . . 10 ⊢ (𝑎 = 𝐴 → (𝑉 ∖ {𝑎}) = (𝑉 ∖ {𝐴}))
4		preq2 4213	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝐴 → {𝑏, 𝑎} = {𝑏, 𝐴})
5	4	preq1d 4218	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝐴 → {{𝑏, 𝑎}, {𝑏, 𝑐}} = {{𝑏, 𝐴}, {𝑏, 𝑐}})
6	5	sseq1d 3595	. . . . . . . . . . 11 ⊢ (𝑎 = 𝐴 → ({{𝑏, 𝑎}, {𝑏, 𝑐}} ⊆ ran 𝐸 ↔ {{𝑏, 𝐴}, {𝑏, 𝑐}} ⊆ ran 𝐸))
7	6	reubidv 3103	. . . . . . . . . 10 ⊢ (𝑎 = 𝐴 → (∃!𝑏 ∈ 𝑉 {{𝑏, 𝑎}, {𝑏, 𝑐}} ⊆ ran 𝐸 ↔ ∃!𝑏 ∈ 𝑉 {{𝑏, 𝐴}, {𝑏, 𝑐}} ⊆ ran 𝐸))
8	3, 7	raleqbidv 3129	. . . . . . . . 9 ⊢ (𝑎 = 𝐴 → (∀𝑐 ∈ (𝑉 ∖ {𝑎})∃!𝑏 ∈ 𝑉 {{𝑏, 𝑎}, {𝑏, 𝑐}} ⊆ ran 𝐸 ↔ ∀𝑐 ∈ (𝑉 ∖ {𝐴})∃!𝑏 ∈ 𝑉 {{𝑏, 𝐴}, {𝑏, 𝑐}} ⊆ ran 𝐸))
9	8	rspcva 3280	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑎 ∈ 𝑉 ∀𝑐 ∈ (𝑉 ∖ {𝑎})∃!𝑏 ∈ 𝑉 {{𝑏, 𝑎}, {𝑏, 𝑐}} ⊆ ran 𝐸) → ∀𝑐 ∈ (𝑉 ∖ {𝐴})∃!𝑏 ∈ 𝑉 {{𝑏, 𝐴}, {𝑏, 𝑐}} ⊆ ran 𝐸)
10		elsni 4142	. . . . . . . . . . . . . . 15 ⊢ (𝐶 ∈ {𝐴} → 𝐶 = 𝐴)
11	10	eqcomd 2616	. . . . . . . . . . . . . 14 ⊢ (𝐶 ∈ {𝐴} → 𝐴 = 𝐶)
12	11	necon3ai 2807	. . . . . . . . . . . . 13 ⊢ (𝐴 ≠ 𝐶 → ¬ 𝐶 ∈ {𝐴})
13	12	anim2i 591	. . . . . . . . . . . 12 ⊢ ((𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶) → (𝐶 ∈ 𝑉 ∧ ¬ 𝐶 ∈ {𝐴}))
14		eldif 3550	. . . . . . . . . . . 12 ⊢ (𝐶 ∈ (𝑉 ∖ {𝐴}) ↔ (𝐶 ∈ 𝑉 ∧ ¬ 𝐶 ∈ {𝐴}))
15	13, 14	sylibr 223	. . . . . . . . . . 11 ⊢ ((𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶) → 𝐶 ∈ (𝑉 ∖ {𝐴}))
16		preq2 4213	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = 𝐶 → {𝑏, 𝑐} = {𝑏, 𝐶})
17	16	preq2d 4219	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = 𝐶 → {{𝑏, 𝐴}, {𝑏, 𝑐}} = {{𝑏, 𝐴}, {𝑏, 𝐶}})
18	17	sseq1d 3595	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = 𝐶 → ({{𝑏, 𝐴}, {𝑏, 𝑐}} ⊆ ran 𝐸 ↔ {{𝑏, 𝐴}, {𝑏, 𝐶}} ⊆ ran 𝐸))
19	18	reubidv 3103	. . . . . . . . . . . . . 14 ⊢ (𝑐 = 𝐶 → (∃!𝑏 ∈ 𝑉 {{𝑏, 𝐴}, {𝑏, 𝑐}} ⊆ ran 𝐸 ↔ ∃!𝑏 ∈ 𝑉 {{𝑏, 𝐴}, {𝑏, 𝐶}} ⊆ ran 𝐸))
20	19	rspcva 3280	. . . . . . . . . . . . 13 ⊢ ((𝐶 ∈ (𝑉 ∖ {𝐴}) ∧ ∀𝑐 ∈ (𝑉 ∖ {𝐴})∃!𝑏 ∈ 𝑉 {{𝑏, 𝐴}, {𝑏, 𝑐}} ⊆ ran 𝐸) → ∃!𝑏 ∈ 𝑉 {{𝑏, 𝐴}, {𝑏, 𝐶}} ⊆ ran 𝐸)
21		prcom 4211	. . . . . . . . . . . . . . . 16 ⊢ {𝑏, 𝐴} = {𝐴, 𝑏}
22	21	preq1i 4215	. . . . . . . . . . . . . . 15 ⊢ {{𝑏, 𝐴}, {𝑏, 𝐶}} = {{𝐴, 𝑏}, {𝑏, 𝐶}}
23	22	sseq1i 3592	. . . . . . . . . . . . . 14 ⊢ ({{𝑏, 𝐴}, {𝑏, 𝐶}} ⊆ ran 𝐸 ↔ {{𝐴, 𝑏}, {𝑏, 𝐶}} ⊆ ran 𝐸)
24	23	reubii 3105	. . . . . . . . . . . . 13 ⊢ (∃!𝑏 ∈ 𝑉 {{𝑏, 𝐴}, {𝑏, 𝐶}} ⊆ ran 𝐸 ↔ ∃!𝑏 ∈ 𝑉 {{𝐴, 𝑏}, {𝑏, 𝐶}} ⊆ ran 𝐸)
25	20, 24	sylib 207	. . . . . . . . . . . 12 ⊢ ((𝐶 ∈ (𝑉 ∖ {𝐴}) ∧ ∀𝑐 ∈ (𝑉 ∖ {𝐴})∃!𝑏 ∈ 𝑉 {{𝑏, 𝐴}, {𝑏, 𝑐}} ⊆ ran 𝐸) → ∃!𝑏 ∈ 𝑉 {{𝐴, 𝑏}, {𝑏, 𝐶}} ⊆ ran 𝐸)
26	25	ex 449	. . . . . . . . . . 11 ⊢ (𝐶 ∈ (𝑉 ∖ {𝐴}) → (∀𝑐 ∈ (𝑉 ∖ {𝐴})∃!𝑏 ∈ 𝑉 {{𝑏, 𝐴}, {𝑏, 𝑐}} ⊆ ran 𝐸 → ∃!𝑏 ∈ 𝑉 {{𝐴, 𝑏}, {𝑏, 𝐶}} ⊆ ran 𝐸))
27	15, 26	syl 17	. . . . . . . . . 10 ⊢ ((𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶) → (∀𝑐 ∈ (𝑉 ∖ {𝐴})∃!𝑏 ∈ 𝑉 {{𝑏, 𝐴}, {𝑏, 𝑐}} ⊆ ran 𝐸 → ∃!𝑏 ∈ 𝑉 {{𝐴, 𝑏}, {𝑏, 𝐶}} ⊆ ran 𝐸))
28	27	ex 449	. . . . . . . . 9 ⊢ (𝐶 ∈ 𝑉 → (𝐴 ≠ 𝐶 → (∀𝑐 ∈ (𝑉 ∖ {𝐴})∃!𝑏 ∈ 𝑉 {{𝑏, 𝐴}, {𝑏, 𝑐}} ⊆ ran 𝐸 → ∃!𝑏 ∈ 𝑉 {{𝐴, 𝑏}, {𝑏, 𝐶}} ⊆ ran 𝐸)))
29	28	com13 86	. . . . . . . 8 ⊢ (∀𝑐 ∈ (𝑉 ∖ {𝐴})∃!𝑏 ∈ 𝑉 {{𝑏, 𝐴}, {𝑏, 𝑐}} ⊆ ran 𝐸 → (𝐴 ≠ 𝐶 → (𝐶 ∈ 𝑉 → ∃!𝑏 ∈ 𝑉 {{𝐴, 𝑏}, {𝑏, 𝐶}} ⊆ ran 𝐸)))
30	9, 29	syl 17	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑎 ∈ 𝑉 ∀𝑐 ∈ (𝑉 ∖ {𝑎})∃!𝑏 ∈ 𝑉 {{𝑏, 𝑎}, {𝑏, 𝑐}} ⊆ ran 𝐸) → (𝐴 ≠ 𝐶 → (𝐶 ∈ 𝑉 → ∃!𝑏 ∈ 𝑉 {{𝐴, 𝑏}, {𝑏, 𝐶}} ⊆ ran 𝐸)))
31	30	ex 449	. . . . . 6 ⊢ (𝐴 ∈ 𝑉 → (∀𝑎 ∈ 𝑉 ∀𝑐 ∈ (𝑉 ∖ {𝑎})∃!𝑏 ∈ 𝑉 {{𝑏, 𝑎}, {𝑏, 𝑐}} ⊆ ran 𝐸 → (𝐴 ≠ 𝐶 → (𝐶 ∈ 𝑉 → ∃!𝑏 ∈ 𝑉 {{𝐴, 𝑏}, {𝑏, 𝐶}} ⊆ ran 𝐸))))
32	31	com24 93	. . . . 5 ⊢ (𝐴 ∈ 𝑉 → (𝐶 ∈ 𝑉 → (𝐴 ≠ 𝐶 → (∀𝑎 ∈ 𝑉 ∀𝑐 ∈ (𝑉 ∖ {𝑎})∃!𝑏 ∈ 𝑉 {{𝑏, 𝑎}, {𝑏, 𝑐}} ⊆ ran 𝐸 → ∃!𝑏 ∈ 𝑉 {{𝐴, 𝑏}, {𝑏, 𝐶}} ⊆ ran 𝐸))))
33	32	3imp 1249	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶) → (∀𝑎 ∈ 𝑉 ∀𝑐 ∈ (𝑉 ∖ {𝑎})∃!𝑏 ∈ 𝑉 {{𝑏, 𝑎}, {𝑏, 𝑐}} ⊆ ran 𝐸 → ∃!𝑏 ∈ 𝑉 {{𝐴, 𝑏}, {𝑏, 𝐶}} ⊆ ran 𝐸))
34	33	com12 32	. . 3 ⊢ (∀𝑎 ∈ 𝑉 ∀𝑐 ∈ (𝑉 ∖ {𝑎})∃!𝑏 ∈ 𝑉 {{𝑏, 𝑎}, {𝑏, 𝑐}} ⊆ ran 𝐸 → ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶) → ∃!𝑏 ∈ 𝑉 {{𝐴, 𝑏}, {𝑏, 𝐶}} ⊆ ran 𝐸))
35	34	adantl 481	. 2 ⊢ ((𝑉 USGrph 𝐸 ∧ ∀𝑎 ∈ 𝑉 ∀𝑐 ∈ (𝑉 ∖ {𝑎})∃!𝑏 ∈ 𝑉 {{𝑏, 𝑎}, {𝑏, 𝑐}} ⊆ ran 𝐸) → ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶) → ∃!𝑏 ∈ 𝑉 {{𝐴, 𝑏}, {𝑏, 𝐶}} ⊆ ran 𝐸))
36	1, 35	syl 17	1 ⊢ (𝑉 FriendGrph 𝐸 → ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶) → ∃!𝑏 ∈ 𝑉 {{𝐴, 𝑏}, {𝑏, 𝐶}} ⊆ ran 𝐸))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  ∃!wreu 2898   ∖ cdif 3537   ⊆ wss 3540  {csn 4125  {cpr 4127   class class class wbr 4583  ran crn 5039   USGrph cusg 25859   FriendGrph cfrgra 26515

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584  df-opab 4644  df-xp 5044  df-rel 5045  df-cnv 5046  df-dm 5048  df-rn 5049  df-frgra 26516

This theorem is referenced by:  frgraun  26523  4cyclusnfrgra  26546  frgrancvvdeqlem3  26559