Metamath Proof Explorer

Theorem frcond3

Description: The friendship condition, expressed by neighborhoods: in a friendship graph, the neighborhood of a vertex and the neighborhood of a second, different vertex have exactly one vertex in common. (Contributed by Alexander van der Vekens, 19-Dec-2017) (Revised by AV, 30-Dec-2021)

Ref Expression
Hypotheses frcond1.v ⊢ V = Vtx ⁡ G
frcond1.e ⊢ E = Edg ⁡ G
Assertion frcond3 ⊢ G ∈ FriendGraph → A ∈ V ∧ C ∈ V ∧ A ≠ C → ∃ x ∈ V G NeighbVtx A ∩ G NeighbVtx C = x

Proof

Step Hyp Ref Expression
1 frcond1.v ⊢ V = Vtx ⁡ G
2 frcond1.e ⊢ E = Edg ⁡ G
3 1 2 frcond1 ⊢ G ∈ FriendGraph → A ∈ V ∧ C ∈ V ∧ A ≠ C → ∃! b ∈ V A b b C ⊆ E
4 3 imp ⊢ G ∈ FriendGraph ∧ A ∈ V ∧ C ∈ V ∧ A ≠ C → ∃! b ∈ V A b b C ⊆ E
5 ssrab2 ⊢ b ∈ V | A b b C ⊆ E ⊆ V
6 sseq1 ⊢ b ∈ V | A b b C ⊆ E = x → b ∈ V | A b b C ⊆ E ⊆ V ↔ x ⊆ V
7 5 6 mpbii ⊢ b ∈ V | A b b C ⊆ E = x → x ⊆ V
8 vex ⊢ x ∈ V
9 8 snss ⊢ x ∈ V ↔ x ⊆ V
10 7 9 sylibr ⊢ b ∈ V | A b b C ⊆ E = x → x ∈ V
11 10 adantl ⊢ G ∈ FriendGraph ∧ A ∈ V ∧ C ∈ V ∧ A ≠ C ∧ b ∈ V | A b b C ⊆ E = x → x ∈ V
12 frgrusgr ⊢ G ∈ FriendGraph → G ∈ USGraph
13 1 2 nbusgr ⊢ G ∈ USGraph → G NeighbVtx A = b ∈ V | A b ∈ E
14 1 2 nbusgr ⊢ G ∈ USGraph → G NeighbVtx C = b ∈ V | C b ∈ E
15 13 14 ineq12d ⊢ G ∈ USGraph → G NeighbVtx A ∩ G NeighbVtx C = b ∈ V | A b ∈ E ∩ b ∈ V | C b ∈ E
16 12 15 syl ⊢ G ∈ FriendGraph → G NeighbVtx A ∩ G NeighbVtx C = b ∈ V | A b ∈ E ∩ b ∈ V | C b ∈ E
17 16 adantr ⊢ G ∈ FriendGraph ∧ A ∈ V ∧ C ∈ V ∧ A ≠ C → G NeighbVtx A ∩ G NeighbVtx C = b ∈ V | A b ∈ E ∩ b ∈ V | C b ∈ E
18 17 adantr ⊢ G ∈ FriendGraph ∧ A ∈ V ∧ C ∈ V ∧ A ≠ C ∧ b ∈ V | A b b C ⊆ E = x → G NeighbVtx A ∩ G NeighbVtx C = b ∈ V | A b ∈ E ∩ b ∈ V | C b ∈ E
19 inrab ⊢ b ∈ V | A b ∈ E ∩ b ∈ V | C b ∈ E = b ∈ V | A b ∈ E ∧ C b ∈ E
20 18 19 syl6eq ⊢ G ∈ FriendGraph ∧ A ∈ V ∧ C ∈ V ∧ A ≠ C ∧ b ∈ V | A b b C ⊆ E = x → G NeighbVtx A ∩ G NeighbVtx C = b ∈ V | A b ∈ E ∧ C b ∈ E
21 prcom ⊢ C b = b C
22 21 eleq1i ⊢ C b ∈ E ↔ b C ∈ E
23 22 anbi2i ⊢ A b ∈ E ∧ C b ∈ E ↔ A b ∈ E ∧ b C ∈ E
24 prex ⊢ A b ∈ V
25 prex ⊢ b C ∈ V
26 24 25 prss ⊢ A b ∈ E ∧ b C ∈ E ↔ A b b C ⊆ E
27 23 26 bitri ⊢ A b ∈ E ∧ C b ∈ E ↔ A b b C ⊆ E
28 27 a1i ⊢ G ∈ FriendGraph ∧ A ∈ V ∧ C ∈ V ∧ A ≠ C ∧ b ∈ V → A b ∈ E ∧ C b ∈ E ↔ A b b C ⊆ E
29 28 rabbidva ⊢ G ∈ FriendGraph ∧ A ∈ V ∧ C ∈ V ∧ A ≠ C → b ∈ V | A b ∈ E ∧ C b ∈ E = b ∈ V | A b b C ⊆ E
30 29 adantr ⊢ G ∈ FriendGraph ∧ A ∈ V ∧ C ∈ V ∧ A ≠ C ∧ b ∈ V | A b b C ⊆ E = x → b ∈ V | A b ∈ E ∧ C b ∈ E = b ∈ V | A b b C ⊆ E
31 simpr ⊢ G ∈ FriendGraph ∧ A ∈ V ∧ C ∈ V ∧ A ≠ C ∧ b ∈ V | A b b C ⊆ E = x → b ∈ V | A b b C ⊆ E = x
32 20 30 31 3eqtrd ⊢ G ∈ FriendGraph ∧ A ∈ V ∧ C ∈ V ∧ A ≠ C ∧ b ∈ V | A b b C ⊆ E = x → G NeighbVtx A ∩ G NeighbVtx C = x
33 11 32 jca ⊢ G ∈ FriendGraph ∧ A ∈ V ∧ C ∈ V ∧ A ≠ C ∧ b ∈ V | A b b C ⊆ E = x → x ∈ V ∧ G NeighbVtx A ∩ G NeighbVtx C = x
34 33 ex ⊢ G ∈ FriendGraph ∧ A ∈ V ∧ C ∈ V ∧ A ≠ C → b ∈ V | A b b C ⊆ E = x → x ∈ V ∧ G NeighbVtx A ∩ G NeighbVtx C = x
35 34 eximdv ⊢ G ∈ FriendGraph ∧ A ∈ V ∧ C ∈ V ∧ A ≠ C → ∃ x b ∈ V | A b b C ⊆ E = x → ∃ x x ∈ V ∧ G NeighbVtx A ∩ G NeighbVtx C = x
36 reusn ⊢ ∃! b ∈ V A b b C ⊆ E ↔ ∃ x b ∈ V | A b b C ⊆ E = x
37 df-rex ⊢ ∃ x ∈ V G NeighbVtx A ∩ G NeighbVtx C = x ↔ ∃ x x ∈ V ∧ G NeighbVtx A ∩ G NeighbVtx C = x
38 35 36 37 3imtr4g ⊢ G ∈ FriendGraph ∧ A ∈ V ∧ C ∈ V ∧ A ≠ C → ∃! b ∈ V A b b C ⊆ E → ∃ x ∈ V G NeighbVtx A ∩ G NeighbVtx C = x
39 4 38 mpd ⊢ G ∈ FriendGraph ∧ A ∈ V ∧ C ∈ V ∧ A ≠ C → ∃ x ∈ V G NeighbVtx A ∩ G NeighbVtx C = x
40 39 ex ⊢ G ∈ FriendGraph → A ∈ V ∧ C ∈ V ∧ A ≠ C → ∃ x ∈ V G NeighbVtx A ∩ G NeighbVtx C = x