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 e. FriendGraph -> ( ( A e. V /\ C e. V /\ A =/= C ) -> E. x e. V ( ( G NeighbVtx A ) i^i ( 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 e. FriendGraph -> ( ( A e. V /\ C e. V /\ A =/= C ) -> E! b e. V { { A , b } , { b , C } } C_ E ) )
4 3 imp 
 |-  ( ( G e. FriendGraph /\ ( A e. V /\ C e. V /\ A =/= C ) ) -> E! b e. V { { A , b } , { b , C } } C_ E )
5 ssrab2 
 |-  { b e. V | { { A , b } , { b , C } } C_ E } C_ V
6 sseq1 
 |-  ( { b e. V | { { A , b } , { b , C } } C_ E } = { x } -> ( { b e. V | { { A , b } , { b , C } } C_ E } C_ V <-> { x } C_ V ) )
7 5 6 mpbii 
 |-  ( { b e. V | { { A , b } , { b , C } } C_ E } = { x } -> { x } C_ V )
8 vex 
 |-  x e. _V
9 8 snss 
 |-  ( x e. V <-> { x } C_ V )
10 7 9 sylibr 
 |-  ( { b e. V | { { A , b } , { b , C } } C_ E } = { x } -> x e. V )
11 10 adantl 
 |-  ( ( ( G e. FriendGraph /\ ( A e. V /\ C e. V /\ A =/= C ) ) /\ { b e. V | { { A , b } , { b , C } } C_ E } = { x } ) -> x e. V )
12 frgrusgr 
 |-  ( G e. FriendGraph -> G e. USGraph )
13 1 2 nbusgr 
 |-  ( G e. USGraph -> ( G NeighbVtx A ) = { b e. V | { A , b } e. E } )
14 1 2 nbusgr 
 |-  ( G e. USGraph -> ( G NeighbVtx C ) = { b e. V | { C , b } e. E } )
15 13 14 ineq12d 
 |-  ( G e. USGraph -> ( ( G NeighbVtx A ) i^i ( G NeighbVtx C ) ) = ( { b e. V | { A , b } e. E } i^i { b e. V | { C , b } e. E } ) )
16 12 15 syl 
 |-  ( G e. FriendGraph -> ( ( G NeighbVtx A ) i^i ( G NeighbVtx C ) ) = ( { b e. V | { A , b } e. E } i^i { b e. V | { C , b } e. E } ) )
17 16 adantr 
 |-  ( ( G e. FriendGraph /\ ( A e. V /\ C e. V /\ A =/= C ) ) -> ( ( G NeighbVtx A ) i^i ( G NeighbVtx C ) ) = ( { b e. V | { A , b } e. E } i^i { b e. V | { C , b } e. E } ) )
18 17 adantr 
 |-  ( ( ( G e. FriendGraph /\ ( A e. V /\ C e. V /\ A =/= C ) ) /\ { b e. V | { { A , b } , { b , C } } C_ E } = { x } ) -> ( ( G NeighbVtx A ) i^i ( G NeighbVtx C ) ) = ( { b e. V | { A , b } e. E } i^i { b e. V | { C , b } e. E } ) )
19 inrab 
 |-  ( { b e. V | { A , b } e. E } i^i { b e. V | { C , b } e. E } ) = { b e. V | ( { A , b } e. E /\ { C , b } e. E ) }
20 18 19 eqtrdi 
 |-  ( ( ( G e. FriendGraph /\ ( A e. V /\ C e. V /\ A =/= C ) ) /\ { b e. V | { { A , b } , { b , C } } C_ E } = { x } ) -> ( ( G NeighbVtx A ) i^i ( G NeighbVtx C ) ) = { b e. V | ( { A , b } e. E /\ { C , b } e. E ) } )
21 prcom 
 |-  { C , b } = { b , C }
22 21 eleq1i 
 |-  ( { C , b } e. E <-> { b , C } e. E )
23 22 anbi2i 
 |-  ( ( { A , b } e. E /\ { C , b } e. E ) <-> ( { A , b } e. E /\ { b , C } e. E ) )
24 prex 
 |-  { A , b } e. _V
25 prex 
 |-  { b , C } e. _V
26 24 25 prss 
 |-  ( ( { A , b } e. E /\ { b , C } e. E ) <-> { { A , b } , { b , C } } C_ E )
27 23 26 bitri 
 |-  ( ( { A , b } e. E /\ { C , b } e. E ) <-> { { A , b } , { b , C } } C_ E )
28 27 a1i 
 |-  ( ( ( G e. FriendGraph /\ ( A e. V /\ C e. V /\ A =/= C ) ) /\ b e. V ) -> ( ( { A , b } e. E /\ { C , b } e. E ) <-> { { A , b } , { b , C } } C_ E ) )
29 28 rabbidva 
 |-  ( ( G e. FriendGraph /\ ( A e. V /\ C e. V /\ A =/= C ) ) -> { b e. V | ( { A , b } e. E /\ { C , b } e. E ) } = { b e. V | { { A , b } , { b , C } } C_ E } )
30 29 adantr 
 |-  ( ( ( G e. FriendGraph /\ ( A e. V /\ C e. V /\ A =/= C ) ) /\ { b e. V | { { A , b } , { b , C } } C_ E } = { x } ) -> { b e. V | ( { A , b } e. E /\ { C , b } e. E ) } = { b e. V | { { A , b } , { b , C } } C_ E } )
31 simpr 
 |-  ( ( ( G e. FriendGraph /\ ( A e. V /\ C e. V /\ A =/= C ) ) /\ { b e. V | { { A , b } , { b , C } } C_ E } = { x } ) -> { b e. V | { { A , b } , { b , C } } C_ E } = { x } )
32 20 30 31 3eqtrd 
 |-  ( ( ( G e. FriendGraph /\ ( A e. V /\ C e. V /\ A =/= C ) ) /\ { b e. V | { { A , b } , { b , C } } C_ E } = { x } ) -> ( ( G NeighbVtx A ) i^i ( G NeighbVtx C ) ) = { x } )
33 11 32 jca 
 |-  ( ( ( G e. FriendGraph /\ ( A e. V /\ C e. V /\ A =/= C ) ) /\ { b e. V | { { A , b } , { b , C } } C_ E } = { x } ) -> ( x e. V /\ ( ( G NeighbVtx A ) i^i ( G NeighbVtx C ) ) = { x } ) )
34 33 ex 
 |-  ( ( G e. FriendGraph /\ ( A e. V /\ C e. V /\ A =/= C ) ) -> ( { b e. V | { { A , b } , { b , C } } C_ E } = { x } -> ( x e. V /\ ( ( G NeighbVtx A ) i^i ( G NeighbVtx C ) ) = { x } ) ) )
35 34 eximdv 
 |-  ( ( G e. FriendGraph /\ ( A e. V /\ C e. V /\ A =/= C ) ) -> ( E. x { b e. V | { { A , b } , { b , C } } C_ E } = { x } -> E. x ( x e. V /\ ( ( G NeighbVtx A ) i^i ( G NeighbVtx C ) ) = { x } ) ) )
36 reusn 
 |-  ( E! b e. V { { A , b } , { b , C } } C_ E <-> E. x { b e. V | { { A , b } , { b , C } } C_ E } = { x } )
37 df-rex 
 |-  ( E. x e. V ( ( G NeighbVtx A ) i^i ( G NeighbVtx C ) ) = { x } <-> E. x ( x e. V /\ ( ( G NeighbVtx A ) i^i ( G NeighbVtx C ) ) = { x } ) )
38 35 36 37 3imtr4g 
 |-  ( ( G e. FriendGraph /\ ( A e. V /\ C e. V /\ A =/= C ) ) -> ( E! b e. V { { A , b } , { b , C } } C_ E -> E. x e. V ( ( G NeighbVtx A ) i^i ( G NeighbVtx C ) ) = { x } ) )
39 4 38 mpd 
 |-  ( ( G e. FriendGraph /\ ( A e. V /\ C e. V /\ A =/= C ) ) -> E. x e. V ( ( G NeighbVtx A ) i^i ( G NeighbVtx C ) ) = { x } )
40 39 ex 
 |-  ( G e. FriendGraph -> ( ( A e. V /\ C e. V /\ A =/= C ) -> E. x e. V ( ( G NeighbVtx A ) i^i ( G NeighbVtx C ) ) = { x } ) )