Metamath Proof Explorer

Theorem frcond1

Description: The friendship condition: any two (different) vertices in a friendship graph have a unique common neighbor. (Contributed by Alexander van der Vekens, 19-Dec-2017) (Revised by AV, 29-Mar-2021)

Ref Expression
Hypotheses frcond1.v ⊢ V = Vtx ⁡ G
frcond1.e ⊢ E = Edg ⁡ G
Assertion frcond1 ⊢ G ∈ FriendGraph → A ∈ V ∧ C ∈ V ∧ A ≠ C → ∃! b ∈ V A b b C ⊆ E

Proof

Step Hyp Ref Expression
1 frcond1.v ⊢ V = Vtx ⁡ G
2 frcond1.e ⊢ E = Edg ⁡ G
3 1 2 isfrgr ⊢ G ∈ FriendGraph ↔ G ∈ USGraph ∧ ∀ k ∈ V ∀ l ∈ V ∖ k ∃! b ∈ V b k b l ⊆ E
4 preq2 ⊢ k = A → b k = b A
5 4 preq1d ⊢ k = A → b k b l = b A b l
6 5 sseq1d ⊢ k = A → b k b l ⊆ E ↔ b A b l ⊆ E
7 6 reubidv ⊢ k = A → ∃! b ∈ V b k b l ⊆ E ↔ ∃! b ∈ V b A b l ⊆ E
8 preq2 ⊢ l = C → b l = b C
9 8 preq2d ⊢ l = C → b A b l = b A b C
10 9 sseq1d ⊢ l = C → b A b l ⊆ E ↔ b A b C ⊆ E
11 10 reubidv ⊢ l = C → ∃! b ∈ V b A b l ⊆ E ↔ ∃! b ∈ V b A b C ⊆ E
12 simp1 ⊢ A ∈ V ∧ C ∈ V ∧ A ≠ C → A ∈ V
13 sneq ⊢ k = A → k = A
14 13 difeq2d ⊢ k = A → V ∖ k = V ∖ A
15 14 adantl ⊢ A ∈ V ∧ C ∈ V ∧ A ≠ C ∧ k = A → V ∖ k = V ∖ A
16 necom ⊢ A ≠ C ↔ C ≠ A
17 16 biimpi ⊢ A ≠ C → C ≠ A
18 17 anim2i ⊢ C ∈ V ∧ A ≠ C → C ∈ V ∧ C ≠ A
19 18 3adant1 ⊢ A ∈ V ∧ C ∈ V ∧ A ≠ C → C ∈ V ∧ C ≠ A
20 eldifsn ⊢ C ∈ V ∖ A ↔ C ∈ V ∧ C ≠ A
21 19 20 sylibr ⊢ A ∈ V ∧ C ∈ V ∧ A ≠ C → C ∈ V ∖ A
22 7 11 12 15 21 rspc2vd ⊢ A ∈ V ∧ C ∈ V ∧ A ≠ C → ∀ k ∈ V ∀ l ∈ V ∖ k ∃! b ∈ V b k b l ⊆ E → ∃! b ∈ V b A b C ⊆ E
23 prcom ⊢ b A = A b
24 23 preq1i ⊢ b A b C = A b b C
25 24 sseq1i ⊢ b A b C ⊆ E ↔ A b b C ⊆ E
26 25 reubii ⊢ ∃! b ∈ V b A b C ⊆ E ↔ ∃! b ∈ V A b b C ⊆ E
27 26 biimpi ⊢ ∃! b ∈ V b A b C ⊆ E → ∃! b ∈ V A b b C ⊆ E
28 22 27 syl6com ⊢ ∀ k ∈ V ∀ l ∈ V ∖ k ∃! b ∈ V b k b l ⊆ E → A ∈ V ∧ C ∈ V ∧ A ≠ C → ∃! b ∈ V A b b C ⊆ E
29 3 28 simplbiim ⊢ G ∈ FriendGraph → A ∈ V ∧ C ∈ V ∧ A ≠ C → ∃! b ∈ V A b b C ⊆ E