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 ( ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ∧ ( { 𝐶 , 𝐷 } ∈ 𝐸 ∧ { 𝐷 , 𝐴 } ∈ 𝐸 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ∧ 𝐵 ≠ 𝐷 ) ) → ¬ ∃! 𝑥 ∈ 𝑉 { { 𝐴 , 𝑥 } , { 𝑥 , 𝐶 } } ⊆ 𝐸 )

Proof

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