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. E /\ { B , C } e. E ) /\ ( { C , D } e. E /\ { D , A } e. E ) /\ ( B e. V /\ D e. V /\ B =/= D ) ) -> -. E! x e. V { { A , x } , { x , C } } C_ E )

Proof

Step Hyp Ref Expression
1 4cycl2v2nb 
 |-  ( ( ( { A , B } e. E /\ { B , C } e. E ) /\ ( { C , D } e. E /\ { D , A } e. E ) ) -> ( { { A , B } , { B , C } } C_ E /\ { { A , D } , { D , C } } 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 } } C_ E <-> { { A , B } , { B , C } } C_ E ) )
6 5 anbi1d 
 |-  ( x = B -> ( ( { { A , x } , { x , C } } C_ E /\ { { A , y } , { y , C } } C_ E ) <-> ( { { A , B } , { B , C } } C_ E /\ { { A , y } , { y , C } } C_ E ) ) )
7 neeq1 
 |-  ( x = B -> ( x =/= y <-> B =/= y ) )
8 6 7 anbi12d 
 |-  ( x = B -> ( ( ( { { A , x } , { x , C } } C_ E /\ { { A , y } , { y , C } } C_ E ) /\ x =/= y ) <-> ( ( { { A , B } , { B , C } } C_ E /\ { { A , y } , { y , C } } 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 } } C_ E <-> { { A , D } , { D , C } } C_ E ) )
13 12 anbi2d 
 |-  ( y = D -> ( ( { { A , B } , { B , C } } C_ E /\ { { A , y } , { y , C } } C_ E ) <-> ( { { A , B } , { B , C } } C_ E /\ { { A , D } , { D , C } } C_ E ) ) )
14 neeq2 
 |-  ( y = D -> ( B =/= y <-> B =/= D ) )
15 13 14 anbi12d 
 |-  ( y = D -> ( ( ( { { A , B } , { B , C } } C_ E /\ { { A , y } , { y , C } } C_ E ) /\ B =/= y ) <-> ( ( { { A , B } , { B , C } } C_ E /\ { { A , D } , { D , C } } C_ E ) /\ B =/= D ) ) )
16 8 15 rspc2ev 
 |-  ( ( B e. V /\ D e. V /\ ( ( { { A , B } , { B , C } } C_ E /\ { { A , D } , { D , C } } C_ E ) /\ B =/= D ) ) -> E. x e. V E. y e. V ( ( { { A , x } , { x , C } } C_ E /\ { { A , y } , { y , C } } C_ E ) /\ x =/= y ) )
17 16 3expa 
 |-  ( ( ( B e. V /\ D e. V ) /\ ( ( { { A , B } , { B , C } } C_ E /\ { { A , D } , { D , C } } C_ E ) /\ B =/= D ) ) -> E. x e. V E. y e. V ( ( { { A , x } , { x , C } } C_ E /\ { { A , y } , { y , C } } C_ E ) /\ x =/= y ) )
18 17 expcom 
 |-  ( ( ( { { A , B } , { B , C } } C_ E /\ { { A , D } , { D , C } } C_ E ) /\ B =/= D ) -> ( ( B e. V /\ D e. V ) -> E. x e. V E. y e. V ( ( { { A , x } , { x , C } } C_ E /\ { { A , y } , { y , C } } C_ E ) /\ x =/= y ) ) )
19 18 ex 
 |-  ( ( { { A , B } , { B , C } } C_ E /\ { { A , D } , { D , C } } C_ E ) -> ( B =/= D -> ( ( B e. V /\ D e. V ) -> E. x e. V E. y e. V ( ( { { A , x } , { x , C } } C_ E /\ { { A , y } , { y , C } } C_ E ) /\ x =/= y ) ) ) )
20 19 com13 
 |-  ( ( B e. V /\ D e. V ) -> ( B =/= D -> ( ( { { A , B } , { B , C } } C_ E /\ { { A , D } , { D , C } } C_ E ) -> E. x e. V E. y e. V ( ( { { A , x } , { x , C } } C_ E /\ { { A , y } , { y , C } } C_ E ) /\ x =/= y ) ) ) )
21 20 3impia 
 |-  ( ( B e. V /\ D e. V /\ B =/= D ) -> ( ( { { A , B } , { B , C } } C_ E /\ { { A , D } , { D , C } } C_ E ) -> E. x e. V E. y e. V ( ( { { A , x } , { x , C } } C_ E /\ { { A , y } , { y , C } } C_ E ) /\ x =/= y ) ) )
22 21 impcom 
 |-  ( ( ( { { A , B } , { B , C } } C_ E /\ { { A , D } , { D , C } } C_ E ) /\ ( B e. V /\ D e. V /\ B =/= D ) ) -> E. x e. V E. y e. V ( ( { { A , x } , { x , C } } C_ E /\ { { A , y } , { y , C } } C_ E ) /\ x =/= y ) )
