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 ∧ F Cycles ⁡ G P → 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 ∧ F Cycles ⁡ G P ∧ F = 4 → ∃ a ∈ Vtx ⁡ G ∃ b ∈ Vtx ⁡ G ∃ c ∈ Vtx ⁡ G ∃ d ∈ Vtx ⁡ G a b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c d ∈ Edg ⁡ G ∧ d a ∈ 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 ⁡ G x k x l ⊆ Edg ⁡ G
8 simplrl ⊢ a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ c ∈ Vtx ⁡ G ∧ d ∈ Vtx ⁡ G ∧ a b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c d ∈ Edg ⁡ G ∧ d a ∈ 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 ⊢ a b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c d ∈ Edg ⁡ G ∧ d a ∈ 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 ∧ a b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c d ∈ Edg ⁡ G ∧ d a ∈ 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 ∧ a b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c d ∈ Edg ⁡ G ∧ d a ∈ 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 → 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 ⊆ Edg ⁡ G ↔ x a x l ⊆ Edg ⁡ G
21 20 reubidv ⊢ k = a → ∃! x ∈ Vtx ⁡ G x k x l ⊆ Edg ⁡ G ↔ ∃! x ∈ Vtx ⁡ G x a x l ⊆ Edg ⁡ G
22 17 21 raleqbidv ⊢ k = a → ∀ l ∈ Vtx ⁡ G ∖ k ∃! x ∈ Vtx ⁡ G x k x l ⊆ Edg ⁡ G ↔ ∀ l ∈ Vtx ⁡ G ∖ a ∃! x ∈ Vtx ⁡ G x a x l ⊆ Edg ⁡ G
23 22 rspcv ⊢ a ∈ Vtx ⁡ G → ∀ k ∈ Vtx ⁡ G ∀ l ∈ Vtx ⁡ G ∖ k ∃! x ∈ Vtx ⁡ G x k x l ⊆ Edg ⁡ G → ∀ l ∈ Vtx ⁡ G ∖ a ∃! x ∈ Vtx ⁡ G x a x l ⊆ Edg ⁡ G
24 23 ad3antrrr ⊢ a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ c ∈ Vtx ⁡ G ∧ d ∈ Vtx ⁡ G ∧ a b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c d ∈ Edg ⁡ G ∧ d a ∈ Edg ⁡ G ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d → ∀ k ∈ Vtx ⁡ G ∀ l ∈ Vtx ⁡ G ∖ k ∃! x ∈ Vtx ⁡ G x k x l ⊆ Edg ⁡ G → ∀ l ∈ Vtx ⁡ G ∖ a ∃! x ∈ Vtx ⁡ G x a x l ⊆ 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 ⊆ Edg ⁡ G ↔ x a x c ⊆ Edg ⁡ G
28 27 reubidv ⊢ l = c → ∃! x ∈ Vtx ⁡ G x a x l ⊆ Edg ⁡ G ↔ ∃! x ∈ Vtx ⁡ G x a x c ⊆ Edg ⁡ G
29 28 rspcv ⊢ c ∈ Vtx ⁡ G ∖ a → ∀ l ∈ Vtx ⁡ G ∖ a ∃! x ∈ Vtx ⁡ G x a x l ⊆ Edg ⁡ G → ∃! x ∈ Vtx ⁡ G x a x c ⊆ Edg ⁡ G
30 15 24 29 sylsyld ⊢ a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ c ∈ Vtx ⁡ G ∧ d ∈ Vtx ⁡ G ∧ a b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c d ∈ Edg ⁡ G ∧ d a ∈ Edg ⁡ G ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d → ∀ k ∈ Vtx ⁡ G ∀ l ∈ Vtx ⁡ G ∖ k ∃! x ∈ Vtx ⁡ G x k x l ⊆ Edg ⁡ G → ∃! x ∈ Vtx ⁡ G x a x 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 ⊆ Edg ⁡ G ↔ a x x c ⊆ Edg ⁡ G
34 33 reubii ⊢ ∃! x ∈ Vtx ⁡ G x a x c ⊆ Edg ⁡ G ↔ ∃! x ∈ Vtx ⁡ G a x x c ⊆ Edg ⁡ G
35 simprll ⊢ a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ c ∈ Vtx ⁡ G ∧ d ∈ Vtx ⁡ G ∧ a b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c d ∈ Edg ⁡ G ∧ d a ∈ Edg ⁡ G ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d → a b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G
36 simprlr ⊢ a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ c ∈ Vtx ⁡ G ∧ d ∈ Vtx ⁡ G ∧ a b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c d ∈ Edg ⁡ G ∧ d a ∈ Edg ⁡ G ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d → c d ∈ Edg ⁡ G ∧ d a ∈ Edg ⁡ G
37 simpllr ⊢ a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ c ∈ Vtx ⁡ G ∧ d ∈ Vtx ⁡ G ∧ a b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c d ∈ Edg ⁡ G ∧ d a ∈ 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 ∧ a b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c d ∈ Edg ⁡ G ∧ d a ∈ Edg ⁡ G ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d → d ∈ Vtx ⁡ G
39 simprr2 ⊢ a b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c d ∈ Edg ⁡ G ∧ d a ∈ 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 ∧ a b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c d ∈ Edg ⁡ G ∧ d a ∈ Edg ⁡ G ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d → b ≠ d
41 4cycl2vnunb ⊢ a b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c d ∈ Edg ⁡ G ∧ d a ∈ Edg ⁡ G ∧ b ∈ Vtx ⁡ G ∧ d ∈ Vtx ⁡ G ∧ b ≠ d → ¬ ∃! x ∈ Vtx ⁡ G a x x c ⊆ Edg ⁡ G
42 35 36 37 38 40 41 syl113anc ⊢ a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ c ∈ Vtx ⁡ G ∧ d ∈ Vtx ⁡ G ∧ a b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c d ∈ Edg ⁡ G ∧ d a ∈ Edg ⁡ G ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d → ¬ ∃! x ∈ Vtx ⁡ G a x x c ⊆ Edg ⁡ G
43 42 pm2.21d ⊢ a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ c ∈ Vtx ⁡ G ∧ d ∈ Vtx ⁡ G ∧ a b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c d ∈ Edg ⁡ G ∧ d a ∈ Edg ⁡ G ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d → ∃! x ∈ Vtx ⁡ G a x x c ⊆ Edg ⁡ G → F ≠ 4
44 43 com12 ⊢ ∃! x ∈ Vtx ⁡ G a x x c ⊆ Edg ⁡ G → a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ c ∈ Vtx ⁡ G ∧ d ∈ Vtx ⁡ G ∧ a b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c d ∈ Edg ⁡ G ∧ d a ∈ Edg ⁡ G ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d → F ≠ 4
45 34 44 sylbi ⊢ ∃! x ∈ Vtx ⁡ G x a x c ⊆ Edg ⁡ G → a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ c ∈ Vtx ⁡ G ∧ d ∈ Vtx ⁡ G ∧ a b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c d ∈ Edg ⁡ G ∧ d a ∈ 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 ∧ a b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c d ∈ Edg ⁡ G ∧ d a ∈ Edg ⁡ G ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d → ∀ k ∈ Vtx ⁡ G ∀ l ∈ Vtx ⁡ G ∖ k ∃! x ∈ Vtx ⁡ G x k x l ⊆ Edg ⁡ G → a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ c ∈ Vtx ⁡ G ∧ d ∈ Vtx ⁡ G ∧ a b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c d ∈ Edg ⁡ G ∧ d a ∈ 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 ⁡ G x k x l ⊆ Edg ⁡ G → a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ c ∈ Vtx ⁡ G ∧ d ∈ Vtx ⁡ G ∧ a b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c d ∈ Edg ⁡ G ∧ d a ∈ 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 ⁡ G x k x l ⊆ Edg ⁡ G → a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ c ∈ Vtx ⁡ G ∧ d ∈ Vtx ⁡ G ∧ a b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c d ∈ Edg ⁡ G ∧ d a ∈ 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 ∧ a b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c d ∈ Edg ⁡ G ∧ d a ∈ 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 → a b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c d ∈ Edg ⁡ G ∧ d a ∈ 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 ⁡ G a b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c d ∈ Edg ⁡ G ∧ d a ∈ 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 ⁡ G a b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c d ∈ Edg ⁡ G ∧ d a ∈ Edg ⁡ G ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d → G ∈ FriendGraph → F ≠ 4
53 6 52 syl ⊢ G ∈ UPGraph ∧ F Cycles ⁡ G P ∧ F = 4 → G ∈ FriendGraph → F ≠ 4
54 53 3exp ⊢ G ∈ UPGraph → F Cycles ⁡ G P → F = 4 → G ∈ FriendGraph → F ≠ 4
55 54 com34 ⊢ G ∈ UPGraph → F Cycles ⁡ G P → G ∈ FriendGraph → F = 4 → F ≠ 4
56 55 com23 ⊢ G ∈ UPGraph → G ∈ FriendGraph → F Cycles ⁡ G P → F = 4 → F ≠ 4
57 3 56 mpcom ⊢ G ∈ FriendGraph → F Cycles ⁡ G P → F = 4 → F ≠ 4
58 57 imp ⊢ G ∈ FriendGraph ∧ F Cycles ⁡ G P → F = 4 → F ≠ 4
59 neqne ⊢ ¬ F = 4 → F ≠ 4
60 58 59 pm2.61d1 ⊢ G ∈ FriendGraph ∧ F Cycles ⁡ G P → F ≠ 4