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 } )