Theorem isfrgr 27122

Description: The property of being a friendship graph. (Contributed by Alexander van der Vekens, 4-Oct-2017.) (Revised by AV, 29-Mar-2021.)

Hypotheses

Ref	Expression
isfrgr.v	⊢ 𝑉 = (Vtx‘𝐺)
isfrgr.e	⊢ 𝐸 = (Edg‘𝐺)

Assertion

Ref	Expression
isfrgr	⊢ (𝐺 ∈ 𝑈 → (𝐺 ∈ FriendGraph ↔ (𝐺 ∈ USGraph ∧ ∀𝑘 ∈ 𝑉 ∀𝑙 ∈ (𝑉 ∖ {𝑘})∃!𝑥 ∈ 𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸)))

Distinct variable groups:   𝑘,𝑙,𝑥,𝐺   𝑘,𝑉,𝑙,𝑥

Allowed substitution hints:   𝑈(𝑥,𝑘,𝑙)   𝐸(𝑥,𝑘,𝑙)

Proof of Theorem isfrgr

Dummy variables 𝑒 ℎ 𝑔 𝑣 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-frgr 27121	. . 3 ⊢ FriendGraph = {𝑔 ∣ (𝑔 ∈ USGraph ∧ [(Vtx‘𝑔) / 𝑣][(Edg‘𝑔) / 𝑒]∀𝑘 ∈ 𝑣 ∀𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥 ∈ 𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒)}
2	1	eleq2i 2693	. 2 ⊢ (𝐺 ∈ FriendGraph ↔ 𝐺 ∈ {𝑔 ∣ (𝑔 ∈ USGraph ∧ [(Vtx‘𝑔) / 𝑣][(Edg‘𝑔) / 𝑒]∀𝑘 ∈ 𝑣 ∀𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥 ∈ 𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒)})
3		eleq1 2689	. . . 4 ⊢ (ℎ = 𝐺 → (ℎ ∈ USGraph ↔ 𝐺 ∈ USGraph ))
4		fveq2 6191	. . . . . 6 ⊢ (ℎ = 𝐺 → (Vtx‘ℎ) = (Vtx‘𝐺))
5		isfrgr.v	. . . . . 6 ⊢ 𝑉 = (Vtx‘𝐺)
6	4, 5	syl6eqr 2674	. . . . 5 ⊢ (ℎ = 𝐺 → (Vtx‘ℎ) = 𝑉)
7	6	difeq1d 3727	. . . . . 6 ⊢ (ℎ = 𝐺 → ((Vtx‘ℎ) ∖ {𝑘}) = (𝑉 ∖ {𝑘}))
8		reueq1 3140	. . . . . . . 8 ⊢ ((Vtx‘ℎ) = 𝑉 → (∃!𝑥 ∈ (Vtx‘ℎ){{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘ℎ) ↔ ∃!𝑥 ∈ 𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘ℎ)))
9	6, 8	syl 17	. . . . . . 7 ⊢ (ℎ = 𝐺 → (∃!𝑥 ∈ (Vtx‘ℎ){{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘ℎ) ↔ ∃!𝑥 ∈ 𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘ℎ)))
10		fveq2 6191	. . . . . . . . . 10 ⊢ (ℎ = 𝐺 → (Edg‘ℎ) = (Edg‘𝐺))
11		isfrgr.e	. . . . . . . . . 10 ⊢ 𝐸 = (Edg‘𝐺)
12	10, 11	syl6eqr 2674	. . . . . . . . 9 ⊢ (ℎ = 𝐺 → (Edg‘ℎ) = 𝐸)
13	12	sseq2d 3633	. . . . . . . 8 ⊢ (ℎ = 𝐺 → ({{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘ℎ) ↔ {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸))
14	13	reubidv 3126	. . . . . . 7 ⊢ (ℎ = 𝐺 → (∃!𝑥 ∈ 𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘ℎ) ↔ ∃!𝑥 ∈ 𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸))
15	9, 14	bitrd 268	. . . . . 6 ⊢ (ℎ = 𝐺 → (∃!𝑥 ∈ (Vtx‘ℎ){{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘ℎ) ↔ ∃!𝑥 ∈ 𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸))
16	7, 15	raleqbidv 3152	. . . . 5 ⊢ (ℎ = 𝐺 → (∀𝑙 ∈ ((Vtx‘ℎ) ∖ {𝑘})∃!𝑥 ∈ (Vtx‘ℎ){{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘ℎ) ↔ ∀𝑙 ∈ (𝑉 ∖ {𝑘})∃!𝑥 ∈ 𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸))
17	6, 16	raleqbidv 3152	. . . 4 ⊢ (ℎ = 𝐺 → (∀𝑘 ∈ (Vtx‘ℎ)∀𝑙 ∈ ((Vtx‘ℎ) ∖ {𝑘})∃!𝑥 ∈ (Vtx‘ℎ){{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘ℎ) ↔ ∀𝑘 ∈ 𝑉 ∀𝑙 ∈ (𝑉 ∖ {𝑘})∃!𝑥 ∈ 𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸))
18	3, 17	anbi12d 747	. . 3 ⊢ (ℎ = 𝐺 → ((ℎ ∈ USGraph ∧ ∀𝑘 ∈ (Vtx‘ℎ)∀𝑙 ∈ ((Vtx‘ℎ) ∖ {𝑘})∃!𝑥 ∈ (Vtx‘ℎ){{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘ℎ)) ↔ (𝐺 ∈ USGraph ∧ ∀𝑘 ∈ 𝑉 ∀𝑙 ∈ (𝑉 ∖ {𝑘})∃!𝑥 ∈ 𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸)))
19		eleq1 2689	. . . . 5 ⊢ (𝑔 = ℎ → (𝑔 ∈ USGraph ↔ ℎ ∈ USGraph ))
20		fvexd 6203	. . . . . 6 ⊢ (𝑔 = ℎ → (Vtx‘𝑔) ∈ V)
21		fveq2 6191	. . . . . 6 ⊢ (𝑔 = ℎ → (Vtx‘𝑔) = (Vtx‘ℎ))
22		fvexd 6203	. . . . . . 7 ⊢ ((𝑔 = ℎ ∧ 𝑣 = (Vtx‘ℎ)) → (Edg‘𝑔) ∈ V)
23		fveq2 6191	. . . . . . . 8 ⊢ (𝑔 = ℎ → (Edg‘𝑔) = (Edg‘ℎ))
24	23	adantr 481	. . . . . . 7 ⊢ ((𝑔 = ℎ ∧ 𝑣 = (Vtx‘ℎ)) → (Edg‘𝑔) = (Edg‘ℎ))
25		simpr 477	. . . . . . . . 9 ⊢ ((𝑔 = ℎ ∧ 𝑣 = (Vtx‘ℎ)) → 𝑣 = (Vtx‘ℎ))
26	25	adantr 481	. . . . . . . 8 ⊢ (((𝑔 = ℎ ∧ 𝑣 = (Vtx‘ℎ)) ∧ 𝑒 = (Edg‘ℎ)) → 𝑣 = (Vtx‘ℎ))
27		difeq1 3721	. . . . . . . . . 10 ⊢ (𝑣 = (Vtx‘ℎ) → (𝑣 ∖ {𝑘}) = ((Vtx‘ℎ) ∖ {𝑘}))
28	27	ad2antlr 763	. . . . . . . . 9 ⊢ (((𝑔 = ℎ ∧ 𝑣 = (Vtx‘ℎ)) ∧ 𝑒 = (Edg‘ℎ)) → (𝑣 ∖ {𝑘}) = ((Vtx‘ℎ) ∖ {𝑘}))
29		reueq1 3140	. . . . . . . . . . 11 ⊢ (𝑣 = (Vtx‘ℎ) → (∃!𝑥 ∈ 𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒 ↔ ∃!𝑥 ∈ (Vtx‘ℎ){{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒))
30	29	ad2antlr 763	. . . . . . . . . 10 ⊢ (((𝑔 = ℎ ∧ 𝑣 = (Vtx‘ℎ)) ∧ 𝑒 = (Edg‘ℎ)) → (∃!𝑥 ∈ 𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒 ↔ ∃!𝑥 ∈ (Vtx‘ℎ){{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒))
31		simpr 477	. . . . . . . . . . . 12 ⊢ (((𝑔 = ℎ ∧ 𝑣 = (Vtx‘ℎ)) ∧ 𝑒 = (Edg‘ℎ)) → 𝑒 = (Edg‘ℎ))
32	31	sseq2d 3633	. . . . . . . . . . 11 ⊢ (((𝑔 = ℎ ∧ 𝑣 = (Vtx‘ℎ)) ∧ 𝑒 = (Edg‘ℎ)) → ({{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒 ↔ {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘ℎ)))
33	32	reubidv 3126	. . . . . . . . . 10 ⊢ (((𝑔 = ℎ ∧ 𝑣 = (Vtx‘ℎ)) ∧ 𝑒 = (Edg‘ℎ)) → (∃!𝑥 ∈ (Vtx‘ℎ){{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒 ↔ ∃!𝑥 ∈ (Vtx‘ℎ){{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘ℎ)))
34	30, 33	bitrd 268	. . . . . . . . 9 ⊢ (((𝑔 = ℎ ∧ 𝑣 = (Vtx‘ℎ)) ∧ 𝑒 = (Edg‘ℎ)) → (∃!𝑥 ∈ 𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒 ↔ ∃!𝑥 ∈ (Vtx‘ℎ){{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘ℎ)))
35	28, 34	raleqbidv 3152	. . . . . . . 8 ⊢ (((𝑔 = ℎ ∧ 𝑣 = (Vtx‘ℎ)) ∧ 𝑒 = (Edg‘ℎ)) → (∀𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥 ∈ 𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒 ↔ ∀𝑙 ∈ ((Vtx‘ℎ) ∖ {𝑘})∃!𝑥 ∈ (Vtx‘ℎ){{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘ℎ)))
36	26, 35	raleqbidv 3152	. . . . . . 7 ⊢ (((𝑔 = ℎ ∧ 𝑣 = (Vtx‘ℎ)) ∧ 𝑒 = (Edg‘ℎ)) → (∀𝑘 ∈ 𝑣 ∀𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥 ∈ 𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒 ↔ ∀𝑘 ∈ (Vtx‘ℎ)∀𝑙 ∈ ((Vtx‘ℎ) ∖ {𝑘})∃!𝑥 ∈ (Vtx‘ℎ){{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘ℎ)))
37	22, 24, 36	sbcied2 3473	. . . . . 6 ⊢ ((𝑔 = ℎ ∧ 𝑣 = (Vtx‘ℎ)) → ([(Edg‘𝑔) / 𝑒]∀𝑘 ∈ 𝑣 ∀𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥 ∈ 𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒 ↔ ∀𝑘 ∈ (Vtx‘ℎ)∀𝑙 ∈ ((Vtx‘ℎ) ∖ {𝑘})∃!𝑥 ∈ (Vtx‘ℎ){{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘ℎ)))
38	20, 21, 37	sbcied2 3473	. . . . 5 ⊢ (𝑔 = ℎ → ([(Vtx‘𝑔) / 𝑣][(Edg‘𝑔) / 𝑒]∀𝑘 ∈ 𝑣 ∀𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥 ∈ 𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒 ↔ ∀𝑘 ∈ (Vtx‘ℎ)∀𝑙 ∈ ((Vtx‘ℎ) ∖ {𝑘})∃!𝑥 ∈ (Vtx‘ℎ){{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘ℎ)))
39	19, 38	anbi12d 747	. . . 4 ⊢ (𝑔 = ℎ → ((𝑔 ∈ USGraph ∧ [(Vtx‘𝑔) / 𝑣][(Edg‘𝑔) / 𝑒]∀𝑘 ∈ 𝑣 ∀𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥 ∈ 𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒) ↔ (ℎ ∈ USGraph ∧ ∀𝑘 ∈ (Vtx‘ℎ)∀𝑙 ∈ ((Vtx‘ℎ) ∖ {𝑘})∃!𝑥 ∈ (Vtx‘ℎ){{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘ℎ))))
40	39	cbvabv 2747	. . 3 ⊢ {𝑔 ∣ (𝑔 ∈ USGraph ∧ [(Vtx‘𝑔) / 𝑣][(Edg‘𝑔) / 𝑒]∀𝑘 ∈ 𝑣 ∀𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥 ∈ 𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒)} = {ℎ ∣ (ℎ ∈ USGraph ∧ ∀𝑘 ∈ (Vtx‘ℎ)∀𝑙 ∈ ((Vtx‘ℎ) ∖ {𝑘})∃!𝑥 ∈ (Vtx‘ℎ){{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘ℎ))}
41	18, 40	elab2g 3353	. 2 ⊢ (𝐺 ∈ 𝑈 → (𝐺 ∈ {𝑔 ∣ (𝑔 ∈ USGraph ∧ [(Vtx‘𝑔) / 𝑣][(Edg‘𝑔) / 𝑒]∀𝑘 ∈ 𝑣 ∀𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥 ∈ 𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒)} ↔ (𝐺 ∈ USGraph ∧ ∀𝑘 ∈ 𝑉 ∀𝑙 ∈ (𝑉 ∖ {𝑘})∃!𝑥 ∈ 𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸)))
42	2, 41	syl5bb 272	1 ⊢ (𝐺 ∈ 𝑈 → (𝐺 ∈ FriendGraph ↔ (𝐺 ∈ USGraph ∧ ∀𝑘 ∈ 𝑉 ∀𝑙 ∈ (𝑉 ∖ {𝑘})∃!𝑥 ∈ 𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸)))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   = wceq 1483   ∈ wcel 1990  {cab 2608  ∀wral 2912  ∃!wreu 2914  Vcvv 3200  [wsbc 3435   ∖ cdif 3571   ⊆ wss 3574  {csn 4177  {cpr 4179  ‘cfv 5888  Vtxcvtx 25874  Edgcedg 25939   USGraph cusgr 26044   FriendGraph cfrgr 27120

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-nul 4789

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-frgr 27121

This theorem is referenced by:  frgrusgrfrcond  27123