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 ∈ N x N x l ⊆ 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 → x k = x N
8 7 preq1d ⊢ k = N → x k x l = x N x l
9 8 sseq1d ⊢ k = N → x k x l ⊆ Edg ⁡ G ↔ x N x l ⊆ Edg ⁡ G
10 9 reubidv ⊢ k = N → ∃! x ∈ N x k x l ⊆ Edg ⁡ G ↔ ∃! x ∈ N x N x l ⊆ Edg ⁡ G
11 6 10 raleqbidv ⊢ k = N → ∀ l ∈ N ∖ k ∃! x ∈ N x k x l ⊆ Edg ⁡ G ↔ ∀ l ∈ ∅ ∃! x ∈ N x N x l ⊆ Edg ⁡ G
12 11 ralsng ⊢ N ∈ V → ∀ k ∈ N ∀ l ∈ N ∖ k ∃! x ∈ N x k x l ⊆ Edg ⁡ G ↔ ∀ l ∈ ∅ ∃! x ∈ N x N x l ⊆ Edg ⁡ G
13 2 12 mpbiri ⊢ N ∈ V → ∀ k ∈ N ∀ l ∈ N ∖ k ∃! x ∈ N x k x l ⊆ Edg ⁡ G
14 snprc ⊢ ¬ N ∈ V ↔ N = ∅
15 rzal ⊢ N = ∅ → ∀ k ∈ N ∀ l ∈ N ∖ k ∃! x ∈ N x k x l ⊆ Edg ⁡ G
16 14 15 sylbi ⊢ ¬ N ∈ V → ∀ k ∈ N ∀ l ∈ N ∖ k ∃! x ∈ N x k x l ⊆ Edg ⁡ G
17 13 16 pm2.61i ⊢ ∀ k ∈ N ∀ l ∈ N ∖ k ∃! x ∈ N x k x l ⊆ 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 ⁡ G x k x l ⊆ Edg ⁡ G ↔ ∃! x ∈ N x k x l ⊆ Edg ⁡ G
21 19 20 raleqbidv ⊢ Vtx ⁡ G = N → ∀ l ∈ Vtx ⁡ G ∖ k ∃! x ∈ Vtx ⁡ G x k x l ⊆ Edg ⁡ G ↔ ∀ l ∈ N ∖ k ∃! x ∈ N x k x l ⊆ Edg ⁡ G
22 18 21 raleqbidv ⊢ Vtx ⁡ G = N → ∀ k ∈ Vtx ⁡ G ∀ l ∈ Vtx ⁡ G ∖ k ∃! x ∈ Vtx ⁡ G x k x l ⊆ Edg ⁡ G ↔ ∀ k ∈ N ∀ l ∈ N ∖ k ∃! x ∈ N x k x l ⊆ Edg ⁡ G
23 22 adantl ⊢ G ∈ USGraph ∧ Vtx ⁡ G = N → ∀ k ∈ Vtx ⁡ G ∀ l ∈ Vtx ⁡ G ∖ k ∃! x ∈ Vtx ⁡ G x k x l ⊆ Edg ⁡ G ↔ ∀ k ∈ N ∀ l ∈ N ∖ k ∃! x ∈ N x k x l ⊆ Edg ⁡ G
24 17 23 mpbiri ⊢ G ∈ USGraph ∧ Vtx ⁡ G = N → ∀ k ∈ Vtx ⁡ G ∀ l ∈ Vtx ⁡ G ∖ k ∃! x ∈ Vtx ⁡ G x k x l ⊆ 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 ⁡ G x k x l ⊆ Edg ⁡ G
28 1 24 27 sylanbrc ⊢ G ∈ USGraph ∧ Vtx ⁡ G = N → G ∈ FriendGraph