Metamath Proof Explorer

Theorem n4cyclfrgr

Description: There is no 4-cycle in a friendship graph, see Proposition 1(a) of MertziosUnger p. 153 : "A friendship graph G contains no C4 as a subgraph ...". (Contributed by Alexander van der Vekens, 19-Nov-2017) (Revised by AV, 2-Apr-2021)

Ref Expression
Assertion n4cyclfrgr 
|- ( ( G e. FriendGraph /\ F ( Cycles ` G ) P ) -> ( # ` F ) =/= 4 )

Proof

Step Hyp Ref Expression
1 frgrusgr 
 |-  ( G e. FriendGraph -> G e. USGraph )
2 usgrupgr 
 |-  ( G e. USGraph -> G e. UPGraph )
3 1 2 syl 
 |-  ( G e. FriendGraph -> G e. UPGraph )
4 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
5 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
6 4 5 upgr4cycl4dv4e 
 |-  ( ( G e. UPGraph /\ F ( Cycles ` G ) P /\ ( # ` F ) = 4 ) -> E. a e. ( Vtx ` G ) E. b e. ( Vtx ` G ) E. c e. ( Vtx ` G ) E. d e. ( Vtx ` G ) ( ( ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) /\ ( { c , d } e. ( Edg ` G ) /\ { d , a } e. ( Edg ` G ) ) ) /\ ( ( a =/= b /\ a =/= c /\ a =/= d ) /\ ( b =/= c /\ b =/= d /\ c =/= d ) ) ) )
7 4 5 isfrgr 
 |-  ( G e. FriendGraph <-> ( G e. USGraph /\ A. k e. ( Vtx ` G ) A. l e. ( ( Vtx ` G ) \ { k } ) E! x e. ( Vtx ` G ) { { x , k } , { x , l } } C_ ( Edg ` G ) ) )
8 simplrl 
 |-  ( ( ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ ( c e. ( Vtx ` G ) /\ d e. ( Vtx ` G ) ) ) /\ ( ( ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) /\ ( { c , d } e. ( Edg ` G ) /\ { d , a } e. ( Edg ` G ) ) ) /\ ( ( a =/= b /\ a =/= c /\ a =/= d ) /\ ( b =/= c /\ b =/= d /\ c =/= d ) ) ) ) -> c e. ( Vtx ` G ) )
9 necom 
 |-  ( a =/= c <-> c =/= a )
10 9 biimpi 
 |-  ( a =/= c -> c =/= a )
11 10 3ad2ant2 
 |-  ( ( a =/= b /\ a =/= c /\ a =/= d ) -> c =/= a )
12 11 ad2antrl 
 |-  ( ( ( ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) /\ ( { c , d } e. ( Edg ` G ) /\ { d , a } e. ( Edg ` G ) ) ) /\ ( ( a =/= b /\ a =/= c /\ a =/= d ) /\ ( b =/= c /\ b =/= d /\ c =/= d ) ) ) -> c =/= a )
13 12 adantl 
 |-  ( ( ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ ( c e. ( Vtx ` G ) /\ d e. ( Vtx ` G ) ) ) /\ ( ( ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) /\ ( { c , d } e. ( Edg ` G ) /\ { d , a } e. ( Edg ` G ) ) ) /\ ( ( a =/= b /\ a =/= c /\ a =/= d ) /\ ( b =/= c /\ b =/= d /\ c =/= d ) ) ) ) -> c =/= a )
14 eldifsn 
 |-  ( c e. ( ( Vtx ` G ) \ { a } ) <-> ( c e. ( Vtx ` G ) /\ c =/= a ) )
15 8 13 14 sylanbrc 
 |-  ( ( ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ ( c e. ( Vtx ` G ) /\ d e. ( Vtx ` G ) ) ) /\ ( ( ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) /\ ( { c , d } e. ( Edg ` G ) /\ { d , a } e. ( Edg ` G ) ) ) /\ ( ( a =/= b /\ a =/= c /\ a =/= d ) /\ ( b =/= c /\ b =/= d /\ c =/= d ) ) ) ) -> c e. ( ( Vtx ` G ) \ { a } ) )
16 sneq 
 |-  ( k = a -> { k } = { a } )
17 16 difeq2d 
 |-  ( k = a -> ( ( Vtx ` G ) \ { k } ) = ( ( Vtx ` G ) \ { a } ) )
