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∈FriendGraph∧FCycles⁡GP→F≠4

Proof

Step Hyp Ref Expression
1 frgrusgr ⊢G∈FriendGraph→G∈USGraph
2 usgrupgr ⊢G∈USGraph→G∈UPGraph
3 1 2 syl ⊢G∈FriendGraph→G∈UPGraph
4 eqid ⊢Vtx⁡G=Vtx⁡G
5 eqid ⊢Edg⁡G=Edg⁡G
6 4 5 upgr4cycl4dv4e ⊢G∈UPGraph∧FCycles⁡GP∧F=4→∃a∈Vtx⁡G∃b∈Vtx⁡G∃c∈Vtx⁡G∃d∈Vtx⁡Gab∈Edg⁡G∧bc∈Edg⁡G∧cd∈Edg⁡G∧da∈Edg⁡G∧a≠b∧a≠c∧a≠d∧b≠c∧b≠d∧c≠d
7 4 5 isfrgr ⊢G∈FriendGraph↔G∈USGraph∧∀k∈Vtx⁡G∀l∈Vtx⁡G∖k∃!x∈Vtx⁡Gxkxl⊆Edg⁡G
8 simplrl ⊢a∈Vtx⁡G∧b∈Vtx⁡G∧c∈Vtx⁡G∧d∈Vtx⁡G∧ab∈Edg⁡G∧bc∈Edg⁡G∧cd∈Edg⁡G∧da∈Edg⁡G∧a≠b∧a≠c∧a≠d∧b≠c∧b≠d∧c≠d→c∈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 ⊢ab∈Edg⁡G∧bc∈Edg⁡G∧cd∈Edg⁡G∧da∈Edg⁡G∧a≠b∧a≠c∧a≠d∧b≠c∧b≠d∧c≠d→c≠a
13 12 adantl ⊢a∈Vtx⁡G∧b∈Vtx⁡G∧c∈Vtx⁡G∧d∈Vtx⁡G∧ab∈Edg⁡G∧bc∈Edg⁡G∧cd∈Edg⁡G∧da∈Edg⁡G∧a≠b∧a≠c∧a≠d∧b≠c∧b≠d∧c≠d→c≠a
14 eldifsn ⊢c∈Vtx⁡G∖a↔c∈Vtx⁡G∧c≠a
15 8 13 14 sylanbrc ⊢a∈Vtx⁡G∧b∈Vtx⁡G∧c∈Vtx⁡G∧d∈Vtx⁡G∧ab∈Edg⁡G∧bc∈Edg⁡G∧cd∈Edg⁡G∧da∈Edg⁡G∧a≠b∧a≠c∧a≠d∧b≠c∧b≠d∧c≠d→c∈Vtx⁡G∖a
16 sneq ⊢k=a→k=a
17 16 difeq2d ⊢k=a→Vtx⁡G∖k=Vtx⁡G∖a
18 preq2 ⊢k=a→xk=xa
19 18 preq1d ⊢k=a→xkxl=xaxl
20 19 sseq1d ⊢k=a→xkxl⊆Edg⁡G↔xaxl⊆Edg⁡G
21 20 reubidv ⊢k=a→∃!x∈Vtx⁡Gxkxl⊆Edg⁡G↔∃!x∈Vtx⁡Gxaxl⊆Edg⁡G
22 17 21 raleqbidv ⊢k=a→∀l∈Vtx⁡G∖k∃!x∈Vtx⁡Gxkxl⊆Edg⁡G↔∀l∈Vtx⁡G∖a∃!x∈Vtx⁡Gxaxl⊆Edg⁡G
23 22 rspcv ⊢a∈Vtx⁡G→∀k∈Vtx⁡G∀l∈Vtx⁡G∖k∃!x∈Vtx⁡Gxkxl⊆Edg⁡G→∀l∈Vtx⁡G∖a∃!x∈Vtx⁡Gxaxl⊆Edg⁡G
24 23 ad3antrrr ⊢a∈Vtx⁡G∧b∈Vtx⁡G∧c∈Vtx⁡G∧d∈Vtx⁡G∧ab∈Edg⁡G∧bc∈Edg⁡G∧cd∈Edg⁡G∧da∈Edg⁡G∧a≠b∧a≠c∧a≠d∧b≠c∧b≠d∧c≠d→∀k∈Vtx⁡G∀l∈Vtx⁡G∖k∃!x∈Vtx⁡Gxkxl⊆Edg⁡G→∀l∈Vtx⁡G∖a∃!x∈Vtx⁡Gxaxl⊆Edg⁡G
25 preq2 ⊢l=c→xl=xc
26 25 preq2d ⊢l=c→xaxl=xaxc
27 26 sseq1d ⊢l=c→xaxl⊆Edg⁡G↔xaxc⊆Edg⁡G
28 27 reubidv ⊢l=c→∃!x∈Vtx⁡Gxaxl⊆Edg⁡G↔∃!x∈Vtx⁡Gxaxc⊆Edg⁡G
29 28 rspcv ⊢c∈Vtx⁡G∖a→∀l∈Vtx⁡G∖a∃!x∈Vtx⁡Gxaxl⊆Edg⁡G→∃!x∈Vtx⁡Gxaxc⊆Edg⁡G
30 15 24 29 sylsyld ⊢a∈Vtx⁡G∧b∈Vtx⁡G∧c∈Vtx⁡G∧d∈Vtx⁡G∧ab∈Edg⁡G∧bc∈Edg⁡G∧cd∈Edg⁡G∧da∈Edg⁡G∧a≠b∧a≠c∧a≠d∧b≠c∧b≠d∧c≠d→∀k∈Vtx⁡G∀l∈Vtx⁡G∖k∃!x∈Vtx⁡Gxkxl⊆Edg⁡G→∃!x∈Vtx⁡Gxaxc⊆Edg⁡G
31 prcom ⊢xa=ax
32 31 preq1i ⊢xaxc=axxc
33 32 sseq1i ⊢xaxc⊆Edg⁡G↔axxc⊆Edg⁡G
34 33 reubii ⊢∃!x∈Vtx⁡Gxaxc⊆Edg⁡G↔∃!x∈Vtx⁡Gaxxc⊆Edg⁡G
35 simprll ⊢a∈Vtx⁡G∧b∈Vtx⁡G∧c∈Vtx⁡G∧d∈Vtx⁡G∧ab∈Edg⁡G∧bc∈Edg⁡G∧cd∈Edg⁡G∧da∈Edg⁡G∧a≠b∧a≠c∧a≠d∧b≠c∧b≠d∧c≠d→ab∈Edg⁡G∧bc∈Edg⁡G
36 simprlr ⊢a∈Vtx⁡G∧b∈Vtx⁡G∧c∈Vtx⁡G∧d∈Vtx⁡G∧ab∈Edg⁡G∧bc∈Edg⁡G∧cd∈Edg⁡G∧da∈Edg⁡G∧a≠b∧a≠c∧a≠d∧b≠c∧b≠d∧c≠d→cd∈Edg⁡G∧da∈Edg⁡G
37 simpllr ⊢a∈Vtx⁡G∧b∈Vtx⁡G∧c∈Vtx⁡G∧d∈Vtx⁡G∧ab∈Edg⁡G∧bc∈Edg⁡G∧cd∈Edg⁡G∧da∈Edg⁡G∧a≠b∧a≠c∧a≠d∧b≠c∧b≠d∧c≠d→b∈Vtx⁡G
38 simplrr ⊢a∈Vtx⁡G∧b∈Vtx⁡G∧c∈Vtx⁡G∧d∈Vtx⁡G∧ab∈Edg⁡G∧bc∈Edg⁡G∧cd∈Edg⁡G∧da∈Edg⁡G∧a≠b∧a≠c∧a≠d∧b≠c∧b≠d∧c≠d→d∈Vtx⁡G
39 simprr2 ⊢ab∈Edg⁡G∧bc∈Edg⁡G∧cd∈Edg⁡G∧da∈Edg⁡G∧a≠b∧a≠c∧a≠d∧b≠c∧b≠d∧c≠d→b≠d
40 39 adantl ⊢a∈Vtx⁡G∧b∈Vtx⁡G∧c∈Vtx⁡G∧d∈Vtx⁡G∧ab∈Edg⁡G∧bc∈Edg⁡G∧cd∈Edg⁡G∧da∈Edg⁡G∧a≠b∧a≠c∧a≠d∧b≠c∧b≠d∧c≠d→b≠d
41 4cycl2vnunb ⊢ab∈Edg⁡G∧bc∈Edg⁡G∧cd∈Edg⁡G∧da∈Edg⁡G∧b∈Vtx⁡G∧d∈Vtx⁡G∧b≠d→¬∃!x∈Vtx⁡Gaxxc⊆Edg⁡G
42 35 36 37 38 40 41 syl113anc ⊢a∈Vtx⁡G∧b∈Vtx⁡G∧c∈Vtx⁡G∧d∈Vtx⁡G∧ab∈Edg⁡G∧bc∈Edg⁡G∧cd∈Edg⁡G∧da∈Edg⁡G∧a≠b∧a≠c∧a≠d∧b≠c∧b≠d∧c≠d→¬∃!x∈Vtx⁡Gaxxc⊆Edg⁡G
43 42 pm2.21d ⊢a∈Vtx⁡G∧b∈Vtx⁡G∧c∈Vtx⁡G∧d∈Vtx⁡G∧ab∈Edg⁡G∧bc∈Edg⁡G∧cd∈Edg⁡G∧da∈Edg⁡G∧a≠b∧a≠c∧a≠d∧b≠c∧b≠d∧c≠d→∃!x∈Vtx⁡Gaxxc⊆Edg⁡G→F≠4
44 43 com12 ⊢∃!x∈Vtx⁡Gaxxc⊆Edg⁡G→a∈Vtx⁡G∧b∈Vtx⁡G∧c∈Vtx⁡G∧d∈Vtx⁡G∧ab∈Edg⁡G∧bc∈Edg⁡G∧cd∈Edg⁡G∧da∈Edg⁡G∧a≠b∧a≠c∧a≠d∧b≠c∧b≠d∧c≠d→F≠4
45 34 44 sylbi ⊢∃!x∈Vtx⁡Gxaxc⊆Edg⁡G→a∈Vtx⁡G∧b∈Vtx⁡G∧c∈Vtx⁡G∧d∈Vtx⁡G∧ab∈Edg⁡G∧bc∈Edg⁡G∧cd∈Edg⁡G∧da∈Edg⁡G∧a≠b∧a≠c∧a≠d∧b≠c∧b≠d∧c≠d→F≠4
46 30 45 syl6 ⊢a∈Vtx⁡G∧b∈Vtx⁡G∧c∈Vtx⁡G∧d∈Vtx⁡G∧ab∈Edg⁡G∧bc∈Edg⁡G∧cd∈Edg⁡G∧da∈Edg⁡G∧a≠b∧a≠c∧a≠d∧b≠c∧b≠d∧c≠d→∀k∈Vtx⁡G∀l∈Vtx⁡G∖k∃!x∈Vtx⁡Gxkxl⊆Edg⁡G→a∈Vtx⁡G∧b∈Vtx⁡G∧c∈Vtx⁡G∧d∈Vtx⁡G∧ab∈Edg⁡G∧bc∈Edg⁡G∧cd∈Edg⁡G∧da∈Edg⁡G∧a≠b∧a≠c∧a≠d∧b≠c∧b≠d∧c≠d→F≠4
47 46 pm2.43b ⊢∀k∈Vtx⁡G∀l∈Vtx⁡G∖k∃!x∈Vtx⁡Gxkxl⊆Edg⁡G→a∈Vtx⁡G∧b∈Vtx⁡G∧c∈Vtx⁡G∧d∈Vtx⁡G∧ab∈Edg⁡G∧bc∈Edg⁡G∧cd∈Edg⁡G∧da∈Edg⁡G∧a≠b∧a≠c∧a≠d∧b≠c∧b≠d∧c≠d→F≠4
48 47 adantl ⊢G∈USGraph∧∀k∈Vtx⁡G∀l∈Vtx⁡G∖k∃!x∈Vtx⁡Gxkxl⊆Edg⁡G→a∈Vtx⁡G∧b∈Vtx⁡G∧c∈Vtx⁡G∧d∈Vtx⁡G∧ab∈Edg⁡G∧bc∈Edg⁡G∧cd∈Edg⁡G∧da∈Edg⁡G∧a≠b∧a≠c∧a≠d∧b≠c∧b≠d∧c≠d→F≠4
49 7 48 sylbi ⊢G∈FriendGraph→a∈Vtx⁡G∧b∈Vtx⁡G∧c∈Vtx⁡G∧d∈Vtx⁡G∧ab∈Edg⁡G∧bc∈Edg⁡G∧cd∈Edg⁡G∧da∈Edg⁡G∧a≠b∧a≠c∧a≠d∧b≠c∧b≠d∧c≠d→F≠4
50 49 expdcom ⊢a∈Vtx⁡G∧b∈Vtx⁡G∧c∈Vtx⁡G∧d∈Vtx⁡G→ab∈Edg⁡G∧bc∈Edg⁡G∧cd∈Edg⁡G∧da∈Edg⁡G∧a≠b∧a≠c∧a≠d∧b≠c∧b≠d∧c≠d→G∈FriendGraph→F≠4
51 50 rexlimdvva ⊢a∈Vtx⁡G∧b∈Vtx⁡G→∃c∈Vtx⁡G∃d∈Vtx⁡Gab∈Edg⁡G∧bc∈Edg⁡G∧cd∈Edg⁡G∧da∈Edg⁡G∧a≠b∧a≠c∧a≠d∧b≠c∧b≠d∧c≠d→G∈FriendGraph→F≠4
52 51 rexlimivv ⊢∃a∈Vtx⁡G∃b∈Vtx⁡G∃c∈Vtx⁡G∃d∈Vtx⁡Gab∈Edg⁡G∧bc∈Edg⁡G∧cd∈Edg⁡G∧da∈Edg⁡G∧a≠b∧a≠c∧a≠d∧b≠c∧b≠d∧c≠d→G∈FriendGraph→F≠4
53 6 52 syl ⊢G∈UPGraph∧FCycles⁡GP∧F=4→G∈FriendGraph→F≠4
54 53 3exp ⊢G∈UPGraph→FCycles⁡GP→F=4→G∈FriendGraph→F≠4
55 54 com34 ⊢G∈UPGraph→FCycles⁡GP→G∈FriendGraph→F=4→F≠4
56 55 com23 ⊢G∈UPGraph→G∈FriendGraph→FCycles⁡GP→F=4→F≠4
57 3 56 mpcom ⊢G∈FriendGraph→FCycles⁡GP→F=4→F≠4
58 57 imp ⊢G∈FriendGraph∧FCycles⁡GP→F=4→F≠4
59 neqne ⊢¬F=4→F≠4
60 58 59 pm2.61d1 ⊢G∈FriendGraph∧FCycles⁡GP→F≠4