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 ⊢ A B ∈ E ∧ B C ∈ E ∧ C D ∈ E ∧ D A ∈ E ∧ B ∈ V ∧ D ∈ V ∧ B ≠ D → ¬ ∃! x ∈ V A x x C ⊆ E

Proof

Step Hyp Ref Expression
1 4cycl2v2nb ⊢ A B ∈ E ∧ B C ∈ E ∧ C D ∈ E ∧ D A ∈ E → A B B C ⊆ E ∧ A D D C ⊆ E
2 preq2 ⊢ x = B → A x = A B
3 preq1 ⊢ x = B → x C = B C
4 2 3 preq12d ⊢ x = B → A x x C = A B B C
5 4 sseq1d ⊢ x = B → A x x C ⊆ E ↔ A B B C ⊆ E
6 5 anbi1d ⊢ x = B → A x x C ⊆ E ∧ A y y C ⊆ E ↔ A B B C ⊆ E ∧ A y y C ⊆ E
7 neeq1 ⊢ x = B → x ≠ y ↔ B ≠ y
8 6 7 anbi12d ⊢ x = B → A x x C ⊆ E ∧ A y y C ⊆ E ∧ x ≠ y ↔ A B B C ⊆ E ∧ A y y C ⊆ E ∧ B ≠ y
9 preq2 ⊢ y = D → A y = A D
10 preq1 ⊢ y = D → y C = D C
11 9 10 preq12d ⊢ y = D → A y y C = A D D C
12 11 sseq1d ⊢ y = D → A y y C ⊆ E ↔ A D D C ⊆ E
13 12 anbi2d ⊢ y = D → A B B C ⊆ E ∧ A y y C ⊆ E ↔ A B B C ⊆ E ∧ A D D C ⊆ E
14 neeq2 ⊢ y = D → B ≠ y ↔ B ≠ D
15 13 14 anbi12d ⊢ y = D → A B B C ⊆ E ∧ A y y C ⊆ E ∧ B ≠ y ↔ A B B C ⊆ E ∧ A D D C ⊆ E ∧ B ≠ D
16 8 15 rspc2ev ⊢ B ∈ V ∧ D ∈ V ∧ A B B C ⊆ E ∧ A D D C ⊆ E ∧ B ≠ D → ∃ x ∈ V ∃ y ∈ V A x x C ⊆ E ∧ A y y C ⊆ E ∧ x ≠ y
17 16 3expa ⊢ B ∈ V ∧ D ∈ V ∧ A B B C ⊆ E ∧ A D D C ⊆ E ∧ B ≠ D → ∃ x ∈ V ∃ y ∈ V A x x C ⊆ E ∧ A y y C ⊆ E ∧ x ≠ y
18 17 expcom ⊢ A B B C ⊆ E ∧ A D D C ⊆ E ∧ B ≠ D → B ∈ V ∧ D ∈ V → ∃ x ∈ V ∃ y ∈ V A x x C ⊆ E ∧ A y y C ⊆ E ∧ x ≠ y
19 18 ex ⊢ A B B C ⊆ E ∧ A D D C ⊆ E → B ≠ D → B ∈ V ∧ D ∈ V → ∃ x ∈ V ∃ y ∈ V A x x C ⊆ E ∧ A y y C ⊆ E ∧ x ≠ y
20 19 com13 ⊢ B ∈ V ∧ D ∈ V → B ≠ D → A B B C ⊆ E ∧ A D D C ⊆ E → ∃ x ∈ V ∃ y ∈ V A x x C ⊆ E ∧ A y y C ⊆ E ∧ x ≠ y
21 20 3impia ⊢ B ∈ V ∧ D ∈ V ∧ B ≠ D → A B B C ⊆ E ∧ A D D C ⊆ E → ∃ x ∈ V ∃ y ∈ V A x x C ⊆ E ∧ A y y C ⊆ E ∧ x ≠ y
22 21 impcom ⊢ A B B C ⊆ E ∧ A D D C ⊆ E ∧ B ∈ V ∧ D ∈ V ∧ B ≠ D → ∃ x ∈ V ∃ y ∈ V A x x C ⊆ E ∧ A y y C ⊆ E ∧ x ≠ y
23 rexnal ⊢ ∃ x ∈ V ¬ ∀ y ∈ V A x x C ⊆ E ∧ A y y C ⊆ E → x = y ↔ ¬ ∀ x ∈ V ∀ y ∈ V A x x C ⊆ E ∧ A y y C ⊆ E → x = y
24 rexnal ⊢ ∃ y ∈ V ¬ A x x C ⊆ E ∧ A y y C ⊆ E → x = y ↔ ¬ ∀ y ∈ V A x x C ⊆ E ∧ A y y C ⊆ E → x = y
25 annim ⊢ A x x C ⊆ E ∧ A y y C ⊆ E ∧ ¬ x = y ↔ ¬ A x x C ⊆ E ∧ A y y C ⊆ E → x = y
26 df-ne ⊢ x ≠ y ↔ ¬ x = y
27 26 bicomi ⊢ ¬ x = y ↔ x ≠ y
28 27 anbi2i ⊢ A x x C ⊆ E ∧ A y y C ⊆ E ∧ ¬ x = y ↔ A x x C ⊆ E ∧ A y y C ⊆ E ∧ x ≠ y
29 25 28 bitr3i ⊢ ¬ A x x C ⊆ E ∧ A y y C ⊆ E → x = y ↔ A x x C ⊆ E ∧ A y y C ⊆ E ∧ x ≠ y
30 29 rexbii ⊢ ∃ y ∈ V ¬ A x x C ⊆ E ∧ A y y C ⊆ E → x = y ↔ ∃ y ∈ V A x x C ⊆ E ∧ A y y C ⊆ E ∧ x ≠ y
31 24 30 bitr3i ⊢ ¬ ∀ y ∈ V A x x C ⊆ E ∧ A y y C ⊆ E → x = y ↔ ∃ y ∈ V A x x C ⊆ E ∧ A y y C ⊆ E ∧ x ≠ y
32 31 rexbii ⊢ ∃ x ∈ V ¬ ∀ y ∈ V A x x C ⊆ E ∧ A y y C ⊆ E → x = y ↔ ∃ x ∈ V ∃ y ∈ V A x x C ⊆ E ∧ A y y C ⊆ E ∧ x ≠ y
33 23 32 bitr3i ⊢ ¬ ∀ x ∈ V ∀ y ∈ V A x x C ⊆ E ∧ A y y C ⊆ E → x = y ↔ ∃ x ∈ V ∃ y ∈ V A x x C ⊆ E ∧ A y y C ⊆ E ∧ x ≠ y
34 22 33 sylibr ⊢ A B B C ⊆ E ∧ A D D C ⊆ E ∧ B ∈ V ∧ D ∈ V ∧ B ≠ D → ¬ ∀ x ∈ V ∀ y ∈ V A x x C ⊆ E ∧ A y y C ⊆ E → x = y
35 34 intnand ⊢ A B B C ⊆ E ∧ A D D C ⊆ E ∧ B ∈ V ∧ D ∈ V ∧ B ≠ D → ¬ ∃ x ∈ V A x x C ⊆ E ∧ ∀ x ∈ V ∀ y ∈ V A x x C ⊆ E ∧ A y y C ⊆ E → x = y
36 preq2 ⊢ x = y → A x = A y
37 preq1 ⊢ x = y → x C = y C
38 36 37 preq12d ⊢ x = y → A x x C = A y y C
39 38 sseq1d ⊢ x = y → A x x C ⊆ E ↔ A y y C ⊆ E
40 39 reu4 ⊢ ∃! x ∈ V A x x C ⊆ E ↔ ∃ x ∈ V A x x C ⊆ E ∧ ∀ x ∈ V ∀ y ∈ V A x x C ⊆ E ∧ A y y C ⊆ E → x = y
41 35 40 sylnibr ⊢ A B B C ⊆ E ∧ A D D C ⊆ E ∧ B ∈ V ∧ D ∈ V ∧ B ≠ D → ¬ ∃! x ∈ V A x x C ⊆ E
42 1 41 stoic3 ⊢ A B ∈ E ∧ B C ∈ E ∧ C D ∈ E ∧ D A ∈ E ∧ B ∈ V ∧ D ∈ V ∧ B ≠ D → ¬ ∃! x ∈ V A x x C ⊆ E