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 eqtrdi 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