18 preq2 
 |-  ( k = a -> { x , k } = { x , a } )
19 18 preq1d 
 |-  ( k = a -> { { x , k } , { x , l } } = { { x , a } , { x , l } } )
20 19 sseq1d 
 |-  ( k = a -> ( { { x , k } , { x , l } } C_ ( Edg ` G ) <-> { { x , a } , { x , l } } C_ ( Edg ` G ) ) )
21 20 reubidv 
 |-  ( k = a -> ( E! x e. ( Vtx ` G ) { { x , k } , { x , l } } C_ ( Edg ` G ) <-> E! x e. ( Vtx ` G ) { { x , a } , { x , l } } C_ ( Edg ` G ) ) )
22 17 21 raleqbidv 
 |-  ( k = a -> ( A. l e. ( ( Vtx ` G ) \ { k } ) E! x e. ( Vtx ` G ) { { x , k } , { x , l } } C_ ( Edg ` G ) <-> A. l e. ( ( Vtx ` G ) \ { a } ) E! x e. ( Vtx ` G ) { { x , a } , { x , l } } C_ ( Edg ` G ) ) )
23 22 rspcv 
 |-  ( a e. ( Vtx ` G ) -> ( A. k e. ( Vtx ` G ) A. l e. ( ( Vtx ` G ) \ { k } ) E! x e. ( Vtx ` G ) { { x , k } , { x , l } } C_ ( Edg ` G ) -> A. l e. ( ( Vtx ` G ) \ { a } ) E! x e. ( Vtx ` G ) { { x , a } , { x , l } } C_ ( Edg ` G ) ) )
