# 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 ${⊢}\left({G}\in \mathrm{FriendGraph}\wedge {F}\mathrm{Cycles}\left({G}\right){P}\right)\to \left|{F}\right|\ne 4$

### Proof

Step Hyp Ref Expression
1 frgrusgr ${⊢}{G}\in \mathrm{FriendGraph}\to {G}\in \mathrm{USGraph}$
2 usgrupgr ${⊢}{G}\in \mathrm{USGraph}\to {G}\in \mathrm{UPGraph}$
3 1 2 syl ${⊢}{G}\in \mathrm{FriendGraph}\to {G}\in \mathrm{UPGraph}$
4 eqid ${⊢}\mathrm{Vtx}\left({G}\right)=\mathrm{Vtx}\left({G}\right)$
5 eqid ${⊢}\mathrm{Edg}\left({G}\right)=\mathrm{Edg}\left({G}\right)$
6 4 5 upgr4cycl4dv4e ${⊢}\left({G}\in \mathrm{UPGraph}\wedge {F}\mathrm{Cycles}\left({G}\right){P}\wedge \left|{F}\right|=4\right)\to \exists {a}\in \mathrm{Vtx}\left({G}\right)\phantom{\rule{.4em}{0ex}}\exists {b}\in \mathrm{Vtx}\left({G}\right)\phantom{\rule{.4em}{0ex}}\exists {c}\in \mathrm{Vtx}\left({G}\right)\phantom{\rule{.4em}{0ex}}\exists {d}\in \mathrm{Vtx}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left(\left(\left(\left\{{a},{b}\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{{b},{c}\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge \left(\left\{{c},{d}\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{{d},{a}\right\}\in \mathrm{Edg}\left({G}\right)\right)\right)\wedge \left(\left({a}\ne {b}\wedge {a}\ne {c}\wedge {a}\ne {d}\right)\wedge \left({b}\ne {c}\wedge {b}\ne {d}\wedge {c}\ne {d}\right)\right)\right)$
7 4 5 isfrgr ${⊢}{G}\in \mathrm{FriendGraph}↔\left({G}\in \mathrm{USGraph}\wedge \forall {k}\in \mathrm{Vtx}\left({G}\right)\phantom{\rule{.4em}{0ex}}\forall {l}\in \left(\mathrm{Vtx}\left({G}\right)\setminus \left\{{k}\right\}\right)\phantom{\rule{.4em}{0ex}}\exists !{x}\in \mathrm{Vtx}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left\{\left\{{x},{k}\right\},\left\{{x},{l}\right\}\right\}\subseteq \mathrm{Edg}\left({G}\right)\right)$
8 simplrl ${⊢}\left(\left(\left({a}\in \mathrm{Vtx}\left({G}\right)\wedge {b}\in \mathrm{Vtx}\left({G}\right)\right)\wedge \left({c}\in \mathrm{Vtx}\left({G}\right)\wedge {d}\in \mathrm{Vtx}\left({G}\right)\right)\right)\wedge \left(\left(\left(\left\{{a},{b}\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{{b},{c}\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge \left(\left\{{c},{d}\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{{d},{a}\right\}\in \mathrm{Edg}\left({G}\right)\right)\right)\wedge \left(\left({a}\ne {b}\wedge {a}\ne {c}\wedge {a}\ne {d}\right)\wedge \left({b}\ne {c}\wedge {b}\ne {d}\wedge {c}\ne {d}\right)\right)\right)\right)\to {c}\in \mathrm{Vtx}\left({G}\right)$
9 necom ${⊢}{a}\ne {c}↔{c}\ne {a}$
10 9 biimpi ${⊢}{a}\ne {c}\to {c}\ne {a}$
11 10 3ad2ant2 ${⊢}\left({a}\ne {b}\wedge {a}\ne {c}\wedge {a}\ne {d}\right)\to {c}\ne {a}$
12 11 ad2antrl ${⊢}\left(\left(\left(\left\{{a},{b}\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{{b},{c}\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge \left(\left\{{c},{d}\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{{d},{a}\right\}\in \mathrm{Edg}\left({G}\right)\right)\right)\wedge \left(\left({a}\ne {b}\wedge {a}\ne {c}\wedge {a}\ne {d}\right)\wedge \left({b}\ne {c}\wedge {b}\ne {d}\wedge {c}\ne {d}\right)\right)\right)\to {c}\ne {a}$
13 12 adantl ${⊢}\left(\left(\left({a}\in \mathrm{Vtx}\left({G}\right)\wedge {b}\in \mathrm{Vtx}\left({G}\right)\right)\wedge \left({c}\in \mathrm{Vtx}\left({G}\right)\wedge {d}\in \mathrm{Vtx}\left({G}\right)\right)\right)\wedge \left(\left(\left(\left\{{a},{b}\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{{b},{c}\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge \left(\left\{{c},{d}\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{{d},{a}\right\}\in \mathrm{Edg}\left({G}\right)\right)\right)\wedge \left(\left({a}\ne {b}\wedge {a}\ne {c}\wedge {a}\ne {d}\right)\wedge \left({b}\ne {c}\wedge {b}\ne {d}\wedge {c}\ne {d}\right)\right)\right)\right)\to {c}\ne {a}$
14 eldifsn ${⊢}{c}\in \left(\mathrm{Vtx}\left({G}\right)\setminus \left\{{a}\right\}\right)↔\left({c}\in \mathrm{Vtx}\left({G}\right)\wedge {c}\ne {a}\right)$
15 8 13 14 sylanbrc ${⊢}\left(\left(\left({a}\in \mathrm{Vtx}\left({G}\right)\wedge {b}\in \mathrm{Vtx}\left({G}\right)\right)\wedge \left({c}\in \mathrm{Vtx}\left({G}\right)\wedge {d}\in \mathrm{Vtx}\left({G}\right)\right)\right)\wedge \left(\left(\left(\left\{{a},{b}\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{{b},{c}\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge \left(\left\{{c},{d}\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{{d},{a}\right\}\in \mathrm{Edg}\left({G}\right)\right)\right)\wedge \left(\left({a}\ne {b}\wedge {a}\ne {c}\wedge {a}\ne {d}\right)\wedge \left({b}\ne {c}\wedge {b}\ne {d}\wedge {c}\ne {d}\right)\right)\right)\right)\to {c}\in \left(\mathrm{Vtx}\left({G}\right)\setminus \left\{{a}\right\}\right)$
16 sneq ${⊢}{k}={a}\to \left\{{k}\right\}=\left\{{a}\right\}$
17 16 difeq2d ${⊢}{k}={a}\to \mathrm{Vtx}\left({G}\right)\setminus \left\{{k}\right\}=\mathrm{Vtx}\left({G}\right)\setminus \left\{{a}\right\}$
18 preq2 ${⊢}{k}={a}\to \left\{{x},{k}\right\}=\left\{{x},{a}\right\}$
19 18 preq1d ${⊢}{k}={a}\to \left\{\left\{{x},{k}\right\},\left\{{x},{l}\right\}\right\}=\left\{\left\{{x},{a}\right\},\left\{{x},{l}\right\}\right\}$
20 19 sseq1d ${⊢}{k}={a}\to \left(\left\{\left\{{x},{k}\right\},\left\{{x},{l}\right\}\right\}\subseteq \mathrm{Edg}\left({G}\right)↔\left\{\left\{{x},{a}\right\},\left\{{x},{l}\right\}\right\}\subseteq \mathrm{Edg}\left({G}\right)\right)$
21 20 reubidv ${⊢}{k}={a}\to \left(\exists !{x}\in \mathrm{Vtx}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left\{\left\{{x},{k}\right\},\left\{{x},{l}\right\}\right\}\subseteq \mathrm{Edg}\left({G}\right)↔\exists !{x}\in \mathrm{Vtx}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left\{\left\{{x},{a}\right\},\left\{{x},{l}\right\}\right\}\subseteq \mathrm{Edg}\left({G}\right)\right)$
22 17 21 raleqbidv ${⊢}{k}={a}\to \left(\forall {l}\in \left(\mathrm{Vtx}\left({G}\right)\setminus \left\{{k}\right\}\right)\phantom{\rule{.4em}{0ex}}\exists !{x}\in \mathrm{Vtx}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left\{\left\{{x},{k}\right\},\left\{{x},{l}\right\}\right\}\subseteq \mathrm{Edg}\left({G}\right)↔\forall {l}\in \left(\mathrm{Vtx}\left({G}\right)\setminus \left\{{a}\right\}\right)\phantom{\rule{.4em}{0ex}}\exists !{x}\in \mathrm{Vtx}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left\{\left\{{x},{a}\right\},\left\{{x},{l}\right\}\right\}\subseteq \mathrm{Edg}\left({G}\right)\right)$
23 22 rspcv ${⊢}{a}\in \mathrm{Vtx}\left({G}\right)\to \left(\forall {k}\in \mathrm{Vtx}\left({G}\right)\phantom{\rule{.4em}{0ex}}\forall {l}\in \left(\mathrm{Vtx}\left({G}\right)\setminus \left\{{k}\right\}\right)\phantom{\rule{.4em}{0ex}}\exists !{x}\in \mathrm{Vtx}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left\{\left\{{x},{k}\right\},\left\{{x},{l}\right\}\right\}\subseteq \mathrm{Edg}\left({G}\right)\to \forall {l}\in \left(\mathrm{Vtx}\left({G}\right)\setminus \left\{{a}\right\}\right)\phantom{\rule{.4em}{0ex}}\exists !{x}\in \mathrm{Vtx}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left\{\left\{{x},{a}\right\},\left\{{x},{l}\right\}\right\}\subseteq \mathrm{Edg}\left({G}\right)\right)$
24 23 ad3antrrr ${⊢}\left(\left(\left({a}\in \mathrm{Vtx}\left({G}\right)\wedge {b}\in \mathrm{Vtx}\left({G}\right)\right)\wedge \left({c}\in \mathrm{Vtx}\left({G}\right)\wedge {d}\in \mathrm{Vtx}\left({G}\right)\right)\right)\wedge \left(\left(\left(\left\{{a},{b}\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{{b},{c}\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge \left(\left\{{c},{d}\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{{d},{a}\right\}\in \mathrm{Edg}\left({G}\right)\right)\right)\wedge \left(\left({a}\ne {b}\wedge {a}\ne {c}\wedge {a}\ne {d}\right)\wedge \left({b}\ne {c}\wedge {b}\ne {d}\wedge {c}\ne {d}\right)\right)\right)\right)\to \left(\forall {k}\in \mathrm{Vtx}\left({G}\right)\phantom{\rule{.4em}{0ex}}\forall {l}\in \left(\mathrm{Vtx}\left({G}\right)\setminus \left\{{k}\right\}\right)\phantom{\rule{.4em}{0ex}}\exists !{x}\in \mathrm{Vtx}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left\{\left\{{x},{k}\right\},\left\{{x},{l}\right\}\right\}\subseteq \mathrm{Edg}\left({G}\right)\to \forall {l}\in \left(\mathrm{Vtx}\left({G}\right)\setminus \left\{{a}\right\}\right)\phantom{\rule{.4em}{0ex}}\exists !{x}\in \mathrm{Vtx}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left\{\left\{{x},{a}\right\},\left\{{x},{l}\right\}\right\}\subseteq \mathrm{Edg}\left({G}\right)\right)$
25 preq2 ${⊢}{l}={c}\to \left\{{x},{l}\right\}=\left\{{x},{c}\right\}$
26 25 preq2d ${⊢}{l}={c}\to \left\{\left\{{x},{a}\right\},\left\{{x},{l}\right\}\right\}=\left\{\left\{{x},{a}\right\},\left\{{x},{c}\right\}\right\}$
27 26 sseq1d ${⊢}{l}={c}\to \left(\left\{\left\{{x},{a}\right\},\left\{{x},{l}\right\}\right\}\subseteq \mathrm{Edg}\left({G}\right)↔\left\{\left\{{x},{a}\right\},\left\{{x},{c}\right\}\right\}\subseteq \mathrm{Edg}\left({G}\right)\right)$
28 27 reubidv ${⊢}{l}={c}\to \left(\exists !{x}\in \mathrm{Vtx}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left\{\left\{{x},{a}\right\},\left\{{x},{l}\right\}\right\}\subseteq \mathrm{Edg}\left({G}\right)↔\exists !{x}\in \mathrm{Vtx}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left\{\left\{{x},{a}\right\},\left\{{x},{c}\right\}\right\}\subseteq \mathrm{Edg}\left({G}\right)\right)$
29 28 rspcv ${⊢}{c}\in \left(\mathrm{Vtx}\left({G}\right)\setminus \left\{{a}\right\}\right)\to \left(\forall {l}\in \left(\mathrm{Vtx}\left({G}\right)\setminus \left\{{a}\right\}\right)\phantom{\rule{.4em}{0ex}}\exists !{x}\in \mathrm{Vtx}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left\{\left\{{x},{a}\right\},\left\{{x},{l}\right\}\right\}\subseteq \mathrm{Edg}\left({G}\right)\to \exists !{x}\in \mathrm{Vtx}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left\{\left\{{x},{a}\right\},\left\{{x},{c}\right\}\right\}\subseteq \mathrm{Edg}\left({G}\right)\right)$
30 15 24 29 sylsyld ${⊢}\left(\left(\left({a}\in \mathrm{Vtx}\left({G}\right)\wedge {b}\in \mathrm{Vtx}\left({G}\right)\right)\wedge \left({c}\in \mathrm{Vtx}\left({G}\right)\wedge {d}\in \mathrm{Vtx}\left({G}\right)\right)\right)\wedge \left(\left(\left(\left\{{a},{b}\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{{b},{c}\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge \left(\left\{{c},{d}\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{{d},{a}\right\}\in \mathrm{Edg}\left({G}\right)\right)\right)\wedge \left(\left({a}\ne {b}\wedge {a}\ne {c}\wedge {a}\ne {d}\right)\wedge \left({b}\ne {c}\wedge {b}\ne {d}\wedge {c}\ne {d}\right)\right)\right)\right)\to \left(\forall {k}\in \mathrm{Vtx}\left({G}\right)\phantom{\rule{.4em}{0ex}}\forall {l}\in \left(\mathrm{Vtx}\left({G}\right)\setminus \left\{{k}\right\}\right)\phantom{\rule{.4em}{0ex}}\exists !{x}\in \mathrm{Vtx}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left\{\left\{{x},{k}\right\},\left\{{x},{l}\right\}\right\}\subseteq \mathrm{Edg}\left({G}\right)\to \exists !{x}\in \mathrm{Vtx}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left\{\left\{{x},{a}\right\},\left\{{x},{c}\right\}\right\}\subseteq \mathrm{Edg}\left({G}\right)\right)$
31 prcom ${⊢}\left\{{x},{a}\right\}=\left\{{a},{x}\right\}$
32 31 preq1i ${⊢}\left\{\left\{{x},{a}\right\},\left\{{x},{c}\right\}\right\}=\left\{\left\{{a},{x}\right\},\left\{{x},{c}\right\}\right\}$
33 32 sseq1i ${⊢}\left\{\left\{{x},{a}\right\},\left\{{x},{c}\right\}\right\}\subseteq \mathrm{Edg}\left({G}\right)↔\left\{\left\{{a},{x}\right\},\left\{{x},{c}\right\}\right\}\subseteq \mathrm{Edg}\left({G}\right)$
34 33 reubii ${⊢}\exists !{x}\in \mathrm{Vtx}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left\{\left\{{x},{a}\right\},\left\{{x},{c}\right\}\right\}\subseteq \mathrm{Edg}\left({G}\right)↔\exists !{x}\in \mathrm{Vtx}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left\{\left\{{a},{x}\right\},\left\{{x},{c}\right\}\right\}\subseteq \mathrm{Edg}\left({G}\right)$
35 simprll ${⊢}\left(\left(\left({a}\in \mathrm{Vtx}\left({G}\right)\wedge {b}\in \mathrm{Vtx}\left({G}\right)\right)\wedge \left({c}\in \mathrm{Vtx}\left({G}\right)\wedge {d}\in \mathrm{Vtx}\left({G}\right)\right)\right)\wedge \left(\left(\left(\left\{{a},{b}\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{{b},{c}\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge \left(\left\{{c},{d}\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{{d},{a}\right\}\in \mathrm{Edg}\left({G}\right)\right)\right)\wedge \left(\left({a}\ne {b}\wedge {a}\ne {c}\wedge {a}\ne {d}\right)\wedge \left({b}\ne {c}\wedge {b}\ne {d}\wedge {c}\ne {d}\right)\right)\right)\right)\to \left(\left\{{a},{b}\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{{b},{c}\right\}\in \mathrm{Edg}\left({G}\right)\right)$
36 simprlr ${⊢}\left(\left(\left({a}\in \mathrm{Vtx}\left({G}\right)\wedge {b}\in \mathrm{Vtx}\left({G}\right)\right)\wedge \left({c}\in \mathrm{Vtx}\left({G}\right)\wedge {d}\in \mathrm{Vtx}\left({G}\right)\right)\right)\wedge \left(\left(\left(\left\{{a},{b}\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{{b},{c}\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge \left(\left\{{c},{d}\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{{d},{a}\right\}\in \mathrm{Edg}\left({G}\right)\right)\right)\wedge \left(\left({a}\ne {b}\wedge {a}\ne {c}\wedge {a}\ne {d}\right)\wedge \left({b}\ne {c}\wedge {b}\ne {d}\wedge {c}\ne {d}\right)\right)\right)\right)\to \left(\left\{{c},{d}\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{{d},{a}\right\}\in \mathrm{Edg}\left({G}\right)\right)$
37 simpllr ${⊢}\left(\left(\left({a}\in \mathrm{Vtx}\left({G}\right)\wedge {b}\in \mathrm{Vtx}\left({G}\right)\right)\wedge \left({c}\in \mathrm{Vtx}\left({G}\right)\wedge {d}\in \mathrm{Vtx}\left({G}\right)\right)\right)\wedge \left(\left(\left(\left\{{a},{b}\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{{b},{c}\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge \left(\left\{{c},{d}\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{{d},{a}\right\}\in \mathrm{Edg}\left({G}\right)\right)\right)\wedge \left(\left({a}\ne {b}\wedge {a}\ne {c}\wedge {a}\ne {d}\right)\wedge \left({b}\ne {c}\wedge {b}\ne {d}\wedge {c}\ne {d}\right)\right)\right)\right)\to {b}\in \mathrm{Vtx}\left({G}\right)$
38 simplrr ${⊢}\left(\left(\left({a}\in \mathrm{Vtx}\left({G}\right)\wedge {b}\in \mathrm{Vtx}\left({G}\right)\right)\wedge \left({c}\in \mathrm{Vtx}\left({G}\right)\wedge {d}\in \mathrm{Vtx}\left({G}\right)\right)\right)\wedge \left(\left(\left(\left\{{a},{b}\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{{b},{c}\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge \left(\left\{{c},{d}\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{{d},{a}\right\}\in \mathrm{Edg}\left({G}\right)\right)\right)\wedge \left(\left({a}\ne {b}\wedge {a}\ne {c}\wedge {a}\ne {d}\right)\wedge \left({b}\ne {c}\wedge {b}\ne {d}\wedge {c}\ne {d}\right)\right)\right)\right)\to {d}\in \mathrm{Vtx}\left({G}\right)$
39 simprr2 ${⊢}\left(\left(\left(\left\{{a},{b}\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{{b},{c}\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge \left(\left\{{c},{d}\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{{d},{a}\right\}\in \mathrm{Edg}\left({G}\right)\right)\right)\wedge \left(\left({a}\ne {b}\wedge {a}\ne {c}\wedge {a}\ne {d}\right)\wedge \left({b}\ne {c}\wedge {b}\ne {d}\wedge {c}\ne {d}\right)\right)\right)\to {b}\ne {d}$
40 39 adantl ${⊢}\left(\left(\left({a}\in \mathrm{Vtx}\left({G}\right)\wedge {b}\in \mathrm{Vtx}\left({G}\right)\right)\wedge \left({c}\in \mathrm{Vtx}\left({G}\right)\wedge {d}\in \mathrm{Vtx}\left({G}\right)\right)\right)\wedge \left(\left(\left(\left\{{a},{b}\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{{b},{c}\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge \left(\left\{{c},{d}\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{{d},{a}\right\}\in \mathrm{Edg}\left({G}\right)\right)\right)\wedge \left(\left({a}\ne {b}\wedge {a}\ne {c}\wedge {a}\ne {d}\right)\wedge \left({b}\ne {c}\wedge {b}\ne {d}\wedge {c}\ne {d}\right)\right)\right)\right)\to {b}\ne {d}$
41 4cycl2vnunb ${⊢}\left(\left(\left\{{a},{b}\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{{b},{c}\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge \left(\left\{{c},{d}\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{{d},{a}\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge \left({b}\in \mathrm{Vtx}\left({G}\right)\wedge {d}\in \mathrm{Vtx}\left({G}\right)\wedge {b}\ne {d}\right)\right)\to ¬\exists !{x}\in \mathrm{Vtx}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left\{\left\{{a},{x}\right\},\left\{{x},{c}\right\}\right\}\subseteq \mathrm{Edg}\left({G}\right)$
42 35 36 37 38 40 41 syl113anc ${⊢}\left(\left(\left({a}\in \mathrm{Vtx}\left({G}\right)\wedge {b}\in \mathrm{Vtx}\left({G}\right)\right)\wedge \left({c}\in \mathrm{Vtx}\left({G}\right)\wedge {d}\in \mathrm{Vtx}\left({G}\right)\right)\right)\wedge \left(\left(\left(\left\{{a},{b}\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{{b},{c}\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge \left(\left\{{c},{d}\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{{d},{a}\right\}\in \mathrm{Edg}\left({G}\right)\right)\right)\wedge \left(\left({a}\ne {b}\wedge {a}\ne {c}\wedge {a}\ne {d}\right)\wedge \left({b}\ne {c}\wedge {b}\ne {d}\wedge {c}\ne {d}\right)\right)\right)\right)\to ¬\exists !{x}\in \mathrm{Vtx}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left\{\left\{{a},{x}\right\},\left\{{x},{c}\right\}\right\}\subseteq \mathrm{Edg}\left({G}\right)$
43 42 pm2.21d ${⊢}\left(\left(\left({a}\in \mathrm{Vtx}\left({G}\right)\wedge {b}\in \mathrm{Vtx}\left({G}\right)\right)\wedge \left({c}\in \mathrm{Vtx}\left({G}\right)\wedge {d}\in \mathrm{Vtx}\left({G}\right)\right)\right)\wedge \left(\left(\left(\left\{{a},{b}\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{{b},{c}\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge \left(\left\{{c},{d}\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{{d},{a}\right\}\in \mathrm{Edg}\left({G}\right)\right)\right)\wedge \left(\left({a}\ne {b}\wedge {a}\ne {c}\wedge {a}\ne {d}\right)\wedge \left({b}\ne {c}\wedge {b}\ne {d}\wedge {c}\ne {d}\right)\right)\right)\right)\to \left(\exists !{x}\in \mathrm{Vtx}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left\{\left\{{a},{x}\right\},\left\{{x},{c}\right\}\right\}\subseteq \mathrm{Edg}\left({G}\right)\to \left|{F}\right|\ne 4\right)$
44 43 com12 ${⊢}\exists !{x}\in \mathrm{Vtx}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left\{\left\{{a},{x}\right\},\left\{{x},{c}\right\}\right\}\subseteq \mathrm{Edg}\left({G}\right)\to \left(\left(\left(\left({a}\in \mathrm{Vtx}\left({G}\right)\wedge {b}\in \mathrm{Vtx}\left({G}\right)\right)\wedge \left({c}\in \mathrm{Vtx}\left({G}\right)\wedge {d}\in \mathrm{Vtx}\left({G}\right)\right)\right)\wedge \left(\left(\left(\left\{{a},{b}\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{{b},{c}\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge \left(\left\{{c},{d}\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{{d},{a}\right\}\in \mathrm{Edg}\left({G}\right)\right)\right)\wedge \left(\left({a}\ne {b}\wedge {a}\ne {c}\wedge {a}\ne {d}\right)\wedge \left({b}\ne {c}\wedge {b}\ne {d}\wedge {c}\ne {d}\right)\right)\right)\right)\to \left|{F}\right|\ne 4\right)$
45 34 44 sylbi ${⊢}\exists !{x}\in \mathrm{Vtx}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left\{\left\{{x},{a}\right\},\left\{{x},{c}\right\}\right\}\subseteq \mathrm{Edg}\left({G}\right)\to \left(\left(\left(\left({a}\in \mathrm{Vtx}\left({G}\right)\wedge {b}\in \mathrm{Vtx}\left({G}\right)\right)\wedge \left({c}\in \mathrm{Vtx}\left({G}\right)\wedge {d}\in \mathrm{Vtx}\left({G}\right)\right)\right)\wedge \left(\left(\left(\left\{{a},{b}\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{{b},{c}\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge \left(\left\{{c},{d}\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{{d},{a}\right\}\in \mathrm{Edg}\left({G}\right)\right)\right)\wedge \left(\left({a}\ne {b}\wedge {a}\ne {c}\wedge {a}\ne {d}\right)\wedge \left({b}\ne {c}\wedge {b}\ne {d}\wedge {c}\ne {d}\right)\right)\right)\right)\to \left|{F}\right|\ne 4\right)$
46 30 45 syl6 ${⊢}\left(\left(\left({a}\in \mathrm{Vtx}\left({G}\right)\wedge {b}\in \mathrm{Vtx}\left({G}\right)\right)\wedge \left({c}\in \mathrm{Vtx}\left({G}\right)\wedge {d}\in \mathrm{Vtx}\left({G}\right)\right)\right)\wedge \left(\left(\left(\left\{{a},{b}\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{{b},{c}\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge \left(\left\{{c},{d}\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{{d},{a}\right\}\in \mathrm{Edg}\left({G}\right)\right)\right)\wedge \left(\left({a}\ne {b}\wedge {a}\ne {c}\wedge {a}\ne {d}\right)\wedge \left({b}\ne {c}\wedge {b}\ne {d}\wedge {c}\ne {d}\right)\right)\right)\right)\to \left(\forall {k}\in \mathrm{Vtx}\left({G}\right)\phantom{\rule{.4em}{0ex}}\forall {l}\in \left(\mathrm{Vtx}\left({G}\right)\setminus \left\{{k}\right\}\right)\phantom{\rule{.4em}{0ex}}\exists !{x}\in \mathrm{Vtx}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left\{\left\{{x},{k}\right\},\left\{{x},{l}\right\}\right\}\subseteq \mathrm{Edg}\left({G}\right)\to \left(\left(\left(\left({a}\in \mathrm{Vtx}\left({G}\right)\wedge {b}\in \mathrm{Vtx}\left({G}\right)\right)\wedge \left({c}\in \mathrm{Vtx}\left({G}\right)\wedge {d}\in \mathrm{Vtx}\left({G}\right)\right)\right)\wedge \left(\left(\left(\left\{{a},{b}\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{{b},{c}\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge \left(\left\{{c},{d}\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{{d},{a}\right\}\in \mathrm{Edg}\left({G}\right)\right)\right)\wedge \left(\left({a}\ne {b}\wedge {a}\ne {c}\wedge {a}\ne {d}\right)\wedge \left({b}\ne {c}\wedge {b}\ne {d}\wedge {c}\ne {d}\right)\right)\right)\right)\to \left|{F}\right|\ne 4\right)\right)$
47 46 pm2.43b ${⊢}\forall {k}\in \mathrm{Vtx}\left({G}\right)\phantom{\rule{.4em}{0ex}}\forall {l}\in \left(\mathrm{Vtx}\left({G}\right)\setminus \left\{{k}\right\}\right)\phantom{\rule{.4em}{0ex}}\exists !{x}\in \mathrm{Vtx}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left\{\left\{{x},{k}\right\},\left\{{x},{l}\right\}\right\}\subseteq \mathrm{Edg}\left({G}\right)\to \left(\left(\left(\left({a}\in \mathrm{Vtx}\left({G}\right)\wedge {b}\in \mathrm{Vtx}\left({G}\right)\right)\wedge \left({c}\in \mathrm{Vtx}\left({G}\right)\wedge {d}\in \mathrm{Vtx}\left({G}\right)\right)\right)\wedge \left(\left(\left(\left\{{a},{b}\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{{b},{c}\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge \left(\left\{{c},{d}\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{{d},{a}\right\}\in \mathrm{Edg}\left({G}\right)\right)\right)\wedge \left(\left({a}\ne {b}\wedge {a}\ne {c}\wedge {a}\ne {d}\right)\wedge \left({b}\ne {c}\wedge {b}\ne {d}\wedge {c}\ne {d}\right)\right)\right)\right)\to \left|{F}\right|\ne 4\right)$
48 47 adantl ${⊢}\left({G}\in \mathrm{USGraph}\wedge \forall {k}\in \mathrm{Vtx}\left({G}\right)\phantom{\rule{.4em}{0ex}}\forall {l}\in \left(\mathrm{Vtx}\left({G}\right)\setminus \left\{{k}\right\}\right)\phantom{\rule{.4em}{0ex}}\exists !{x}\in \mathrm{Vtx}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left\{\left\{{x},{k}\right\},\left\{{x},{l}\right\}\right\}\subseteq \mathrm{Edg}\left({G}\right)\right)\to \left(\left(\left(\left({a}\in \mathrm{Vtx}\left({G}\right)\wedge {b}\in \mathrm{Vtx}\left({G}\right)\right)\wedge \left({c}\in \mathrm{Vtx}\left({G}\right)\wedge {d}\in \mathrm{Vtx}\left({G}\right)\right)\right)\wedge \left(\left(\left(\left\{{a},{b}\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{{b},{c}\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge \left(\left\{{c},{d}\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{{d},{a}\right\}\in \mathrm{Edg}\left({G}\right)\right)\right)\wedge \left(\left({a}\ne {b}\wedge {a}\ne {c}\wedge {a}\ne {d}\right)\wedge \left({b}\ne {c}\wedge {b}\ne {d}\wedge {c}\ne {d}\right)\right)\right)\right)\to \left|{F}\right|\ne 4\right)$
49 7 48 sylbi ${⊢}{G}\in \mathrm{FriendGraph}\to \left(\left(\left(\left({a}\in \mathrm{Vtx}\left({G}\right)\wedge {b}\in \mathrm{Vtx}\left({G}\right)\right)\wedge \left({c}\in \mathrm{Vtx}\left({G}\right)\wedge {d}\in \mathrm{Vtx}\left({G}\right)\right)\right)\wedge \left(\left(\left(\left\{{a},{b}\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{{b},{c}\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge \left(\left\{{c},{d}\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{{d},{a}\right\}\in \mathrm{Edg}\left({G}\right)\right)\right)\wedge \left(\left({a}\ne {b}\wedge {a}\ne {c}\wedge {a}\ne {d}\right)\wedge \left({b}\ne {c}\wedge {b}\ne {d}\wedge {c}\ne {d}\right)\right)\right)\right)\to \left|{F}\right|\ne 4\right)$
50 49 expdcom ${⊢}\left(\left({a}\in \mathrm{Vtx}\left({G}\right)\wedge {b}\in \mathrm{Vtx}\left({G}\right)\right)\wedge \left({c}\in \mathrm{Vtx}\left({G}\right)\wedge {d}\in \mathrm{Vtx}\left({G}\right)\right)\right)\to \left(\left(\left(\left(\left\{{a},{b}\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{{b},{c}\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge \left(\left\{{c},{d}\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{{d},{a}\right\}\in \mathrm{Edg}\left({G}\right)\right)\right)\wedge \left(\left({a}\ne {b}\wedge {a}\ne {c}\wedge {a}\ne {d}\right)\wedge \left({b}\ne {c}\wedge {b}\ne {d}\wedge {c}\ne {d}\right)\right)\right)\to \left({G}\in \mathrm{FriendGraph}\to \left|{F}\right|\ne 4\right)\right)$
51 50 rexlimdvva ${⊢}\left({a}\in \mathrm{Vtx}\left({G}\right)\wedge {b}\in \mathrm{Vtx}\left({G}\right)\right)\to \left(\exists {c}\in \mathrm{Vtx}\left({G}\right)\phantom{\rule{.4em}{0ex}}\exists {d}\in \mathrm{Vtx}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left(\left(\left(\left\{{a},{b}\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{{b},{c}\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge \left(\left\{{c},{d}\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{{d},{a}\right\}\in \mathrm{Edg}\left({G}\right)\right)\right)\wedge \left(\left({a}\ne {b}\wedge {a}\ne {c}\wedge {a}\ne {d}\right)\wedge \left({b}\ne {c}\wedge {b}\ne {d}\wedge {c}\ne {d}\right)\right)\right)\to \left({G}\in \mathrm{FriendGraph}\to \left|{F}\right|\ne 4\right)\right)$
52 51 rexlimivv ${⊢}\exists {a}\in \mathrm{Vtx}\left({G}\right)\phantom{\rule{.4em}{0ex}}\exists {b}\in \mathrm{Vtx}\left({G}\right)\phantom{\rule{.4em}{0ex}}\exists {c}\in \mathrm{Vtx}\left({G}\right)\phantom{\rule{.4em}{0ex}}\exists {d}\in \mathrm{Vtx}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left(\left(\left(\left\{{a},{b}\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{{b},{c}\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge \left(\left\{{c},{d}\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{{d},{a}\right\}\in \mathrm{Edg}\left({G}\right)\right)\right)\wedge \left(\left({a}\ne {b}\wedge {a}\ne {c}\wedge {a}\ne {d}\right)\wedge \left({b}\ne {c}\wedge {b}\ne {d}\wedge {c}\ne {d}\right)\right)\right)\to \left({G}\in \mathrm{FriendGraph}\to \left|{F}\right|\ne 4\right)$
53 6 52 syl ${⊢}\left({G}\in \mathrm{UPGraph}\wedge {F}\mathrm{Cycles}\left({G}\right){P}\wedge \left|{F}\right|=4\right)\to \left({G}\in \mathrm{FriendGraph}\to \left|{F}\right|\ne 4\right)$
54 53 3exp ${⊢}{G}\in \mathrm{UPGraph}\to \left({F}\mathrm{Cycles}\left({G}\right){P}\to \left(\left|{F}\right|=4\to \left({G}\in \mathrm{FriendGraph}\to \left|{F}\right|\ne 4\right)\right)\right)$
55 54 com34 ${⊢}{G}\in \mathrm{UPGraph}\to \left({F}\mathrm{Cycles}\left({G}\right){P}\to \left({G}\in \mathrm{FriendGraph}\to \left(\left|{F}\right|=4\to \left|{F}\right|\ne 4\right)\right)\right)$
56 55 com23 ${⊢}{G}\in \mathrm{UPGraph}\to \left({G}\in \mathrm{FriendGraph}\to \left({F}\mathrm{Cycles}\left({G}\right){P}\to \left(\left|{F}\right|=4\to \left|{F}\right|\ne 4\right)\right)\right)$
57 3 56 mpcom ${⊢}{G}\in \mathrm{FriendGraph}\to \left({F}\mathrm{Cycles}\left({G}\right){P}\to \left(\left|{F}\right|=4\to \left|{F}\right|\ne 4\right)\right)$
58 57 imp ${⊢}\left({G}\in \mathrm{FriendGraph}\wedge {F}\mathrm{Cycles}\left({G}\right){P}\right)\to \left(\left|{F}\right|=4\to \left|{F}\right|\ne 4\right)$
59 neqne ${⊢}¬\left|{F}\right|=4\to \left|{F}\right|\ne 4$
60 58 59 pm2.61d1 ${⊢}\left({G}\in \mathrm{FriendGraph}\wedge {F}\mathrm{Cycles}\left({G}\right){P}\right)\to \left|{F}\right|\ne 4$