# 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}=\mathrm{Vtx}\left({G}\right)$
3cyclfrgrrn1.e ${⊢}{E}=\mathrm{Edg}\left({G}\right)$
Assertion 3cyclfrgrrn1 ${⊢}\left({G}\in \mathrm{FriendGraph}\wedge \left({A}\in {V}\wedge {C}\in {V}\right)\wedge {A}\ne {C}\right)\to \exists {b}\in {V}\phantom{\rule{.4em}{0ex}}\exists {c}\in {V}\phantom{\rule{.4em}{0ex}}\left(\left\{{A},{b}\right\}\in {E}\wedge \left\{{b},{c}\right\}\in {E}\wedge \left\{{c},{A}\right\}\in {E}\right)$

### Proof

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