24 23 ad3antrrr 
 |-  ( ( ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ ( c e. ( Vtx ` G ) /\ d e. ( Vtx ` G ) ) ) /\ ( ( ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) /\ ( { c , d } e. ( Edg ` G ) /\ { d , a } e. ( Edg ` G ) ) ) /\ ( ( a =/= b /\ a =/= c /\ a =/= d ) /\ ( b =/= c /\ b =/= d /\ c =/= d ) ) ) ) -> ( A. k e. ( Vtx ` G ) A. l e. ( ( Vtx ` G ) \ { k } ) E! x e. ( Vtx ` G ) { { x , k } , { x , l } } C_ ( Edg ` G ) -> A. l e. ( ( Vtx ` G ) \ { a } ) E! x e. ( Vtx ` G ) { { x , a } , { x , l } } C_ ( Edg ` G ) ) )
25 preq2 
 |-  ( l = c -> { x , l } = { x , c } )
26 25 preq2d 
 |-  ( l = c -> { { x , a } , { x , l } } = { { x , a } , { x , c } } )
27 26 sseq1d 
 |-  ( l = c -> ( { { x , a } , { x , l } } C_ ( Edg ` G ) <-> { { x , a } , { x , c } } C_ ( Edg ` G ) ) )
28 27 reubidv 
 |-  ( l = c -> ( E! x e. ( Vtx ` G ) { { x , a } , { x , l } } C_ ( Edg ` G ) <-> E! x e. ( Vtx ` G ) { { x , a } , { x , c } } C_ ( Edg ` G ) ) )
29 28 rspcv 
 |-  ( c e. ( ( Vtx ` G ) \ { a } ) -> ( A. l e. ( ( Vtx ` G ) \ { a } ) E! x e. ( Vtx ` G ) { { x , a } , { x , l } } C_ ( Edg ` G ) -> E! x e. ( Vtx ` G ) { { x , a } , { x , c } } C_ ( Edg ` G ) ) )
30 15 24 29 sylsyld 
 |-  ( ( ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ ( c e. ( Vtx ` G ) /\ d e. ( Vtx ` G ) ) ) /\ ( ( ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) /\ ( { c , d } e. ( Edg ` G ) /\ { d , a } e. ( Edg ` G ) ) ) /\ ( ( a =/= b /\ a =/= c /\ a =/= d ) /\ ( b =/= c /\ b =/= d /\ c =/= d ) ) ) ) -> ( A. k e. ( Vtx ` G ) A. l e. ( ( Vtx ` G ) \ { k } ) E! x e. ( Vtx ` G ) { { x , k } , { x , l } } C_ ( Edg ` G ) -> E! x e. ( Vtx ` G ) { { x , a } , { x , c } } C_ ( Edg ` G ) ) )
31 prcom 
 |-  { x , a } = { a , x }
32 31 preq1i 
 |-  { { x , a } , { x , c } } = { { a , x } , { x , c } }
33 32 sseq1i 
 |-  ( { { x , a } , { x , c } } C_ ( Edg ` G ) <-> { { a , x } , { x , c } } C_ ( Edg ` G ) )
34 33 reubii 
 |-  ( E! x e. ( Vtx ` G ) { { x , a } , { x , c } } C_ ( Edg ` G ) <-> E! x e. ( Vtx ` G ) { { a , x } , { x , c } } C_ ( Edg ` G ) )
35 simprll 
 |-  ( ( ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ ( c e. ( Vtx ` G ) /\ d e. ( Vtx ` G ) ) ) /\ ( ( ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) /\ ( { c , d } e. ( Edg ` G ) /\ { d , a } e. ( Edg ` G ) ) ) /\ ( ( a =/= b /\ a =/= c /\ a =/= d ) /\ ( b =/= c /\ b =/= d /\ c =/= d ) ) ) ) -> ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) )
36 simprlr 
 |-  ( ( ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ ( c e. ( Vtx ` G ) /\ d e. ( Vtx ` G ) ) ) /\ ( ( ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) /\ ( { c , d } e. ( Edg ` G ) /\ { d , a } e. ( Edg ` G ) ) ) /\ ( ( a =/= b /\ a =/= c /\ a =/= d ) /\ ( b =/= c /\ b =/= d /\ c =/= d ) ) ) ) -> ( { c , d } e. ( Edg ` G ) /\ { d , a } e. ( Edg ` G ) ) )
37 simpllr 
 |-  ( ( ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ ( c e. ( Vtx ` G ) /\ d e. ( Vtx ` G ) ) ) /\ ( ( ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) /\ ( { c , d } e. ( Edg ` G ) /\ { d , a } e. ( Edg ` G ) ) ) /\ ( ( a =/= b /\ a =/= c /\ a =/= d ) /\ ( b =/= c /\ b =/= d /\ c =/= d ) ) ) ) -> b e. ( Vtx ` G ) )
38 simplrr 
 |-  ( ( ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ ( c e. ( Vtx ` G ) /\ d e. ( Vtx ` G ) ) ) /\ ( ( ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) /\ ( { c , d } e. ( Edg ` G ) /\ { d , a } e. ( Edg ` G ) ) ) /\ ( ( a =/= b /\ a =/= c /\ a =/= d ) /\ ( b =/= c /\ b =/= d /\ c =/= d ) ) ) ) -> d e. ( Vtx ` G ) )
39 simprr2 
 |-  ( ( ( ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) /\ ( { c , d } e. ( Edg ` G ) /\ { d , a } e. ( Edg ` G ) ) ) /\ ( ( a =/= b /\ a =/= c /\ a =/= d ) /\ ( b =/= c /\ b =/= d /\ c =/= d ) ) ) -> b =/= d )
40 39 adantl 
 |-  ( ( ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ ( c e. ( Vtx ` G ) /\ d e. ( Vtx ` G ) ) ) /\ ( ( ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) /\ ( { c , d } e. ( Edg ` G ) /\ { d , a } e. ( Edg ` G ) ) ) /\ ( ( a =/= b /\ a =/= c /\ a =/= d ) /\ ( b =/= c /\ b =/= d /\ c =/= d ) ) ) ) -> b =/= d )
41 4cycl2vnunb 
 |-  ( ( ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) /\ ( { c , d } e. ( Edg ` G ) /\ { d , a } e. ( Edg ` G ) ) /\ ( b e. ( Vtx ` G ) /\ d e. ( Vtx ` G ) /\ b =/= d ) ) -> -. E! x e. ( Vtx ` G ) { { a , x } , { x , c } } C_ ( Edg ` G ) )
42 35 36 37 38 40 41 syl113anc 
 |-  ( ( ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ ( c e. ( Vtx ` G ) /\ d e. ( Vtx ` G ) ) ) /\ ( ( ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) /\ ( { c , d } e. ( Edg ` G ) /\ { d , a } e. ( Edg ` G ) ) ) /\ ( ( a =/= b /\ a =/= c /\ a =/= d ) /\ ( b =/= c /\ b =/= d /\ c =/= d ) ) ) ) -> -. E! x e. ( Vtx ` G ) { { a , x } , { x , c } } C_ ( Edg ` G ) )
43 42 pm2.21d 
 |-  ( ( ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ ( c e. ( Vtx ` G ) /\ d e. ( Vtx ` G ) ) ) /\ ( ( ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) /\ ( { c , d } e. ( Edg ` G ) /\ { d , a } e. ( Edg ` G ) ) ) /\ ( ( a =/= b /\ a =/= c /\ a =/= d ) /\ ( b =/= c /\ b =/= d /\ c =/= d ) ) ) ) -> ( E! x e. ( Vtx ` G ) { { a , x } , { x , c } } C_ ( Edg ` G ) -> ( # ` F ) =/= 4 ) )
