Metamath Proof Explorer

Theorem 3cyclfrgrrn1

Description: Every vertex in a friendship graph (with more than 1 vertex) is part of a 3-cycle. (Contributed by Alexander van der Vekens, 16-Nov-2017) (Revised by AV, 2-Apr-2021)

Ref Expression
Hypotheses 3cyclfrgrrn1.v ⊢ V = Vtx ⁡ G
3cyclfrgrrn1.e ⊢ E = Edg ⁡ G
Assertion 3cyclfrgrrn1 ⊢ G ∈ FriendGraph ∧ A ∈ V ∧ C ∈ V ∧ A ≠ C → ∃ b ∈ V ∃ c ∈ V A b ∈ E ∧ b c ∈ E ∧ c A ∈ E

Proof

Step Hyp Ref Expression
1 3cyclfrgrrn1.v ⊢ V = Vtx ⁡ G
2 3cyclfrgrrn1.e ⊢ E = Edg ⁡ G
3 1 2 2pthfrgrrn2 ⊢ G ∈ FriendGraph → ∀ a ∈ V ∀ z ∈ V ∖ a ∃ x ∈ V a x ∈ E ∧ x z ∈ E ∧ a ≠ x ∧ x ≠ z
4 necom ⊢ A ≠ C ↔ C ≠ A
5 eldifsn ⊢ C ∈ V ∖ A ↔ C ∈ V ∧ C ≠ A
6 5 simplbi2com ⊢ C ≠ A → C ∈ V → C ∈ V ∖ A
7 4 6 sylbi ⊢ A ≠ C → C ∈ V → C ∈ V ∖ A
8 7 com12 ⊢ C ∈ V → A ≠ C → C ∈ V ∖ A
9 8 adantl ⊢ A ∈ V ∧ C ∈ V → A ≠ C → C ∈ V ∖ A
10 9 imp ⊢ A ∈ V ∧ C ∈ V ∧ A ≠ C → C ∈ V ∖ A
11 sneq ⊢ a = A → a = A
12 11 difeq2d ⊢ a = A → V ∖ a = V ∖ A
13 preq1 ⊢ a = A → a x = A x
14 13 eleq1d ⊢ a = A → a x ∈ E ↔ A x ∈ E
15 14 anbi1d ⊢ a = A → a x ∈ E ∧ x z ∈ E ↔ A x ∈ E ∧ x z ∈ E
16 neeq1 ⊢ a = A → a ≠ x ↔ A ≠ x
17 16 anbi1d ⊢ a = A → a ≠ x ∧ x ≠ z ↔ A ≠ x ∧ x ≠ z
18 15 17 anbi12d ⊢ a = A → a x ∈ E ∧ x z ∈ E ∧ a ≠ x ∧ x ≠ z ↔ A x ∈ E ∧ x z ∈ E ∧ A ≠ x ∧ x ≠ z
19 18 rexbidv ⊢ a = A → ∃ x ∈ V a x ∈ E ∧ x z ∈ E ∧ a ≠ x ∧ x ≠ z ↔ ∃ x ∈ V A x ∈ E ∧ x z ∈ E ∧ A ≠ x ∧ x ≠ z
20 12 19 raleqbidv ⊢ a = A → ∀ z ∈ V ∖ a ∃ x ∈ V a x ∈ E ∧ x z ∈ E ∧ a ≠ x ∧ x ≠ z ↔ ∀ z ∈ V ∖ A ∃ x ∈ V A x ∈ E ∧ x z ∈ E ∧ A ≠ x ∧ x ≠ z
21 20 rspcv ⊢ A ∈ V → ∀ a ∈ V ∀ z ∈ V ∖ a ∃ x ∈ V a x ∈ E ∧ x z ∈ E ∧ a ≠ x ∧ x ≠ z → ∀ z ∈ V ∖ A ∃ x ∈ V A x ∈ E ∧ x z ∈ E ∧ A ≠ x ∧ x ≠ z
22 21 ad2antrr ⊢ A ∈ V ∧ C ∈ V ∧ A ≠ C → ∀ a ∈ V ∀ z ∈ V ∖ a ∃ x ∈ V a x ∈ E ∧ x z ∈ E ∧ a ≠ x ∧ x ≠ z → ∀ z ∈ V ∖ A ∃ x ∈ V A x ∈ E ∧ x z ∈ E ∧ A ≠ x ∧ x ≠ z
23 preq2 ⊢ z = C → x z = x C
24 23 eleq1d ⊢ z = C → x z ∈ E ↔ x C ∈ E
25 24 anbi2d ⊢ z = C → A x ∈ E ∧ x z ∈ E ↔ A x ∈ E ∧ x C ∈ E
26 neeq2 ⊢ z = C → x ≠ z ↔ x ≠ C
27 26 anbi2d ⊢ z = C → A ≠ x ∧ x ≠ z ↔ A ≠ x ∧ x ≠ C
28 25 27 anbi12d ⊢ z = C → A x ∈ E ∧ x z ∈ E ∧ A ≠ x ∧ x ≠ z ↔ A x ∈ E ∧ x C ∈ E ∧ A ≠ x ∧ x ≠ C
29 28 rexbidv ⊢ z = C → ∃ x ∈ V A x ∈ E ∧ x z ∈ E ∧ A ≠ x ∧ x ≠ z ↔ ∃ x ∈ V A x ∈ E ∧ x C ∈ E ∧ A ≠ x ∧ x ≠ C
30 29 rspcv ⊢ C ∈ V ∖ A → ∀ z ∈ V ∖ A ∃ x ∈ V A x ∈ E ∧ x z ∈ E ∧ A ≠ x ∧ x ≠ z → ∃ x ∈ V A x ∈ E ∧ x C ∈ E ∧ A ≠ x ∧ x ≠ C
31 10 22 30 sylsyld ⊢ A ∈ V ∧ C ∈ V ∧ A ≠ C → ∀ a ∈ V ∀ z ∈ V ∖ a ∃ x ∈ V a x ∈ E ∧ x z ∈ E ∧ a ≠ x ∧ x ≠ z → ∃ x ∈ V A x ∈ E ∧ x C ∈ E ∧ A ≠ x ∧ x ≠ C
32 1 2 2pthfrgrrn ⊢ G ∈ FriendGraph → ∀ u ∈ V ∀ v ∈ V ∖ u ∃ y ∈ V u y ∈ E ∧ y v ∈ E
33 necom ⊢ A ≠ x ↔ x ≠ A
34 eldifsn ⊢ x ∈ V ∖ A ↔ x ∈ V ∧ x ≠ A
35 34 simplbi2com ⊢ x ≠ A → x ∈ V → x ∈ V ∖ A
36 33 35 sylbi ⊢ A ≠ x → x ∈ V → x ∈ V ∖ A
37 36 adantr ⊢ A ≠ x ∧ A ∈ V → x ∈ V → x ∈ V ∖ A
38 37 imp ⊢ A ≠ x ∧ A ∈ V ∧ x ∈ V → x ∈ V ∖ A
39 sneq ⊢ u = A → u = A
40 39 difeq2d ⊢ u = A → V ∖ u = V ∖ A
41 preq1 ⊢ u = A → u y = A y
42 41 eleq1d ⊢ u = A → u y ∈ E ↔ A y ∈ E
43 42 anbi1d ⊢ u = A → u y ∈ E ∧ y v ∈ E ↔ A y ∈ E ∧ y v ∈ E
44 43 rexbidv ⊢ u = A → ∃ y ∈ V u y ∈ E ∧ y v ∈ E ↔ ∃ y ∈ V A y ∈ E ∧ y v ∈ E
45 40 44 raleqbidv ⊢ u = A → ∀ v ∈ V ∖ u ∃ y ∈ V u y ∈ E ∧ y v ∈ E ↔ ∀ v ∈ V ∖ A ∃ y ∈ V A y ∈ E ∧ y v ∈ E
46 45 rspcv ⊢ A ∈ V → ∀ u ∈ V ∀ v ∈ V ∖ u ∃ y ∈ V u y ∈ E ∧ y v ∈ E → ∀ v ∈ V ∖ A ∃ y ∈ V A y ∈ E ∧ y v ∈ E
47 46 adantl ⊢ A ≠ x ∧ A ∈ V → ∀ u ∈ V ∀ v ∈ V ∖ u ∃ y ∈ V u y ∈ E ∧ y v ∈ E → ∀ v ∈ V ∖ A ∃ y ∈ V A y ∈ E ∧ y v ∈ E
48 47 adantr ⊢ A ≠ x ∧ A ∈ V ∧ x ∈ V → ∀ u ∈ V ∀ v ∈ V ∖ u ∃ y ∈ V u y ∈ E ∧ y v ∈ E → ∀ v ∈ V ∖ A ∃ y ∈ V A y ∈ E ∧ y v ∈ E
49 preq2 ⊢ v = x → y v = y x
50 49 eleq1d ⊢ v = x → y v ∈ E ↔ y x ∈ E
51 50 anbi2d ⊢ v = x → A y ∈ E ∧ y v ∈ E ↔ A y ∈ E ∧ y x ∈ E
52 51 rexbidv ⊢ v = x → ∃ y ∈ V A y ∈ E ∧ y v ∈ E ↔ ∃ y ∈ V A y ∈ E ∧ y x ∈ E
53 52 rspcv ⊢ x ∈ V ∖ A → ∀ v ∈ V ∖ A ∃ y ∈ V A y ∈ E ∧ y v ∈ E → ∃ y ∈ V A y ∈ E ∧ y x ∈ E
54 38 48 53 sylsyld ⊢ A ≠ x ∧ A ∈ V ∧ x ∈ V → ∀ u ∈ V ∀ v ∈ V ∖ u ∃ y ∈ V u y ∈ E ∧ y v ∈ E → ∃ y ∈ V A y ∈ E ∧ y x ∈ E
55 prcom ⊢ A y = y A
56 55 eleq1i ⊢ A y ∈ E ↔ y A ∈ E
57 prcom ⊢ y x = x y
58 57 eleq1i ⊢ y x ∈ E ↔ x y ∈ E
59 56 58 anbi12ci ⊢ A y ∈ E ∧ y x ∈ E ↔ x y ∈ E ∧ y A ∈ E
60 preq2 ⊢ b = x → A b = A x
61 60 eleq1d ⊢ b = x → A b ∈ E ↔ A x ∈ E
62 preq1 ⊢ b = x → b c = x c
63 62 eleq1d ⊢ b = x → b c ∈ E ↔ x c ∈ E
64 biidd ⊢ b = x → c A ∈ E ↔ c A ∈ E
65 61 63 64 3anbi123d ⊢ b = x → A b ∈ E ∧ b c ∈ E ∧ c A ∈ E ↔ A x ∈ E ∧ x c ∈ E ∧ c A ∈ E
66 biidd ⊢ c = y → A x ∈ E ↔ A x ∈ E
67 preq2 ⊢ c = y → x c = x y
68 67 eleq1d ⊢ c = y → x c ∈ E ↔ x y ∈ E
69 preq1 ⊢ c = y → c A = y A
70 69 eleq1d ⊢ c = y → c A ∈ E ↔ y A ∈ E
71 66 68 70 3anbi123d ⊢ c = y → A x ∈ E ∧ x c ∈ E ∧ c A ∈ E ↔ A x ∈ E ∧ x y ∈ E ∧ y A ∈ E
72 65 71 rspc2ev ⊢ x ∈ V ∧ y ∈ V ∧ A x ∈ E ∧ x y ∈ E ∧ y A ∈ E → ∃ b ∈ V ∃ c ∈ V A b ∈ E ∧ b c ∈ E ∧ c A ∈ E
73 72 3expa ⊢ x ∈ V ∧ y ∈ V ∧ A x ∈ E ∧ x y ∈ E ∧ y A ∈ E → ∃ b ∈ V ∃ c ∈ V A b ∈ E ∧ b c ∈ E ∧ c A ∈ E
74 73 expcom ⊢ A x ∈ E ∧ x y ∈ E ∧ y A ∈ E → x ∈ V ∧ y ∈ V → ∃ b ∈ V ∃ c ∈ V A b ∈ E ∧ b c ∈ E ∧ c A ∈ E
75 74 3expib ⊢ A x ∈ E → x y ∈ E ∧ y A ∈ E → x ∈ V ∧ y ∈ V → ∃ b ∈ V ∃ c ∈ V A b ∈ E ∧ b c ∈ E ∧ c A ∈ E
76 59 75 syl5bi ⊢ A x ∈ E → A y ∈ E ∧ y x ∈ E → x ∈ V ∧ y ∈ V → ∃ b ∈ V ∃ c ∈ V A b ∈ E ∧ b c ∈ E ∧ c A ∈ E
77 76 adantr ⊢ A x ∈ E ∧ x C ∈ E → A y ∈ E ∧ y x ∈ E → x ∈ V ∧ y ∈ V → ∃ b ∈ V ∃ c ∈ V A b ∈ E ∧ b c ∈ E ∧ c A ∈ E
78 77 com13 ⊢ x ∈ V ∧ y ∈ V → A y ∈ E ∧ y x ∈ E → A x ∈ E ∧ x C ∈ E → ∃ b ∈ V ∃ c ∈ V A b ∈ E ∧ b c ∈ E ∧ c A ∈ E
79 78 rexlimdva ⊢ x ∈ V → ∃ y ∈ V A y ∈ E ∧ y x ∈ E → A x ∈ E ∧ x C ∈ E → ∃ b ∈ V ∃ c ∈ V A b ∈ E ∧ b c ∈ E ∧ c A ∈ E
80 79 com13 ⊢ A x ∈ E ∧ x C ∈ E → ∃ y ∈ V A y ∈ E ∧ y x ∈ E → x ∈ V → ∃ b ∈ V ∃ c ∈ V A b ∈ E ∧ b c ∈ E ∧ c A ∈ E
81 54 80 syl9 ⊢ A ≠ x ∧ A ∈ V ∧ x ∈ V → A x ∈ E ∧ x C ∈ E → ∀ u ∈ V ∀ v ∈ V ∖ u ∃ y ∈ V u y ∈ E ∧ y v ∈ E → x ∈ V → ∃ b ∈ V ∃ c ∈ V A b ∈ E ∧ b c ∈ E ∧ c A ∈ E
82 81 exp31 ⊢ A ≠ x → A ∈ V → x ∈ V → A x ∈ E ∧ x C ∈ E → ∀ u ∈ V ∀ v ∈ V ∖ u ∃ y ∈ V u y ∈ E ∧ y v ∈ E → x ∈ V → ∃ b ∈ V ∃ c ∈ V A b ∈ E ∧ b c ∈ E ∧ c A ∈ E
83 82 com24 ⊢ A ≠ x → A x ∈ E ∧ x C ∈ E → x ∈ V → A ∈ V → ∀ u ∈ V ∀ v ∈ V ∖ u ∃ y ∈ V u y ∈ E ∧ y v ∈ E → x ∈ V → ∃ b ∈ V ∃ c ∈ V A b ∈ E ∧ b c ∈ E ∧ c A ∈ E
84 83 adantr ⊢ A ≠ x ∧ x ≠ C → A x ∈ E ∧ x C ∈ E → x ∈ V → A ∈ V → ∀ u ∈ V ∀ v ∈ V ∖ u ∃ y ∈ V u y ∈ E ∧ y v ∈ E → x ∈ V → ∃ b ∈ V ∃ c ∈ V A b ∈ E ∧ b c ∈ E ∧ c A ∈ E
85 84 impcom ⊢ A x ∈ E ∧ x C ∈ E ∧ A ≠ x ∧ x ≠ C → x ∈ V → A ∈ V → ∀ u ∈ V ∀ v ∈ V ∖ u ∃ y ∈ V u y ∈ E ∧ y v ∈ E → x ∈ V → ∃ b ∈ V ∃ c ∈ V A b ∈ E ∧ b c ∈ E ∧ c A ∈ E
86 85 com15 ⊢ x ∈ V → x ∈ V → A ∈ V → ∀ u ∈ V ∀ v ∈ V ∖ u ∃ y ∈ V u y ∈ E ∧ y v ∈ E → A x ∈ E ∧ x C ∈ E ∧ A ≠ x ∧ x ≠ C → ∃ b ∈ V ∃ c ∈ V A b ∈ E ∧ b c ∈ E ∧ c A ∈ E
87 86 pm2.43i ⊢ x ∈ V → A ∈ V → ∀ u ∈ V ∀ v ∈ V ∖ u ∃ y ∈ V u y ∈ E ∧ y v ∈ E → A x ∈ E ∧ x C ∈ E ∧ A ≠ x ∧ x ≠ C → ∃ b ∈ V ∃ c ∈ V A b ∈ E ∧ b c ∈ E ∧ c A ∈ E
88 87 com12 ⊢ A ∈ V → x ∈ V → ∀ u ∈ V ∀ v ∈ V ∖ u ∃ y ∈ V u y ∈ E ∧ y v ∈ E → A x ∈ E ∧ x C ∈ E ∧ A ≠ x ∧ x ≠ C → ∃ b ∈ V ∃ c ∈ V A b ∈ E ∧ b c ∈ E ∧ c A ∈ E
89 88 ad2antrr ⊢ A ∈ V ∧ C ∈ V ∧ A ≠ C → x ∈ V → ∀ u ∈ V ∀ v ∈ V ∖ u ∃ y ∈ V u y ∈ E ∧ y v ∈ E → A x ∈ E ∧ x C ∈ E ∧ A ≠ x ∧ x ≠ C → ∃ b ∈ V ∃ c ∈ V A b ∈ E ∧ b c ∈ E ∧ c A ∈ E
90 89 com4t ⊢ ∀ u ∈ V ∀ v ∈ V ∖ u ∃ y ∈ V u y ∈ E ∧ y v ∈ E → A x ∈ E ∧ x C ∈ E ∧ A ≠ x ∧ x ≠ C → A ∈ V ∧ C ∈ V ∧ A ≠ C → x ∈ V → ∃ b ∈ V ∃ c ∈ V A b ∈ E ∧ b c ∈ E ∧ c A ∈ E
91 32 90 syl ⊢ G ∈ FriendGraph → A x ∈ E ∧ x C ∈ E ∧ A ≠ x ∧ x ≠ C → A ∈ V ∧ C ∈ V ∧ A ≠ C → x ∈ V → ∃ b ∈ V ∃ c ∈ V A b ∈ E ∧ b c ∈ E ∧ c A ∈ E
92 91 com14 ⊢ x ∈ V → A x ∈ E ∧ x C ∈ E ∧ A ≠ x ∧ x ≠ C → A ∈ V ∧ C ∈ V ∧ A ≠ C → G ∈ FriendGraph → ∃ b ∈ V ∃ c ∈ V A b ∈ E ∧ b c ∈ E ∧ c A ∈ E
93 92 rexlimiv ⊢ ∃ x ∈ V A x ∈ E ∧ x C ∈ E ∧ A ≠ x ∧ x ≠ C → A ∈ V ∧ C ∈ V ∧ A ≠ C → G ∈ FriendGraph → ∃ b ∈ V ∃ c ∈ V A b ∈ E ∧ b c ∈ E ∧ c A ∈ E
94 31 93 syl6 ⊢ A ∈ V ∧ C ∈ V ∧ A ≠ C → ∀ a ∈ V ∀ z ∈ V ∖ a ∃ x ∈ V a x ∈ E ∧ x z ∈ E ∧ a ≠ x ∧ x ≠ z → A ∈ V ∧ C ∈ V ∧ A ≠ C → G ∈ FriendGraph → ∃ b ∈ V ∃ c ∈ V A b ∈ E ∧ b c ∈ E ∧ c A ∈ E
95 94 pm2.43a ⊢ A ∈ V ∧ C ∈ V ∧ A ≠ C → ∀ a ∈ V ∀ z ∈ V ∖ a ∃ x ∈ V a x ∈ E ∧ x z ∈ E ∧ a ≠ x ∧ x ≠ z → G ∈ FriendGraph → ∃ b ∈ V ∃ c ∈ V A b ∈ E ∧ b c ∈ E ∧ c A ∈ E
96 95 ex ⊢ A ∈ V ∧ C ∈ V → A ≠ C → ∀ a ∈ V ∀ z ∈ V ∖ a ∃ x ∈ V a x ∈ E ∧ x z ∈ E ∧ a ≠ x ∧ x ≠ z → G ∈ FriendGraph → ∃ b ∈ V ∃ c ∈ V A b ∈ E ∧ b c ∈ E ∧ c A ∈ E
97 96 com4t ⊢ ∀ a ∈ V ∀ z ∈ V ∖ a ∃ x ∈ V a x ∈ E ∧ x z ∈ E ∧ a ≠ x ∧ x ≠ z → G ∈ FriendGraph → A ∈ V ∧ C ∈ V → A ≠ C → ∃ b ∈ V ∃ c ∈ V A b ∈ E ∧ b c ∈ E ∧ c A ∈ E
98 3 97 mpcom ⊢ G ∈ FriendGraph → A ∈ V ∧ C ∈ V → A ≠ C → ∃ b ∈ V ∃ c ∈ V A b ∈ E ∧ b c ∈ E ∧ c A ∈ E
99 98 3imp ⊢ G ∈ FriendGraph ∧ A ∈ V ∧ C ∈ V ∧ A ≠ C → ∃ b ∈ V ∃ c ∈ V A b ∈ E ∧ b c ∈ E ∧ c A ∈ E