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∈VAb∈E∧bc∈E∧cA∈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∈Vax∈E∧xz∈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→ax=Ax
14 13 eleq1d ⊢a=A→ax∈E↔Ax∈E
15 14 anbi1d ⊢a=A→ax∈E∧xz∈E↔Ax∈E∧xz∈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→ax∈E∧xz∈E∧a≠x∧x≠z↔Ax∈E∧xz∈E∧A≠x∧x≠z
19 18 rexbidv ⊢a=A→∃x∈Vax∈E∧xz∈E∧a≠x∧x≠z↔∃x∈VAx∈E∧xz∈E∧A≠x∧x≠z
20 12 19 raleqbidv ⊢a=A→∀z∈V∖a∃x∈Vax∈E∧xz∈E∧a≠x∧x≠z↔∀z∈V∖A∃x∈VAx∈E∧xz∈E∧A≠x∧x≠z
21 20 rspcv ⊢A∈V→∀a∈V∀z∈V∖a∃x∈Vax∈E∧xz∈E∧a≠x∧x≠z→∀z∈V∖A∃x∈VAx∈E∧xz∈E∧A≠x∧x≠z
22 21 ad2antrr ⊢A∈V∧C∈V∧A≠C→∀a∈V∀z∈V∖a∃x∈Vax∈E∧xz∈E∧a≠x∧x≠z→∀z∈V∖A∃x∈VAx∈E∧xz∈E∧A≠x∧x≠z
23 preq2 ⊢z=C→xz=xC
24 23 eleq1d ⊢z=C→xz∈E↔xC∈E
25 24 anbi2d ⊢z=C→Ax∈E∧xz∈E↔Ax∈E∧xC∈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→Ax∈E∧xz∈E∧A≠x∧x≠z↔Ax∈E∧xC∈E∧A≠x∧x≠C
29 28 rexbidv ⊢z=C→∃x∈VAx∈E∧xz∈E∧A≠x∧x≠z↔∃x∈VAx∈E∧xC∈E∧A≠x∧x≠C
30 29 rspcv ⊢C∈V∖A→∀z∈V∖A∃x∈VAx∈E∧xz∈E∧A≠x∧x≠z→∃x∈VAx∈E∧xC∈E∧A≠x∧x≠C
31 10 22 30 sylsyld ⊢A∈V∧C∈V∧A≠C→∀a∈V∀z∈V∖a∃x∈Vax∈E∧xz∈E∧a≠x∧x≠z→∃x∈VAx∈E∧xC∈E∧A≠x∧x≠C
32 1 2 2pthfrgrrn ⊢G∈FriendGraph→∀u∈V∀v∈V∖u∃y∈Vuy∈E∧yv∈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→uy=Ay
42 41 eleq1d ⊢u=A→uy∈E↔Ay∈E
43 42 anbi1d ⊢u=A→uy∈E∧yv∈E↔Ay∈E∧yv∈E
44 43 rexbidv ⊢u=A→∃y∈Vuy∈E∧yv∈E↔∃y∈VAy∈E∧yv∈E
45 40 44 raleqbidv ⊢u=A→∀v∈V∖u∃y∈Vuy∈E∧yv∈E↔∀v∈V∖A∃y∈VAy∈E∧yv∈E
46 45 rspcv ⊢A∈V→∀u∈V∀v∈V∖u∃y∈Vuy∈E∧yv∈E→∀v∈V∖A∃y∈VAy∈E∧yv∈E
47 46 adantl ⊢A≠x∧A∈V→∀u∈V∀v∈V∖u∃y∈Vuy∈E∧yv∈E→∀v∈V∖A∃y∈VAy∈E∧yv∈E
48 47 adantr ⊢A≠x∧A∈V∧x∈V→∀u∈V∀v∈V∖u∃y∈Vuy∈E∧yv∈E→∀v∈V∖A∃y∈VAy∈E∧yv∈E
49 preq2 ⊢v=x→yv=yx
50 49 eleq1d ⊢v=x→yv∈E↔yx∈E
51 50 anbi2d ⊢v=x→Ay∈E∧yv∈E↔Ay∈E∧yx∈E
52 51 rexbidv ⊢v=x→∃y∈VAy∈E∧yv∈E↔∃y∈VAy∈E∧yx∈E
53 52 rspcv ⊢x∈V∖A→∀v∈V∖A∃y∈VAy∈E∧yv∈E→∃y∈VAy∈E∧yx∈E
54 38 48 53 sylsyld ⊢A≠x∧A∈V∧x∈V→∀u∈V∀v∈V∖u∃y∈Vuy∈E∧yv∈E→∃y∈VAy∈E∧yx∈E
55 prcom ⊢Ay=yA
56 55 eleq1i ⊢Ay∈E↔yA∈E
57 prcom ⊢yx=xy
58 57 eleq1i ⊢yx∈E↔xy∈E
59 56 58 anbi12ci ⊢Ay∈E∧yx∈E↔xy∈E∧yA∈E
60 preq2 ⊢b=x→Ab=Ax
61 60 eleq1d ⊢b=x→Ab∈E↔Ax∈E
62 preq1 ⊢b=x→bc=xc
63 62 eleq1d ⊢b=x→bc∈E↔xc∈E
64 biidd ⊢b=x→cA∈E↔cA∈E
65 61 63 64 3anbi123d ⊢b=x→Ab∈E∧bc∈E∧cA∈E↔Ax∈E∧xc∈E∧cA∈E
66 biidd ⊢c=y→Ax∈E↔Ax∈E
67 preq2 ⊢c=y→xc=xy
68 67 eleq1d ⊢c=y→xc∈E↔xy∈E
69 preq1 ⊢c=y→cA=yA
70 69 eleq1d ⊢c=y→cA∈E↔yA∈E
71 66 68 70 3anbi123d ⊢c=y→Ax∈E∧xc∈E∧cA∈E↔Ax∈E∧xy∈E∧yA∈E
72 65 71 rspc2ev ⊢x∈V∧y∈V∧Ax∈E∧xy∈E∧yA∈E→∃b∈V∃c∈VAb∈E∧bc∈E∧cA∈E
73 72 3expa ⊢x∈V∧y∈V∧Ax∈E∧xy∈E∧yA∈E→∃b∈V∃c∈VAb∈E∧bc∈E∧cA∈E
74 73 expcom ⊢Ax∈E∧xy∈E∧yA∈E→x∈V∧y∈V→∃b∈V∃c∈VAb∈E∧bc∈E∧cA∈E
75 74 3expib ⊢Ax∈E→xy∈E∧yA∈E→x∈V∧y∈V→∃b∈V∃c∈VAb∈E∧bc∈E∧cA∈E
76 59 75 biimtrid ⊢Ax∈E→Ay∈E∧yx∈E→x∈V∧y∈V→∃b∈V∃c∈VAb∈E∧bc∈E∧cA∈E
77 76 adantr ⊢Ax∈E∧xC∈E→Ay∈E∧yx∈E→x∈V∧y∈V→∃b∈V∃c∈VAb∈E∧bc∈E∧cA∈E
78 77 com13 ⊢x∈V∧y∈V→Ay∈E∧yx∈E→Ax∈E∧xC∈E→∃b∈V∃c∈VAb∈E∧bc∈E∧cA∈E
79 78 rexlimdva ⊢x∈V→∃y∈VAy∈E∧yx∈E→Ax∈E∧xC∈E→∃b∈V∃c∈VAb∈E∧bc∈E∧cA∈E
80 79 com13 ⊢Ax∈E∧xC∈E→∃y∈VAy∈E∧yx∈E→x∈V→∃b∈V∃c∈VAb∈E∧bc∈E∧cA∈E
81 54 80 syl9 ⊢A≠x∧A∈V∧x∈V→Ax∈E∧xC∈E→∀u∈V∀v∈V∖u∃y∈Vuy∈E∧yv∈E→x∈V→∃b∈V∃c∈VAb∈E∧bc∈E∧cA∈E
82 81 exp31 ⊢A≠x→A∈V→x∈V→Ax∈E∧xC∈E→∀u∈V∀v∈V∖u∃y∈Vuy∈E∧yv∈E→x∈V→∃b∈V∃c∈VAb∈E∧bc∈E∧cA∈E
83 82 com24 ⊢A≠x→Ax∈E∧xC∈E→x∈V→A∈V→∀u∈V∀v∈V∖u∃y∈Vuy∈E∧yv∈E→x∈V→∃b∈V∃c∈VAb∈E∧bc∈E∧cA∈E
84 83 adantr ⊢A≠x∧x≠C→Ax∈E∧xC∈E→x∈V→A∈V→∀u∈V∀v∈V∖u∃y∈Vuy∈E∧yv∈E→x∈V→∃b∈V∃c∈VAb∈E∧bc∈E∧cA∈E
85 84 impcom ⊢Ax∈E∧xC∈E∧A≠x∧x≠C→x∈V→A∈V→∀u∈V∀v∈V∖u∃y∈Vuy∈E∧yv∈E→x∈V→∃b∈V∃c∈VAb∈E∧bc∈E∧cA∈E
86 85 com15 ⊢x∈V→x∈V→A∈V→∀u∈V∀v∈V∖u∃y∈Vuy∈E∧yv∈E→Ax∈E∧xC∈E∧A≠x∧x≠C→∃b∈V∃c∈VAb∈E∧bc∈E∧cA∈E
87 86 pm2.43i ⊢x∈V→A∈V→∀u∈V∀v∈V∖u∃y∈Vuy∈E∧yv∈E→Ax∈E∧xC∈E∧A≠x∧x≠C→∃b∈V∃c∈VAb∈E∧bc∈E∧cA∈E
88 87 com12 ⊢A∈V→x∈V→∀u∈V∀v∈V∖u∃y∈Vuy∈E∧yv∈E→Ax∈E∧xC∈E∧A≠x∧x≠C→∃b∈V∃c∈VAb∈E∧bc∈E∧cA∈E
89 88 ad2antrr ⊢A∈V∧C∈V∧A≠C→x∈V→∀u∈V∀v∈V∖u∃y∈Vuy∈E∧yv∈E→Ax∈E∧xC∈E∧A≠x∧x≠C→∃b∈V∃c∈VAb∈E∧bc∈E∧cA∈E
90 89 com4t ⊢∀u∈V∀v∈V∖u∃y∈Vuy∈E∧yv∈E→Ax∈E∧xC∈E∧A≠x∧x≠C→A∈V∧C∈V∧A≠C→x∈V→∃b∈V∃c∈VAb∈E∧bc∈E∧cA∈E
91 32 90 syl ⊢G∈FriendGraph→Ax∈E∧xC∈E∧A≠x∧x≠C→A∈V∧C∈V∧A≠C→x∈V→∃b∈V∃c∈VAb∈E∧bc∈E∧cA∈E
92 91 com14 ⊢x∈V→Ax∈E∧xC∈E∧A≠x∧x≠C→A∈V∧C∈V∧A≠C→G∈FriendGraph→∃b∈V∃c∈VAb∈E∧bc∈E∧cA∈E
93 92 rexlimiv ⊢∃x∈VAx∈E∧xC∈E∧A≠x∧x≠C→A∈V∧C∈V∧A≠C→G∈FriendGraph→∃b∈V∃c∈VAb∈E∧bc∈E∧cA∈E
94 31 93 syl6 ⊢A∈V∧C∈V∧A≠C→∀a∈V∀z∈V∖a∃x∈Vax∈E∧xz∈E∧a≠x∧x≠z→A∈V∧C∈V∧A≠C→G∈FriendGraph→∃b∈V∃c∈VAb∈E∧bc∈E∧cA∈E
95 94 pm2.43a ⊢A∈V∧C∈V∧A≠C→∀a∈V∀z∈V∖a∃x∈Vax∈E∧xz∈E∧a≠x∧x≠z→G∈FriendGraph→∃b∈V∃c∈VAb∈E∧bc∈E∧cA∈E
96 95 ex ⊢A∈V∧C∈V→A≠C→∀a∈V∀z∈V∖a∃x∈Vax∈E∧xz∈E∧a≠x∧x≠z→G∈FriendGraph→∃b∈V∃c∈VAb∈E∧bc∈E∧cA∈E
97 96 com4t ⊢∀a∈V∀z∈V∖a∃x∈Vax∈E∧xz∈E∧a≠x∧x≠z→G∈FriendGraph→A∈V∧C∈V→A≠C→∃b∈V∃c∈VAb∈E∧bc∈E∧cA∈E
98 3 97 mpcom ⊢G∈FriendGraph→A∈V∧C∈V→A≠C→∃b∈V∃c∈VAb∈E∧bc∈E∧cA∈E
99 98 3imp ⊢G∈FriendGraph∧A∈V∧C∈V∧A≠C→∃b∈V∃c∈VAb∈E∧bc∈E∧cA∈E