44 43 com12 
 |-  ( E! x e. ( Vtx ` G ) { { a , x } , { x , c } } C_ ( Edg ` G ) -> ( ( ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ ( c e. ( Vtx ` G ) /\ d e. ( Vtx ` G ) ) ) /\ ( ( ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) /\ ( { c , d } e. ( Edg ` G ) /\ { d , a } e. ( Edg ` G ) ) ) /\ ( ( a =/= b /\ a =/= c /\ a =/= d ) /\ ( b =/= c /\ b =/= d /\ c =/= d ) ) ) ) -> ( # ` F ) =/= 4 ) )
45 34 44 sylbi 
 |-  ( E! x e. ( Vtx ` G ) { { x , a } , { x , c } } C_ ( Edg ` G ) -> ( ( ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ ( c e. ( Vtx ` G ) /\ d e. ( Vtx ` G ) ) ) /\ ( ( ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) /\ ( { c , d } e. ( Edg ` G ) /\ { d , a } e. ( Edg ` G ) ) ) /\ ( ( a =/= b /\ a =/= c /\ a =/= d ) /\ ( b =/= c /\ b =/= d /\ c =/= d ) ) ) ) -> ( # ` F ) =/= 4 ) )
46 30 45 syl6 
 |-  ( ( ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ ( c e. ( Vtx ` G ) /\ d e. ( Vtx ` G ) ) ) /\ ( ( ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) /\ ( { c , d } e. ( Edg ` G ) /\ { d , a } e. ( Edg ` G ) ) ) /\ ( ( a =/= b /\ a =/= c /\ a =/= d ) /\ ( b =/= c /\ b =/= d /\ c =/= d ) ) ) ) -> ( A. k e. ( Vtx ` G ) A. l e. ( ( Vtx ` G ) \ { k } ) E! x e. ( Vtx ` G ) { { x , k } , { x , l } } C_ ( Edg ` G ) -> ( ( ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ ( c e. ( Vtx ` G ) /\ d e. ( Vtx ` G ) ) ) /\ ( ( ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) /\ ( { c , d } e. ( Edg ` G ) /\ { d , a } e. ( Edg ` G ) ) ) /\ ( ( a =/= b /\ a =/= c /\ a =/= d ) /\ ( b =/= c /\ b =/= d /\ c =/= d ) ) ) ) -> ( # ` F ) =/= 4 ) ) )
47 46 pm2.43b 
 |-  ( A. k e. ( Vtx ` G ) A. l e. ( ( Vtx ` G ) \ { k } ) E! x e. ( Vtx ` G ) { { x , k } , { x , l } } C_ ( Edg ` G ) -> ( ( ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ ( c e. ( Vtx ` G ) /\ d e. ( Vtx ` G ) ) ) /\ ( ( ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) /\ ( { c , d } e. ( Edg ` G ) /\ { d , a } e. ( Edg ` G ) ) ) /\ ( ( a =/= b /\ a =/= c /\ a =/= d ) /\ ( b =/= c /\ b =/= d /\ c =/= d ) ) ) ) -> ( # ` F ) =/= 4 ) )
48 47 adantl 
 |-  ( ( G e. USGraph /\ A. k e. ( Vtx ` G ) A. l e. ( ( Vtx ` G ) \ { k } ) E! x e. ( Vtx ` G ) { { x , k } , { x , l } } C_ ( Edg ` G ) ) -> ( ( ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ ( c e. ( Vtx ` G ) /\ d e. ( Vtx ` G ) ) ) /\ ( ( ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) /\ ( { c , d } e. ( Edg ` G ) /\ { d , a } e. ( Edg ` G ) ) ) /\ ( ( a =/= b /\ a =/= c /\ a =/= d ) /\ ( b =/= c /\ b =/= d /\ c =/= d ) ) ) ) -> ( # ` F ) =/= 4 ) )
49 7 48 sylbi 
 |-  ( G e. FriendGraph -> ( ( ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ ( c e. ( Vtx ` G ) /\ d e. ( Vtx ` G ) ) ) /\ ( ( ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) /\ ( { c , d } e. ( Edg ` G ) /\ { d , a } e. ( Edg ` G ) ) ) /\ ( ( a =/= b /\ a =/= c /\ a =/= d ) /\ ( b =/= c /\ b =/= d /\ c =/= d ) ) ) ) -> ( # ` F ) =/= 4 ) )
50 49 expdcom 
 |-  ( ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ ( c e. ( Vtx ` G ) /\ d e. ( Vtx ` G ) ) ) -> ( ( ( ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) /\ ( { c , d } e. ( Edg ` G ) /\ { d , a } e. ( Edg ` G ) ) ) /\ ( ( a =/= b /\ a =/= c /\ a =/= d ) /\ ( b =/= c /\ b =/= d /\ c =/= d ) ) ) -> ( G e. FriendGraph -> ( # ` F ) =/= 4 ) ) )
51 50 rexlimdvva 
 |-  ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) -> ( E. c e. ( Vtx ` G ) E. d e. ( Vtx ` G ) ( ( ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) /\ ( { c , d } e. ( Edg ` G ) /\ { d , a } e. ( Edg ` G ) ) ) /\ ( ( a =/= b /\ a =/= c /\ a =/= d ) /\ ( b =/= c /\ b =/= d /\ c =/= d ) ) ) -> ( G e. FriendGraph -> ( # ` F ) =/= 4 ) ) )
52 51 rexlimivv 
 |-  ( E. a e. ( Vtx ` G ) E. b e. ( Vtx ` G ) E. c e. ( Vtx ` G ) E. d e. ( Vtx ` G ) ( ( ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) /\ ( { c , d } e. ( Edg ` G ) /\ { d , a } e. ( Edg ` G ) ) ) /\ ( ( a =/= b /\ a =/= c /\ a =/= d ) /\ ( b =/= c /\ b =/= d /\ c =/= d ) ) ) -> ( G e. FriendGraph -> ( # ` F ) =/= 4 ) )
53 6 52 syl 
 |-  ( ( G e. UPGraph /\ F ( Cycles ` G ) P /\ ( # ` F ) = 4 ) -> ( G e. FriendGraph -> ( # ` F ) =/= 4 ) )
54 53 3exp 
 |-  ( G e. UPGraph -> ( F ( Cycles ` G ) P -> ( ( # ` F ) = 4 -> ( G e. FriendGraph -> ( # ` F ) =/= 4 ) ) ) )
55 54 com34 
 |-  ( G e. UPGraph -> ( F ( Cycles ` G ) P -> ( G e. FriendGraph -> ( ( # ` F ) = 4 -> ( # ` F ) =/= 4 ) ) ) )
56 55 com23 
 |-  ( G e. UPGraph -> ( G e. FriendGraph -> ( F ( Cycles ` G ) P -> ( ( # ` F ) = 4 -> ( # ` F ) =/= 4 ) ) ) )
57 3 56 mpcom 
 |-  ( G e. FriendGraph -> ( F ( Cycles ` G ) P -> ( ( # ` F ) = 4 -> ( # ` F ) =/= 4 ) ) )
58 57 imp 
 |-  ( ( G e. FriendGraph /\ F ( Cycles ` G ) P ) -> ( ( # ` F ) = 4 -> ( # ` F ) =/= 4 ) )
59 neqne 
 |-  ( -. ( # ` F ) = 4 -> ( # ` F ) =/= 4 )
60 58 59 pm2.61d1 
 |-  ( ( G e. FriendGraph /\ F ( Cycles ` G ) P ) -> ( # ` F ) =/= 4 )