Metamath Proof Explorer

Theorem 4cyclusnfrgr

Description: A graph with a 4-cycle is not a friendhip graph. (Contributed by Alexander van der Vekens, 19-Dec-2017) (Revised by AV, 2-Apr-2021)

Ref Expression
Hypotheses 4cyclusnfrgr.v 
|- V = ( Vtx ` G )
4cyclusnfrgr.e 
|- E = ( Edg ` G )
Assertion 4cyclusnfrgr 
|- ( ( G e. USGraph /\ ( A e. V /\ C e. V /\ A =/= C ) /\ ( B e. V /\ D e. V /\ B =/= D ) ) -> ( ( ( { A , B } e. E /\ { B , C } e. E ) /\ ( { C , D } e. E /\ { D , A } e. E ) ) -> G e/ FriendGraph ) )

Proof

Step Hyp Ref Expression
1 4cyclusnfrgr.v 
 |-  V = ( Vtx ` G )
2 4cyclusnfrgr.e 
 |-  E = ( Edg ` G )
3 simprl 
 |-  ( ( ( G e. USGraph /\ ( A e. V /\ C e. V /\ A =/= C ) /\ ( B e. V /\ D e. V /\ B =/= D ) ) /\ ( ( { A , B } e. E /\ { B , C } e. E ) /\ ( { C , D } e. E /\ { D , A } e. E ) ) ) -> ( { A , B } e. E /\ { B , C } e. E ) )
4 simprr 
 |-  ( ( ( G e. USGraph /\ ( A e. V /\ C e. V /\ A =/= C ) /\ ( B e. V /\ D e. V /\ B =/= D ) ) /\ ( ( { A , B } e. E /\ { B , C } e. E ) /\ ( { C , D } e. E /\ { D , A } e. E ) ) ) -> ( { C , D } e. E /\ { D , A } e. E ) )
5 simpl3 
 |-  ( ( ( G e. USGraph /\ ( A e. V /\ C e. V /\ A =/= C ) /\ ( B e. V /\ D e. V /\ B =/= D ) ) /\ ( ( { A , B } e. E /\ { B , C } e. E ) /\ ( { C , D } e. E /\ { D , A } e. E ) ) ) -> ( B e. V /\ D e. V /\ B =/= D ) )
6 4cycl2vnunb 
 |-  ( ( ( { A , B } e. E /\ { B , C } e. E ) /\ ( { C , D } e. E /\ { D , A } e. E ) /\ ( B e. V /\ D e. V /\ B =/= D ) ) -> -. E! x e. V { { A , x } , { x , C } } C_ E )
7 3 4 5 6 syl3anc 
 |-  ( ( ( G e. USGraph /\ ( A e. V /\ C e. V /\ A =/= C ) /\ ( B e. V /\ D e. V /\ B =/= D ) ) /\ ( ( { A , B } e. E /\ { B , C } e. E ) /\ ( { C , D } e. E /\ { D , A } e. E ) ) ) -> -. E! x e. V { { A , x } , { x , C } } C_ E )
8 1 2 frcond1 
 |-  ( G e. FriendGraph -> ( ( A e. V /\ C e. V /\ A =/= C ) -> E! x e. V { { A , x } , { x , C } } C_ E ) )
9 pm2.24 
 |-  ( E! x e. V { { A , x } , { x , C } } C_ E -> ( -. E! x e. V { { A , x } , { x , C } } C_ E -> -. G e. FriendGraph ) )
10 8 9 syl6com 
 |-  ( ( A e. V /\ C e. V /\ A =/= C ) -> ( G e. FriendGraph -> ( -. E! x e. V { { A , x } , { x , C } } C_ E -> -. G e. FriendGraph ) ) )
11 10 3ad2ant2 
 |-  ( ( G e. USGraph /\ ( A e. V /\ C e. V /\ A =/= C ) /\ ( B e. V /\ D e. V /\ B =/= D ) ) -> ( G e. FriendGraph -> ( -. E! x e. V { { A , x } , { x , C } } C_ E -> -. G e. FriendGraph ) ) )
12 11 com23 
 |-  ( ( G e. USGraph /\ ( A e. V /\ C e. V /\ A =/= C ) /\ ( B e. V /\ D e. V /\ B =/= D ) ) -> ( -. E! x e. V { { A , x } , { x , C } } C_ E -> ( G e. FriendGraph -> -. G e. FriendGraph ) ) )
13 12 adantr 
 |-  ( ( ( G e. USGraph /\ ( A e. V /\ C e. V /\ A =/= C ) /\ ( B e. V /\ D e. V /\ B =/= D ) ) /\ ( ( { A , B } e. E /\ { B , C } e. E ) /\ ( { C , D } e. E /\ { D , A } e. E ) ) ) -> ( -. E! x e. V { { A , x } , { x , C } } C_ E -> ( G e. FriendGraph -> -. G e. FriendGraph ) ) )
14 7 13 mpd 
 |-  ( ( ( G e. USGraph /\ ( A e. V /\ C e. V /\ A =/= C ) /\ ( B e. V /\ D e. V /\ B =/= D ) ) /\ ( ( { A , B } e. E /\ { B , C } e. E ) /\ ( { C , D } e. E /\ { D , A } e. E ) ) ) -> ( G e. FriendGraph -> -. G e. FriendGraph ) )
15 14 pm2.01d 
 |-  ( ( ( G e. USGraph /\ ( A e. V /\ C e. V /\ A =/= C ) /\ ( B e. V /\ D e. V /\ B =/= D ) ) /\ ( ( { A , B } e. E /\ { B , C } e. E ) /\ ( { C , D } e. E /\ { D , A } e. E ) ) ) -> -. G e. FriendGraph )
16 df-nel 
 |-  ( G e/ FriendGraph <-> -. G e. FriendGraph )
17 15 16 sylibr 
 |-  ( ( ( G e. USGraph /\ ( A e. V /\ C e. V /\ A =/= C ) /\ ( B e. V /\ D e. V /\ B =/= D ) ) /\ ( ( { A , B } e. E /\ { B , C } e. E ) /\ ( { C , D } e. E /\ { D , A } e. E ) ) ) -> G e/ FriendGraph )
18 17 ex 
 |-  ( ( G e. USGraph /\ ( A e. V /\ C e. V /\ A =/= C ) /\ ( B e. V /\ D e. V /\ B =/= D ) ) -> ( ( ( { A , B } e. E /\ { B , C } e. E ) /\ ( { C , D } e. E /\ { D , A } e. E ) ) -> G e/ FriendGraph ) )