# Metamath Proof Explorer

## Theorem 4cycl2vnunb

Description: In a 4-cycle, two distinct vertices have not a unique common neighbor. (Contributed by Alexander van der Vekens, 19-Nov-2017) (Revised by AV, 2-Apr-2021)

Ref Expression
Assertion 4cycl2vnunb ${⊢}\left(\left(\left\{{A},{B}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\right)\wedge \left(\left\{{C},{D}\right\}\in {E}\wedge \left\{{D},{A}\right\}\in {E}\right)\wedge \left({B}\in {V}\wedge {D}\in {V}\wedge {B}\ne {D}\right)\right)\to ¬\exists !{x}\in {V}\phantom{\rule{.4em}{0ex}}\left\{\left\{{A},{x}\right\},\left\{{x},{C}\right\}\right\}\subseteq {E}$

### Proof

Step Hyp Ref Expression
1 4cycl2v2nb ${⊢}\left(\left(\left\{{A},{B}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\right)\wedge \left(\left\{{C},{D}\right\}\in {E}\wedge \left\{{D},{A}\right\}\in {E}\right)\right)\to \left(\left\{\left\{{A},{B}\right\},\left\{{B},{C}\right\}\right\}\subseteq {E}\wedge \left\{\left\{{A},{D}\right\},\left\{{D},{C}\right\}\right\}\subseteq {E}\right)$
2 preq2 ${⊢}{x}={B}\to \left\{{A},{x}\right\}=\left\{{A},{B}\right\}$
3 preq1 ${⊢}{x}={B}\to \left\{{x},{C}\right\}=\left\{{B},{C}\right\}$
4 2 3 preq12d ${⊢}{x}={B}\to \left\{\left\{{A},{x}\right\},\left\{{x},{C}\right\}\right\}=\left\{\left\{{A},{B}\right\},\left\{{B},{C}\right\}\right\}$
5 4 sseq1d ${⊢}{x}={B}\to \left(\left\{\left\{{A},{x}\right\},\left\{{x},{C}\right\}\right\}\subseteq {E}↔\left\{\left\{{A},{B}\right\},\left\{{B},{C}\right\}\right\}\subseteq {E}\right)$
6 5 anbi1d ${⊢}{x}={B}\to \left(\left(\left\{\left\{{A},{x}\right\},\left\{{x},{C}\right\}\right\}\subseteq {E}\wedge \left\{\left\{{A},{y}\right\},\left\{{y},{C}\right\}\right\}\subseteq {E}\right)↔\left(\left\{\left\{{A},{B}\right\},\left\{{B},{C}\right\}\right\}\subseteq {E}\wedge \left\{\left\{{A},{y}\right\},\left\{{y},{C}\right\}\right\}\subseteq {E}\right)\right)$
7 neeq1 ${⊢}{x}={B}\to \left({x}\ne {y}↔{B}\ne {y}\right)$
8 6 7 anbi12d ${⊢}{x}={B}\to \left(\left(\left(\left\{\left\{{A},{x}\right\},\left\{{x},{C}\right\}\right\}\subseteq {E}\wedge \left\{\left\{{A},{y}\right\},\left\{{y},{C}\right\}\right\}\subseteq {E}\right)\wedge {x}\ne {y}\right)↔\left(\left(\left\{\left\{{A},{B}\right\},\left\{{B},{C}\right\}\right\}\subseteq {E}\wedge \left\{\left\{{A},{y}\right\},\left\{{y},{C}\right\}\right\}\subseteq {E}\right)\wedge {B}\ne {y}\right)\right)$
9 preq2 ${⊢}{y}={D}\to \left\{{A},{y}\right\}=\left\{{A},{D}\right\}$
10 preq1 ${⊢}{y}={D}\to \left\{{y},{C}\right\}=\left\{{D},{C}\right\}$
11 9 10 preq12d ${⊢}{y}={D}\to \left\{\left\{{A},{y}\right\},\left\{{y},{C}\right\}\right\}=\left\{\left\{{A},{D}\right\},\left\{{D},{C}\right\}\right\}$
12 11 sseq1d ${⊢}{y}={D}\to \left(\left\{\left\{{A},{y}\right\},\left\{{y},{C}\right\}\right\}\subseteq {E}↔\left\{\left\{{A},{D}\right\},\left\{{D},{C}\right\}\right\}\subseteq {E}\right)$
13 12 anbi2d ${⊢}{y}={D}\to \left(\left(\left\{\left\{{A},{B}\right\},\left\{{B},{C}\right\}\right\}\subseteq {E}\wedge \left\{\left\{{A},{y}\right\},\left\{{y},{C}\right\}\right\}\subseteq {E}\right)↔\left(\left\{\left\{{A},{B}\right\},\left\{{B},{C}\right\}\right\}\subseteq {E}\wedge \left\{\left\{{A},{D}\right\},\left\{{D},{C}\right\}\right\}\subseteq {E}\right)\right)$
14 neeq2 ${⊢}{y}={D}\to \left({B}\ne {y}↔{B}\ne {D}\right)$
15 13 14 anbi12d ${⊢}{y}={D}\to \left(\left(\left(\left\{\left\{{A},{B}\right\},\left\{{B},{C}\right\}\right\}\subseteq {E}\wedge \left\{\left\{{A},{y}\right\},\left\{{y},{C}\right\}\right\}\subseteq {E}\right)\wedge {B}\ne {y}\right)↔\left(\left(\left\{\left\{{A},{B}\right\},\left\{{B},{C}\right\}\right\}\subseteq {E}\wedge \left\{\left\{{A},{D}\right\},\left\{{D},{C}\right\}\right\}\subseteq {E}\right)\wedge {B}\ne {D}\right)\right)$
16 8 15 rspc2ev ${⊢}\left({B}\in {V}\wedge {D}\in {V}\wedge \left(\left(\left\{\left\{{A},{B}\right\},\left\{{B},{C}\right\}\right\}\subseteq {E}\wedge \left\{\left\{{A},{D}\right\},\left\{{D},{C}\right\}\right\}\subseteq {E}\right)\wedge {B}\ne {D}\right)\right)\to \exists {x}\in {V}\phantom{\rule{.4em}{0ex}}\exists {y}\in {V}\phantom{\rule{.4em}{0ex}}\left(\left(\left\{\left\{{A},{x}\right\},\left\{{x},{C}\right\}\right\}\subseteq {E}\wedge \left\{\left\{{A},{y}\right\},\left\{{y},{C}\right\}\right\}\subseteq {E}\right)\wedge {x}\ne {y}\right)$
17 16 3expa ${⊢}\left(\left({B}\in {V}\wedge {D}\in {V}\right)\wedge \left(\left(\left\{\left\{{A},{B}\right\},\left\{{B},{C}\right\}\right\}\subseteq {E}\wedge \left\{\left\{{A},{D}\right\},\left\{{D},{C}\right\}\right\}\subseteq {E}\right)\wedge {B}\ne {D}\right)\right)\to \exists {x}\in {V}\phantom{\rule{.4em}{0ex}}\exists {y}\in {V}\phantom{\rule{.4em}{0ex}}\left(\left(\left\{\left\{{A},{x}\right\},\left\{{x},{C}\right\}\right\}\subseteq {E}\wedge \left\{\left\{{A},{y}\right\},\left\{{y},{C}\right\}\right\}\subseteq {E}\right)\wedge {x}\ne {y}\right)$
18 17 expcom ${⊢}\left(\left(\left\{\left\{{A},{B}\right\},\left\{{B},{C}\right\}\right\}\subseteq {E}\wedge \left\{\left\{{A},{D}\right\},\left\{{D},{C}\right\}\right\}\subseteq {E}\right)\wedge {B}\ne {D}\right)\to \left(\left({B}\in {V}\wedge {D}\in {V}\right)\to \exists {x}\in {V}\phantom{\rule{.4em}{0ex}}\exists {y}\in {V}\phantom{\rule{.4em}{0ex}}\left(\left(\left\{\left\{{A},{x}\right\},\left\{{x},{C}\right\}\right\}\subseteq {E}\wedge \left\{\left\{{A},{y}\right\},\left\{{y},{C}\right\}\right\}\subseteq {E}\right)\wedge {x}\ne {y}\right)\right)$
19 18 ex ${⊢}\left(\left\{\left\{{A},{B}\right\},\left\{{B},{C}\right\}\right\}\subseteq {E}\wedge \left\{\left\{{A},{D}\right\},\left\{{D},{C}\right\}\right\}\subseteq {E}\right)\to \left({B}\ne {D}\to \left(\left({B}\in {V}\wedge {D}\in {V}\right)\to \exists {x}\in {V}\phantom{\rule{.4em}{0ex}}\exists {y}\in {V}\phantom{\rule{.4em}{0ex}}\left(\left(\left\{\left\{{A},{x}\right\},\left\{{x},{C}\right\}\right\}\subseteq {E}\wedge \left\{\left\{{A},{y}\right\},\left\{{y},{C}\right\}\right\}\subseteq {E}\right)\wedge {x}\ne {y}\right)\right)\right)$
20 19 com13 ${⊢}\left({B}\in {V}\wedge {D}\in {V}\right)\to \left({B}\ne {D}\to \left(\left(\left\{\left\{{A},{B}\right\},\left\{{B},{C}\right\}\right\}\subseteq {E}\wedge \left\{\left\{{A},{D}\right\},\left\{{D},{C}\right\}\right\}\subseteq {E}\right)\to \exists {x}\in {V}\phantom{\rule{.4em}{0ex}}\exists {y}\in {V}\phantom{\rule{.4em}{0ex}}\left(\left(\left\{\left\{{A},{x}\right\},\left\{{x},{C}\right\}\right\}\subseteq {E}\wedge \left\{\left\{{A},{y}\right\},\left\{{y},{C}\right\}\right\}\subseteq {E}\right)\wedge {x}\ne {y}\right)\right)\right)$
21 20 3impia ${⊢}\left({B}\in {V}\wedge {D}\in {V}\wedge {B}\ne {D}\right)\to \left(\left(\left\{\left\{{A},{B}\right\},\left\{{B},{C}\right\}\right\}\subseteq {E}\wedge \left\{\left\{{A},{D}\right\},\left\{{D},{C}\right\}\right\}\subseteq {E}\right)\to \exists {x}\in {V}\phantom{\rule{.4em}{0ex}}\exists {y}\in {V}\phantom{\rule{.4em}{0ex}}\left(\left(\left\{\left\{{A},{x}\right\},\left\{{x},{C}\right\}\right\}\subseteq {E}\wedge \left\{\left\{{A},{y}\right\},\left\{{y},{C}\right\}\right\}\subseteq {E}\right)\wedge {x}\ne {y}\right)\right)$
22 21 impcom ${⊢}\left(\left(\left\{\left\{{A},{B}\right\},\left\{{B},{C}\right\}\right\}\subseteq {E}\wedge \left\{\left\{{A},{D}\right\},\left\{{D},{C}\right\}\right\}\subseteq {E}\right)\wedge \left({B}\in {V}\wedge {D}\in {V}\wedge {B}\ne {D}\right)\right)\to \exists {x}\in {V}\phantom{\rule{.4em}{0ex}}\exists {y}\in {V}\phantom{\rule{.4em}{0ex}}\left(\left(\left\{\left\{{A},{x}\right\},\left\{{x},{C}\right\}\right\}\subseteq {E}\wedge \left\{\left\{{A},{y}\right\},\left\{{y},{C}\right\}\right\}\subseteq {E}\right)\wedge {x}\ne {y}\right)$
23 rexnal ${⊢}\exists {x}\in {V}\phantom{\rule{.4em}{0ex}}¬\forall {y}\in {V}\phantom{\rule{.4em}{0ex}}\left(\left(\left\{\left\{{A},{x}\right\},\left\{{x},{C}\right\}\right\}\subseteq {E}\wedge \left\{\left\{{A},{y}\right\},\left\{{y},{C}\right\}\right\}\subseteq {E}\right)\to {x}={y}\right)↔¬\forall {x}\in {V}\phantom{\rule{.4em}{0ex}}\forall {y}\in {V}\phantom{\rule{.4em}{0ex}}\left(\left(\left\{\left\{{A},{x}\right\},\left\{{x},{C}\right\}\right\}\subseteq {E}\wedge \left\{\left\{{A},{y}\right\},\left\{{y},{C}\right\}\right\}\subseteq {E}\right)\to {x}={y}\right)$
24 rexnal ${⊢}\exists {y}\in {V}\phantom{\rule{.4em}{0ex}}¬\left(\left(\left\{\left\{{A},{x}\right\},\left\{{x},{C}\right\}\right\}\subseteq {E}\wedge \left\{\left\{{A},{y}\right\},\left\{{y},{C}\right\}\right\}\subseteq {E}\right)\to {x}={y}\right)↔¬\forall {y}\in {V}\phantom{\rule{.4em}{0ex}}\left(\left(\left\{\left\{{A},{x}\right\},\left\{{x},{C}\right\}\right\}\subseteq {E}\wedge \left\{\left\{{A},{y}\right\},\left\{{y},{C}\right\}\right\}\subseteq {E}\right)\to {x}={y}\right)$
25 annim ${⊢}\left(\left(\left\{\left\{{A},{x}\right\},\left\{{x},{C}\right\}\right\}\subseteq {E}\wedge \left\{\left\{{A},{y}\right\},\left\{{y},{C}\right\}\right\}\subseteq {E}\right)\wedge ¬{x}={y}\right)↔¬\left(\left(\left\{\left\{{A},{x}\right\},\left\{{x},{C}\right\}\right\}\subseteq {E}\wedge \left\{\left\{{A},{y}\right\},\left\{{y},{C}\right\}\right\}\subseteq {E}\right)\to {x}={y}\right)$
26 df-ne ${⊢}{x}\ne {y}↔¬{x}={y}$
27 26 bicomi ${⊢}¬{x}={y}↔{x}\ne {y}$
28 27 anbi2i ${⊢}\left(\left(\left\{\left\{{A},{x}\right\},\left\{{x},{C}\right\}\right\}\subseteq {E}\wedge \left\{\left\{{A},{y}\right\},\left\{{y},{C}\right\}\right\}\subseteq {E}\right)\wedge ¬{x}={y}\right)↔\left(\left(\left\{\left\{{A},{x}\right\},\left\{{x},{C}\right\}\right\}\subseteq {E}\wedge \left\{\left\{{A},{y}\right\},\left\{{y},{C}\right\}\right\}\subseteq {E}\right)\wedge {x}\ne {y}\right)$
29 25 28 bitr3i ${⊢}¬\left(\left(\left\{\left\{{A},{x}\right\},\left\{{x},{C}\right\}\right\}\subseteq {E}\wedge \left\{\left\{{A},{y}\right\},\left\{{y},{C}\right\}\right\}\subseteq {E}\right)\to {x}={y}\right)↔\left(\left(\left\{\left\{{A},{x}\right\},\left\{{x},{C}\right\}\right\}\subseteq {E}\wedge \left\{\left\{{A},{y}\right\},\left\{{y},{C}\right\}\right\}\subseteq {E}\right)\wedge {x}\ne {y}\right)$
30 29 rexbii ${⊢}\exists {y}\in {V}\phantom{\rule{.4em}{0ex}}¬\left(\left(\left\{\left\{{A},{x}\right\},\left\{{x},{C}\right\}\right\}\subseteq {E}\wedge \left\{\left\{{A},{y}\right\},\left\{{y},{C}\right\}\right\}\subseteq {E}\right)\to {x}={y}\right)↔\exists {y}\in {V}\phantom{\rule{.4em}{0ex}}\left(\left(\left\{\left\{{A},{x}\right\},\left\{{x},{C}\right\}\right\}\subseteq {E}\wedge \left\{\left\{{A},{y}\right\},\left\{{y},{C}\right\}\right\}\subseteq {E}\right)\wedge {x}\ne {y}\right)$
31 24 30 bitr3i ${⊢}¬\forall {y}\in {V}\phantom{\rule{.4em}{0ex}}\left(\left(\left\{\left\{{A},{x}\right\},\left\{{x},{C}\right\}\right\}\subseteq {E}\wedge \left\{\left\{{A},{y}\right\},\left\{{y},{C}\right\}\right\}\subseteq {E}\right)\to {x}={y}\right)↔\exists {y}\in {V}\phantom{\rule{.4em}{0ex}}\left(\left(\left\{\left\{{A},{x}\right\},\left\{{x},{C}\right\}\right\}\subseteq {E}\wedge \left\{\left\{{A},{y}\right\},\left\{{y},{C}\right\}\right\}\subseteq {E}\right)\wedge {x}\ne {y}\right)$
32 31 rexbii ${⊢}\exists {x}\in {V}\phantom{\rule{.4em}{0ex}}¬\forall {y}\in {V}\phantom{\rule{.4em}{0ex}}\left(\left(\left\{\left\{{A},{x}\right\},\left\{{x},{C}\right\}\right\}\subseteq {E}\wedge \left\{\left\{{A},{y}\right\},\left\{{y},{C}\right\}\right\}\subseteq {E}\right)\to {x}={y}\right)↔\exists {x}\in {V}\phantom{\rule{.4em}{0ex}}\exists {y}\in {V}\phantom{\rule{.4em}{0ex}}\left(\left(\left\{\left\{{A},{x}\right\},\left\{{x},{C}\right\}\right\}\subseteq {E}\wedge \left\{\left\{{A},{y}\right\},\left\{{y},{C}\right\}\right\}\subseteq {E}\right)\wedge {x}\ne {y}\right)$
33 23 32 bitr3i ${⊢}¬\forall {x}\in {V}\phantom{\rule{.4em}{0ex}}\forall {y}\in {V}\phantom{\rule{.4em}{0ex}}\left(\left(\left\{\left\{{A},{x}\right\},\left\{{x},{C}\right\}\right\}\subseteq {E}\wedge \left\{\left\{{A},{y}\right\},\left\{{y},{C}\right\}\right\}\subseteq {E}\right)\to {x}={y}\right)↔\exists {x}\in {V}\phantom{\rule{.4em}{0ex}}\exists {y}\in {V}\phantom{\rule{.4em}{0ex}}\left(\left(\left\{\left\{{A},{x}\right\},\left\{{x},{C}\right\}\right\}\subseteq {E}\wedge \left\{\left\{{A},{y}\right\},\left\{{y},{C}\right\}\right\}\subseteq {E}\right)\wedge {x}\ne {y}\right)$
34 22 33 sylibr ${⊢}\left(\left(\left\{\left\{{A},{B}\right\},\left\{{B},{C}\right\}\right\}\subseteq {E}\wedge \left\{\left\{{A},{D}\right\},\left\{{D},{C}\right\}\right\}\subseteq {E}\right)\wedge \left({B}\in {V}\wedge {D}\in {V}\wedge {B}\ne {D}\right)\right)\to ¬\forall {x}\in {V}\phantom{\rule{.4em}{0ex}}\forall {y}\in {V}\phantom{\rule{.4em}{0ex}}\left(\left(\left\{\left\{{A},{x}\right\},\left\{{x},{C}\right\}\right\}\subseteq {E}\wedge \left\{\left\{{A},{y}\right\},\left\{{y},{C}\right\}\right\}\subseteq {E}\right)\to {x}={y}\right)$
35 34 intnand ${⊢}\left(\left(\left\{\left\{{A},{B}\right\},\left\{{B},{C}\right\}\right\}\subseteq {E}\wedge \left\{\left\{{A},{D}\right\},\left\{{D},{C}\right\}\right\}\subseteq {E}\right)\wedge \left({B}\in {V}\wedge {D}\in {V}\wedge {B}\ne {D}\right)\right)\to ¬\left(\exists {x}\in {V}\phantom{\rule{.4em}{0ex}}\left\{\left\{{A},{x}\right\},\left\{{x},{C}\right\}\right\}\subseteq {E}\wedge \forall {x}\in {V}\phantom{\rule{.4em}{0ex}}\forall {y}\in {V}\phantom{\rule{.4em}{0ex}}\left(\left(\left\{\left\{{A},{x}\right\},\left\{{x},{C}\right\}\right\}\subseteq {E}\wedge \left\{\left\{{A},{y}\right\},\left\{{y},{C}\right\}\right\}\subseteq {E}\right)\to {x}={y}\right)\right)$
36 preq2 ${⊢}{x}={y}\to \left\{{A},{x}\right\}=\left\{{A},{y}\right\}$
37 preq1 ${⊢}{x}={y}\to \left\{{x},{C}\right\}=\left\{{y},{C}\right\}$
38 36 37 preq12d ${⊢}{x}={y}\to \left\{\left\{{A},{x}\right\},\left\{{x},{C}\right\}\right\}=\left\{\left\{{A},{y}\right\},\left\{{y},{C}\right\}\right\}$
39 38 sseq1d ${⊢}{x}={y}\to \left(\left\{\left\{{A},{x}\right\},\left\{{x},{C}\right\}\right\}\subseteq {E}↔\left\{\left\{{A},{y}\right\},\left\{{y},{C}\right\}\right\}\subseteq {E}\right)$
40 39 reu4 ${⊢}\exists !{x}\in {V}\phantom{\rule{.4em}{0ex}}\left\{\left\{{A},{x}\right\},\left\{{x},{C}\right\}\right\}\subseteq {E}↔\left(\exists {x}\in {V}\phantom{\rule{.4em}{0ex}}\left\{\left\{{A},{x}\right\},\left\{{x},{C}\right\}\right\}\subseteq {E}\wedge \forall {x}\in {V}\phantom{\rule{.4em}{0ex}}\forall {y}\in {V}\phantom{\rule{.4em}{0ex}}\left(\left(\left\{\left\{{A},{x}\right\},\left\{{x},{C}\right\}\right\}\subseteq {E}\wedge \left\{\left\{{A},{y}\right\},\left\{{y},{C}\right\}\right\}\subseteq {E}\right)\to {x}={y}\right)\right)$
41 35 40 sylnibr ${⊢}\left(\left(\left\{\left\{{A},{B}\right\},\left\{{B},{C}\right\}\right\}\subseteq {E}\wedge \left\{\left\{{A},{D}\right\},\left\{{D},{C}\right\}\right\}\subseteq {E}\right)\wedge \left({B}\in {V}\wedge {D}\in {V}\wedge {B}\ne {D}\right)\right)\to ¬\exists !{x}\in {V}\phantom{\rule{.4em}{0ex}}\left\{\left\{{A},{x}\right\},\left\{{x},{C}\right\}\right\}\subseteq {E}$
42 1 41 stoic3 ${⊢}\left(\left(\left\{{A},{B}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\right)\wedge \left(\left\{{C},{D}\right\}\in {E}\wedge \left\{{D},{A}\right\}\in {E}\right)\wedge \left({B}\in {V}\wedge {D}\in {V}\wedge {B}\ne {D}\right)\right)\to ¬\exists !{x}\in {V}\phantom{\rule{.4em}{0ex}}\left\{\left\{{A},{x}\right\},\left\{{x},{C}\right\}\right\}\subseteq {E}$