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∈VGNeighbVtxA∩GNeighbVtxC=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∈VAbbC⊆E
4 3 imp ⊢G∈FriendGraph∧A∈V∧C∈V∧A≠C→∃!b∈VAbbC⊆E
5 ssrab2 ⊢b∈V|AbbC⊆E⊆V
6 sseq1 ⊢b∈V|AbbC⊆E=x→b∈V|AbbC⊆E⊆V↔x⊆V
7 5 6 mpbii ⊢b∈V|AbbC⊆E=x→x⊆V
8 vex ⊢x∈V
9 8 snss ⊢x∈V↔x⊆V
10 7 9 sylibr ⊢b∈V|AbbC⊆E=x→x∈V
11 10 adantl ⊢G∈FriendGraph∧A∈V∧C∈V∧A≠C∧b∈V|AbbC⊆E=x→x∈V
12 frgrusgr ⊢G∈FriendGraph→G∈USGraph
13 1 2 nbusgr ⊢G∈USGraph→GNeighbVtxA=b∈V|Ab∈E
14 1 2 nbusgr ⊢G∈USGraph→GNeighbVtxC=b∈V|Cb∈E
15 13 14 ineq12d ⊢G∈USGraph→GNeighbVtxA∩GNeighbVtxC=b∈V|Ab∈E∩b∈V|Cb∈E
16 12 15 syl ⊢G∈FriendGraph→GNeighbVtxA∩GNeighbVtxC=b∈V|Ab∈E∩b∈V|Cb∈E
17 16 adantr ⊢G∈FriendGraph∧A∈V∧C∈V∧A≠C→GNeighbVtxA∩GNeighbVtxC=b∈V|Ab∈E∩b∈V|Cb∈E
18 17 adantr ⊢G∈FriendGraph∧A∈V∧C∈V∧A≠C∧b∈V|AbbC⊆E=x→GNeighbVtxA∩GNeighbVtxC=b∈V|Ab∈E∩b∈V|Cb∈E
19 inrab ⊢b∈V|Ab∈E∩b∈V|Cb∈E=b∈V|Ab∈E∧Cb∈E
20 18 19 eqtrdi ⊢G∈FriendGraph∧A∈V∧C∈V∧A≠C∧b∈V|AbbC⊆E=x→GNeighbVtxA∩GNeighbVtxC=b∈V|Ab∈E∧Cb∈E
21 prcom ⊢Cb=bC
22 21 eleq1i ⊢Cb∈E↔bC∈E
23 22 anbi2i ⊢Ab∈E∧Cb∈E↔Ab∈E∧bC∈E
24 prex ⊢Ab∈V
25 prex ⊢bC∈V
26 24 25 prss ⊢Ab∈E∧bC∈E↔AbbC⊆E
27 23 26 bitri ⊢Ab∈E∧Cb∈E↔AbbC⊆E
28 27 a1i ⊢G∈FriendGraph∧A∈V∧C∈V∧A≠C∧b∈V→Ab∈E∧Cb∈E↔AbbC⊆E
29 28 rabbidva ⊢G∈FriendGraph∧A∈V∧C∈V∧A≠C→b∈V|Ab∈E∧Cb∈E=b∈V|AbbC⊆E
30 29 adantr ⊢G∈FriendGraph∧A∈V∧C∈V∧A≠C∧b∈V|AbbC⊆E=x→b∈V|Ab∈E∧Cb∈E=b∈V|AbbC⊆E
31 simpr ⊢G∈FriendGraph∧A∈V∧C∈V∧A≠C∧b∈V|AbbC⊆E=x→b∈V|AbbC⊆E=x
32 20 30 31 3eqtrd ⊢G∈FriendGraph∧A∈V∧C∈V∧A≠C∧b∈V|AbbC⊆E=x→GNeighbVtxA∩GNeighbVtxC=x
33 11 32 jca ⊢G∈FriendGraph∧A∈V∧C∈V∧A≠C∧b∈V|AbbC⊆E=x→x∈V∧GNeighbVtxA∩GNeighbVtxC=x
34 33 ex ⊢G∈FriendGraph∧A∈V∧C∈V∧A≠C→b∈V|AbbC⊆E=x→x∈V∧GNeighbVtxA∩GNeighbVtxC=x
35 34 eximdv ⊢G∈FriendGraph∧A∈V∧C∈V∧A≠C→∃xb∈V|AbbC⊆E=x→∃xx∈V∧GNeighbVtxA∩GNeighbVtxC=x
36 reusn ⊢∃!b∈VAbbC⊆E↔∃xb∈V|AbbC⊆E=x
37 df-rex ⊢∃x∈VGNeighbVtxA∩GNeighbVtxC=x↔∃xx∈V∧GNeighbVtxA∩GNeighbVtxC=x
38 35 36 37 3imtr4g ⊢G∈FriendGraph∧A∈V∧C∈V∧A≠C→∃!b∈VAbbC⊆E→∃x∈VGNeighbVtxA∩GNeighbVtxC=x
39 4 38 mpd ⊢G∈FriendGraph∧A∈V∧C∈V∧A≠C→∃x∈VGNeighbVtxA∩GNeighbVtxC=x
40 39 ex ⊢G∈FriendGraph→A∈V∧C∈V∧A≠C→∃x∈VGNeighbVtxA∩GNeighbVtxC=x