Metamath Proof Explorer

Theorem frcond4

Description: The friendship condition, alternatively expressed by neighborhoods: in a friendship graph, the neighborhoods of two different vertices have exactly one vertex in common. (Contributed by Alexander van der Vekens, 19-Dec-2017) (Revised by AV, 29-Mar-2021) (Proof shortened by AV, 30-Dec-2021)

Ref Expression
Hypotheses frcond1.v
`|- V = ( Vtx ` G )`
frcond1.e
`|- E = ( Edg ` G )`
Assertion frcond4
`|- ( G e. FriendGraph -> A. k e. V A. l e. ( V \ { k } ) E. x e. V ( ( G NeighbVtx k ) i^i ( G NeighbVtx l ) ) = { x } )`

Proof

Step Hyp Ref Expression
1 frcond1.v
` |-  V = ( Vtx ` G )`
2 frcond1.e
` |-  E = ( Edg ` G )`
3 1 2 frcond3
` |-  ( G e. FriendGraph -> ( ( k e. V /\ l e. V /\ k =/= l ) -> E. x e. V ( ( G NeighbVtx k ) i^i ( G NeighbVtx l ) ) = { x } ) )`
4 eldifsn
` |-  ( l e. ( V \ { k } ) <-> ( l e. V /\ l =/= k ) )`
5 necom
` |-  ( l =/= k <-> k =/= l )`
6 5 biimpi
` |-  ( l =/= k -> k =/= l )`
7 6 anim2i
` |-  ( ( l e. V /\ l =/= k ) -> ( l e. V /\ k =/= l ) )`
8 4 7 sylbi
` |-  ( l e. ( V \ { k } ) -> ( l e. V /\ k =/= l ) )`
9 8 anim2i
` |-  ( ( k e. V /\ l e. ( V \ { k } ) ) -> ( k e. V /\ ( l e. V /\ k =/= l ) ) )`
10 3anass
` |-  ( ( k e. V /\ l e. V /\ k =/= l ) <-> ( k e. V /\ ( l e. V /\ k =/= l ) ) )`
11 9 10 sylibr
` |-  ( ( k e. V /\ l e. ( V \ { k } ) ) -> ( k e. V /\ l e. V /\ k =/= l ) )`
12 3 11 impel
` |-  ( ( G e. FriendGraph /\ ( k e. V /\ l e. ( V \ { k } ) ) ) -> E. x e. V ( ( G NeighbVtx k ) i^i ( G NeighbVtx l ) ) = { x } )`
13 12 ralrimivva
` |-  ( G e. FriendGraph -> A. k e. V A. l e. ( V \ { k } ) E. x e. V ( ( G NeighbVtx k ) i^i ( G NeighbVtx l ) ) = { x } )`