23 rexnal 
 |-  ( E. x e. V -. A. y e. V ( ( { { A , x } , { x , C } } C_ E /\ { { A , y } , { y , C } } C_ E ) -> x = y ) <-> -. A. x e. V A. y e. V ( ( { { A , x } , { x , C } } C_ E /\ { { A , y } , { y , C } } C_ E ) -> x = y ) )
24 rexnal 
 |-  ( E. y e. V -. ( ( { { A , x } , { x , C } } C_ E /\ { { A , y } , { y , C } } C_ E ) -> x = y ) <-> -. A. y e. V ( ( { { A , x } , { x , C } } C_ E /\ { { A , y } , { y , C } } C_ E ) -> x = y ) )
25 annim 
 |-  ( ( ( { { A , x } , { x , C } } C_ E /\ { { A , y } , { y , C } } C_ E ) /\ -. x = y ) <-> -. ( ( { { A , x } , { x , C } } C_ E /\ { { A , y } , { y , C } } 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 } } C_ E /\ { { A , y } , { y , C } } C_ E ) /\ -. x = y ) <-> ( ( { { A , x } , { x , C } } C_ E /\ { { A , y } , { y , C } } C_ E ) /\ x =/= y ) )
29 25 28 bitr3i 
 |-  ( -. ( ( { { A , x } , { x , C } } C_ E /\ { { A , y } , { y , C } } C_ E ) -> x = y ) <-> ( ( { { A , x } , { x , C } } C_ E /\ { { A , y } , { y , C } } C_ E ) /\ x =/= y ) )
30 29 rexbii 
 |-  ( E. y e. V -. ( ( { { A , x } , { x , C } } C_ E /\ { { A , y } , { y , C } } C_ E ) -> x = y ) <-> E. y e. V ( ( { { A , x } , { x , C } } C_ E /\ { { A , y } , { y , C } } C_ E ) /\ x =/= y ) )
31 24 30 bitr3i 
 |-  ( -. A. y e. V ( ( { { A , x } , { x , C } } C_ E /\ { { A , y } , { y , C } } C_ E ) -> x = y ) <-> E. y e. V ( ( { { A , x } , { x , C } } C_ E /\ { { A , y } , { y , C } } C_ E ) /\ x =/= y ) )
32 31 rexbii 
 |-  ( E. x e. V -. A. y e. V ( ( { { A , x } , { x , C } } C_ E /\ { { A , y } , { y , C } } C_ E ) -> x = y ) <-> E. x e. V E. y e. V ( ( { { A , x } , { x , C } } C_ E /\ { { A , y } , { y , C } } C_ E ) /\ x =/= y ) )
33 23 32 bitr3i 
 |-  ( -. A. x e. V A. y e. V ( ( { { A , x } , { x , C } } C_ E /\ { { A , y } , { y , C } } C_ E ) -> x = y ) <-> E. x e. V E. y e. V ( ( { { A , x } , { x , C } } C_ E /\ { { A , y } , { y , C } } C_ E ) /\ x =/= y ) )
34 22 33 sylibr 
 |-  ( ( ( { { A , B } , { B , C } } C_ E /\ { { A , D } , { D , C } } C_ E ) /\ ( B e. V /\ D e. V /\ B =/= D ) ) -> -. A. x e. V A. y e. V ( ( { { A , x } , { x , C } } C_ E /\ { { A , y } , { y , C } } C_ E ) -> x = y ) )
35 34 intnand 
 |-  ( ( ( { { A , B } , { B , C } } C_ E /\ { { A , D } , { D , C } } C_ E ) /\ ( B e. V /\ D e. V /\ B =/= D ) ) -> -. ( E. x e. V { { A , x } , { x , C } } C_ E /\ A. x e. V A. y e. V ( ( { { A , x } , { x , C } } C_ E /\ { { A , y } , { y , C } } 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 } } C_ E <-> { { A , y } , { y , C } } C_ E ) )
40 39 reu4 
 |-  ( E! x e. V { { A , x } , { x , C } } C_ E <-> ( E. x e. V { { A , x } , { x , C } } C_ E /\ A. x e. V A. y e. V ( ( { { A , x } , { x , C } } C_ E /\ { { A , y } , { y , C } } C_ E ) -> x = y ) ) )
41 35 40 sylnibr 
 |-  ( ( ( { { A , B } , { B , C } } C_ E /\ { { A , D } , { D , C } } C_ E ) /\ ( B e. V /\ D e. V /\ B =/= D ) ) -> -. E! x e. V { { A , x } , { x , C } } C_ E )
42 1 41 stoic3 
 |-  ( ( ( { A , B } e. E /\ { B , C } e. E ) /\ ( { C , D } e. E /\ { D , A } e. E ) /\ ( B e. V /\ D e. V /\ B =/= D ) ) -> -. E! x e. V { { A , x } , { x , C } } C_ E )