Metamath Proof Explorer

Theorem frgr1v

Description: Any graph with (at most) one vertex is a friendship graph. (Contributed by Alexander van der Vekens, 4-Oct-2017) (Revised by AV, 29-Mar-2021)

Ref Expression
Assertion frgr1v ⊢G∈USGraph∧Vtx⁡G=N→G∈FriendGraph

Proof

Step Hyp Ref Expression
1 simpl ⊢G∈USGraph∧Vtx⁡G=N→G∈USGraph
2 ral0 ⊢∀l∈∅∃!x∈NxNxl⊆Edg⁡G
3 sneq ⊢k=N→k=N
4 3 difeq2d ⊢k=N→N∖k=N∖N
5 difid ⊢N∖N=∅
6 4 5 eqtrdi ⊢k=N→N∖k=∅
7 preq2 ⊢k=N→xk=xN
8 7 preq1d ⊢k=N→xkxl=xNxl
9 8 sseq1d ⊢k=N→xkxl⊆Edg⁡G↔xNxl⊆Edg⁡G
10 9 reubidv ⊢k=N→∃!x∈Nxkxl⊆Edg⁡G↔∃!x∈NxNxl⊆Edg⁡G
11 6 10 raleqbidv ⊢k=N→∀l∈N∖k∃!x∈Nxkxl⊆Edg⁡G↔∀l∈∅∃!x∈NxNxl⊆Edg⁡G
12 11 ralsng ⊢N∈V→∀k∈N∀l∈N∖k∃!x∈Nxkxl⊆Edg⁡G↔∀l∈∅∃!x∈NxNxl⊆Edg⁡G
13 2 12 mpbiri ⊢N∈V→∀k∈N∀l∈N∖k∃!x∈Nxkxl⊆Edg⁡G
14 snprc ⊢¬N∈V↔N=∅
15 rzal ⊢N=∅→∀k∈N∀l∈N∖k∃!x∈Nxkxl⊆Edg⁡G
16 14 15 sylbi ⊢¬N∈V→∀k∈N∀l∈N∖k∃!x∈Nxkxl⊆Edg⁡G
17 13 16 pm2.61i ⊢∀k∈N∀l∈N∖k∃!x∈Nxkxl⊆Edg⁡G
18 id ⊢Vtx⁡G=N→Vtx⁡G=N
19 difeq1 ⊢Vtx⁡G=N→Vtx⁡G∖k=N∖k
20 reueq1 ⊢Vtx⁡G=N→∃!x∈Vtx⁡Gxkxl⊆Edg⁡G↔∃!x∈Nxkxl⊆Edg⁡G
21 19 20 raleqbidv ⊢Vtx⁡G=N→∀l∈Vtx⁡G∖k∃!x∈Vtx⁡Gxkxl⊆Edg⁡G↔∀l∈N∖k∃!x∈Nxkxl⊆Edg⁡G
22 18 21 raleqbidv ⊢Vtx⁡G=N→∀k∈Vtx⁡G∀l∈Vtx⁡G∖k∃!x∈Vtx⁡Gxkxl⊆Edg⁡G↔∀k∈N∀l∈N∖k∃!x∈Nxkxl⊆Edg⁡G
23 22 adantl ⊢G∈USGraph∧Vtx⁡G=N→∀k∈Vtx⁡G∀l∈Vtx⁡G∖k∃!x∈Vtx⁡Gxkxl⊆Edg⁡G↔∀k∈N∀l∈N∖k∃!x∈Nxkxl⊆Edg⁡G
24 17 23 mpbiri ⊢G∈USGraph∧Vtx⁡G=N→∀k∈Vtx⁡G∀l∈Vtx⁡G∖k∃!x∈Vtx⁡Gxkxl⊆Edg⁡G
25 eqid ⊢Vtx⁡G=Vtx⁡G
26 eqid ⊢Edg⁡G=Edg⁡G
27 25 26 isfrgr ⊢G∈FriendGraph↔G∈USGraph∧∀k∈Vtx⁡G∀l∈Vtx⁡G∖k∃!x∈Vtx⁡Gxkxl⊆Edg⁡G
28 1 24 27 sylanbrc ⊢G∈USGraph∧Vtx⁡G=N→G∈FriendGraph