Metamath Proof Explorer

Theorem 3cyclfrgrrn1

Description: Every vertex in a friendship graph (with more than 1 vertex) is part of a 3-cycle. (Contributed by Alexander van der Vekens, 16-Nov-2017) (Revised by AV, 2-Apr-2021)

Ref Expression
Hypotheses 3cyclfrgrrn1.v 
|- V = ( Vtx ` G )
3cyclfrgrrn1.e 
|- E = ( Edg ` G )
Assertion 3cyclfrgrrn1 
|- ( ( G e. FriendGraph /\ ( A e. V /\ C e. V ) /\ A =/= C ) -> E. b e. V E. c e. V ( { A , b } e. E /\ { b , c } e. E /\ { c , A } e. E ) )

Proof

Step Hyp Ref Expression
1 3cyclfrgrrn1.v 
 |-  V = ( Vtx ` G )
2 3cyclfrgrrn1.e 
 |-  E = ( Edg ` G )
3 1 2 2pthfrgrrn2 
 |-  ( G e. FriendGraph -> A. a e. V A. z e. ( V \ { a } ) E. x e. V ( ( { a , x } e. E /\ { x , z } e. E ) /\ ( a =/= x /\ x =/= z ) ) )
4 necom 
 |-  ( A =/= C <-> C =/= A )
5 eldifsn 
 |-  ( C e. ( V \ { A } ) <-> ( C e. V /\ C =/= A ) )
6 5 simplbi2com 
 |-  ( C =/= A -> ( C e. V -> C e. ( V \ { A } ) ) )
7 4 6 sylbi 
 |-  ( A =/= C -> ( C e. V -> C e. ( V \ { A } ) ) )
8 7 com12 
 |-  ( C e. V -> ( A =/= C -> C e. ( V \ { A } ) ) )
9 8 adantl 
 |-  ( ( A e. V /\ C e. V ) -> ( A =/= C -> C e. ( V \ { A } ) ) )
10 9 imp 
 |-  ( ( ( A e. V /\ C e. V ) /\ A =/= C ) -> C e. ( V \ { A } ) )
11 sneq 
 |-  ( a = A -> { a } = { A } )
12 11 difeq2d 
 |-  ( a = A -> ( V \ { a } ) = ( V \ { A } ) )
13 preq1 
 |-  ( a = A -> { a , x } = { A , x } )
14 13 eleq1d 
 |-  ( a = A -> ( { a , x } e. E <-> { A , x } e. E ) )
15 14 anbi1d 
 |-  ( a = A -> ( ( { a , x } e. E /\ { x , z } e. E ) <-> ( { A , x } e. E /\ { x , z } e. E ) ) )
16 neeq1 
 |-  ( a = A -> ( a =/= x <-> A =/= x ) )
17 16 anbi1d 
 |-  ( a = A -> ( ( a =/= x /\ x =/= z ) <-> ( A =/= x /\ x =/= z ) ) )
18 15 17 anbi12d 
 |-  ( a = A -> ( ( ( { a , x } e. E /\ { x , z } e. E ) /\ ( a =/= x /\ x =/= z ) ) <-> ( ( { A , x } e. E /\ { x , z } e. E ) /\ ( A =/= x /\ x =/= z ) ) ) )
19 18 rexbidv 
 |-  ( a = A -> ( E. x e. V ( ( { a , x } e. E /\ { x , z } e. E ) /\ ( a =/= x /\ x =/= z ) ) <-> E. x e. V ( ( { A , x } e. E /\ { x , z } e. E ) /\ ( A =/= x /\ x =/= z ) ) ) )
20 12 19 raleqbidv 
 |-  ( a = A -> ( A. z e. ( V \ { a } ) E. x e. V ( ( { a , x } e. E /\ { x , z } e. E ) /\ ( a =/= x /\ x =/= z ) ) <-> A. z e. ( V \ { A } ) E. x e. V ( ( { A , x } e. E /\ { x , z } e. E ) /\ ( A =/= x /\ x =/= z ) ) ) )
21 20 rspcv 
 |-  ( A e. V -> ( A. a e. V A. z e. ( V \ { a } ) E. x e. V ( ( { a , x } e. E /\ { x , z } e. E ) /\ ( a =/= x /\ x =/= z ) ) -> A. z e. ( V \ { A } ) E. x e. V ( ( { A , x } e. E /\ { x , z } e. E ) /\ ( A =/= x /\ x =/= z ) ) ) )
22 21 ad2antrr 
 |-  ( ( ( A e. V /\ C e. V ) /\ A =/= C ) -> ( A. a e. V A. z e. ( V \ { a } ) E. x e. V ( ( { a , x } e. E /\ { x , z } e. E ) /\ ( a =/= x /\ x =/= z ) ) -> A. z e. ( V \ { A } ) E. x e. V ( ( { A , x } e. E /\ { x , z } e. E ) /\ ( A =/= x /\ x =/= z ) ) ) )
23 preq2 
 |-  ( z = C -> { x , z } = { x , C } )
24 23 eleq1d 
 |-  ( z = C -> ( { x , z } e. E <-> { x , C } e. E ) )
25 24 anbi2d 
 |-  ( z = C -> ( ( { A , x } e. E /\ { x , z } e. E ) <-> ( { A , x } e. E /\ { x , C } e. E ) ) )
26 neeq2 
 |-  ( z = C -> ( x =/= z <-> x =/= C ) )
27 26 anbi2d 
 |-  ( z = C -> ( ( A =/= x /\ x =/= z ) <-> ( A =/= x /\ x =/= C ) ) )
28 25 27 anbi12d 
 |-  ( z = C -> ( ( ( { A , x } e. E /\ { x , z } e. E ) /\ ( A =/= x /\ x =/= z ) ) <-> ( ( { A , x } e. E /\ { x , C } e. E ) /\ ( A =/= x /\ x =/= C ) ) ) )
29 28 rexbidv 
 |-  ( z = C -> ( E. x e. V ( ( { A , x } e. E /\ { x , z } e. E ) /\ ( A =/= x /\ x =/= z ) ) <-> E. x e. V ( ( { A , x } e. E /\ { x , C } e. E ) /\ ( A =/= x /\ x =/= C ) ) ) )
30 29 rspcv 
 |-  ( C e. ( V \ { A } ) -> ( A. z e. ( V \ { A } ) E. x e. V ( ( { A , x } e. E /\ { x , z } e. E ) /\ ( A =/= x /\ x =/= z ) ) -> E. x e. V ( ( { A , x } e. E /\ { x , C } e. E ) /\ ( A =/= x /\ x =/= C ) ) ) )
31 10 22 30 sylsyld 
 |-  ( ( ( A e. V /\ C e. V ) /\ A =/= C ) -> ( A. a e. V A. z e. ( V \ { a } ) E. x e. V ( ( { a , x } e. E /\ { x , z } e. E ) /\ ( a =/= x /\ x =/= z ) ) -> E. x e. V ( ( { A , x } e. E /\ { x , C } e. E ) /\ ( A =/= x /\ x =/= C ) ) ) )
32 1 2 2pthfrgrrn 
 |-  ( G e. FriendGraph -> A. u e. V A. v e. ( V \ { u } ) E. y e. V ( { u , y } e. E /\ { y , v } e. E ) )
33 necom 
 |-  ( A =/= x <-> x =/= A )
34 eldifsn 
 |-  ( x e. ( V \ { A } ) <-> ( x e. V /\ x =/= A ) )
35 34 simplbi2com 
 |-  ( x =/= A -> ( x e. V -> x e. ( V \ { A } ) ) )
36 33 35 sylbi 
 |-  ( A =/= x -> ( x e. V -> x e. ( V \ { A } ) ) )
37 36 adantr 
 |-  ( ( A =/= x /\ A e. V ) -> ( x e. V -> x e. ( V \ { A } ) ) )
38 37 imp 
 |-  ( ( ( A =/= x /\ A e. V ) /\ x e. V ) -> x e. ( V \ { A } ) )
39 sneq 
 |-  ( u = A -> { u } = { A } )
40 39 difeq2d 
 |-  ( u = A -> ( V \ { u } ) = ( V \ { A } ) )
41 preq1 
 |-  ( u = A -> { u , y } = { A , y } )
42 41 eleq1d 
 |-  ( u = A -> ( { u , y } e. E <-> { A , y } e. E ) )
43 42 anbi1d 
 |-  ( u = A -> ( ( { u , y } e. E /\ { y , v } e. E ) <-> ( { A , y } e. E /\ { y , v } e. E ) ) )
44 43 rexbidv 
 |-  ( u = A -> ( E. y e. V ( { u , y } e. E /\ { y , v } e. E ) <-> E. y e. V ( { A , y } e. E /\ { y , v } e. E ) ) )
45 40 44 raleqbidv 
 |-  ( u = A -> ( A. v e. ( V \ { u } ) E. y e. V ( { u , y } e. E /\ { y , v } e. E ) <-> A. v e. ( V \ { A } ) E. y e. V ( { A , y } e. E /\ { y , v } e. E ) ) )
46 45 rspcv 
 |-  ( A e. V -> ( A. u e. V A. v e. ( V \ { u } ) E. y e. V ( { u , y } e. E /\ { y , v } e. E ) -> A. v e. ( V \ { A } ) E. y e. V ( { A , y } e. E /\ { y , v } e. E ) ) )
47 46 adantl 
 |-  ( ( A =/= x /\ A e. V ) -> ( A. u e. V A. v e. ( V \ { u } ) E. y e. V ( { u , y } e. E /\ { y , v } e. E ) -> A. v e. ( V \ { A } ) E. y e. V ( { A , y } e. E /\ { y , v } e. E ) ) )
48 47 adantr 
 |-  ( ( ( A =/= x /\ A e. V ) /\ x e. V ) -> ( A. u e. V A. v e. ( V \ { u } ) E. y e. V ( { u , y } e. E /\ { y , v } e. E ) -> A. v e. ( V \ { A } ) E. y e. V ( { A , y } e. E /\ { y , v } e. E ) ) )
49 preq2 
 |-  ( v = x -> { y , v } = { y , x } )
50 49 eleq1d 
 |-  ( v = x -> ( { y , v } e. E <-> { y , x } e. E ) )
51 50 anbi2d 
 |-  ( v = x -> ( ( { A , y } e. E /\ { y , v } e. E ) <-> ( { A , y } e. E /\ { y , x } e. E ) ) )
52 51 rexbidv 
 |-  ( v = x -> ( E. y e. V ( { A , y } e. E /\ { y , v } e. E ) <-> E. y e. V ( { A , y } e. E /\ { y , x } e. E ) ) )
53 52 rspcv 
 |-  ( x e. ( V \ { A } ) -> ( A. v e. ( V \ { A } ) E. y e. V ( { A , y } e. E /\ { y , v } e. E ) -> E. y e. V ( { A , y } e. E /\ { y , x } e. E ) ) )
54 38 48 53 sylsyld 
 |-  ( ( ( A =/= x /\ A e. V ) /\ x e. V ) -> ( A. u e. V A. v e. ( V \ { u } ) E. y e. V ( { u , y } e. E /\ { y , v } e. E ) -> E. y e. V ( { A , y } e. E /\ { y , x } e. E ) ) )
55 prcom 
 |-  { A , y } = { y , A }
56 55 eleq1i 
 |-  ( { A , y } e. E <-> { y , A } e. E )
57 prcom 
 |-  { y , x } = { x , y }
58 57 eleq1i 
 |-  ( { y , x } e. E <-> { x , y } e. E )
59 56 58 anbi12ci 
 |-  ( ( { A , y } e. E /\ { y , x } e. E ) <-> ( { x , y } e. E /\ { y , A } e. E ) )
60 preq2 
 |-  ( b = x -> { A , b } = { A , x } )
61 60 eleq1d 
 |-  ( b = x -> ( { A , b } e. E <-> { A , x } e. E ) )
62 preq1 
 |-  ( b = x -> { b , c } = { x , c } )
63 62 eleq1d 
 |-  ( b = x -> ( { b , c } e. E <-> { x , c } e. E ) )
64 biidd 
 |-  ( b = x -> ( { c , A } e. E <-> { c , A } e. E ) )
65 61 63 64 3anbi123d 
 |-  ( b = x -> ( ( { A , b } e. E /\ { b , c } e. E /\ { c , A } e. E ) <-> ( { A , x } e. E /\ { x , c } e. E /\ { c , A } e. E ) ) )
66 biidd 
 |-  ( c = y -> ( { A , x } e. E <-> { A , x } e. E ) )
67 preq2 
 |-  ( c = y -> { x , c } = { x , y } )
68 67 eleq1d 
 |-  ( c = y -> ( { x , c } e. E <-> { x , y } e. E ) )
69 preq1 
 |-  ( c = y -> { c , A } = { y , A } )
70 69 eleq1d 
 |-  ( c = y -> ( { c , A } e. E <-> { y , A } e. E ) )
71 66 68 70 3anbi123d 
 |-  ( c = y -> ( ( { A , x } e. E /\ { x , c } e. E /\ { c , A } e. E ) <-> ( { A , x } e. E /\ { x , y } e. E /\ { y , A } e. E ) ) )
72 65 71 rspc2ev 
 |-  ( ( x e. V /\ y e. V /\ ( { A , x } e. E /\ { x , y } e. E /\ { y , A } e. E ) ) -> E. b e. V E. c e. V ( { A , b } e. E /\ { b , c } e. E /\ { c , A } e. E ) )
73 72 3expa 
 |-  ( ( ( x e. V /\ y e. V ) /\ ( { A , x } e. E /\ { x , y } e. E /\ { y , A } e. E ) ) -> E. b e. V E. c e. V ( { A , b } e. E /\ { b , c } e. E /\ { c , A } e. E ) )
74 73 expcom 
 |-  ( ( { A , x } e. E /\ { x , y } e. E /\ { y , A } e. E ) -> ( ( x e. V /\ y e. V ) -> E. b e. V E. c e. V ( { A , b } e. E /\ { b , c } e. E /\ { c , A } e. E ) ) )
75 74 3expib 
 |-  ( { A , x } e. E -> ( ( { x , y } e. E /\ { y , A } e. E ) -> ( ( x e. V /\ y e. V ) -> E. b e. V E. c e. V ( { A , b } e. E /\ { b , c } e. E /\ { c , A } e. E ) ) ) )
76 59 75 syl5bi 
 |-  ( { A , x } e. E -> ( ( { A , y } e. E /\ { y , x } e. E ) -> ( ( x e. V /\ y e. V ) -> E. b e. V E. c e. V ( { A , b } e. E /\ { b , c } e. E /\ { c , A } e. E ) ) ) )
77 76 adantr 
 |-  ( ( { A , x } e. E /\ { x , C } e. E ) -> ( ( { A , y } e. E /\ { y , x } e. E ) -> ( ( x e. V /\ y e. V ) -> E. b e. V E. c e. V ( { A , b } e. E /\ { b , c } e. E /\ { c , A } e. E ) ) ) )
78 77 com13 
 |-  ( ( x e. V /\ y e. V ) -> ( ( { A , y } e. E /\ { y , x } e. E ) -> ( ( { A , x } e. E /\ { x , C } e. E ) -> E. b e. V E. c e. V ( { A , b } e. E /\ { b , c } e. E /\ { c , A } e. E ) ) ) )
79 78 rexlimdva 
 |-  ( x e. V -> ( E. y e. V ( { A , y } e. E /\ { y , x } e. E ) -> ( ( { A , x } e. E /\ { x , C } e. E ) -> E. b e. V E. c e. V ( { A , b } e. E /\ { b , c } e. E /\ { c , A } e. E ) ) ) )
80 79 com13 
 |-  ( ( { A , x } e. E /\ { x , C } e. E ) -> ( E. y e. V ( { A , y } e. E /\ { y , x } e. E ) -> ( x e. V -> E. b e. V E. c e. V ( { A , b } e. E /\ { b , c } e. E /\ { c , A } e. E ) ) ) )
81 54 80 syl9 
 |-  ( ( ( A =/= x /\ A e. V ) /\ x e. V ) -> ( ( { A , x } e. E /\ { x , C } e. E ) -> ( A. u e. V A. v e. ( V \ { u } ) E. y e. V ( { u , y } e. E /\ { y , v } e. E ) -> ( x e. V -> E. b e. V E. c e. V ( { A , b } e. E /\ { b , c } e. E /\ { c , A } e. E ) ) ) ) )
82 81 exp31 
 |-  ( A =/= x -> ( A e. V -> ( x e. V -> ( ( { A , x } e. E /\ { x , C } e. E ) -> ( A. u e. V A. v e. ( V \ { u } ) E. y e. V ( { u , y } e. E /\ { y , v } e. E ) -> ( x e. V -> E. b e. V E. c e. V ( { A , b } e. E /\ { b , c } e. E /\ { c , A } e. E ) ) ) ) ) ) )
83 82 com24 
 |-  ( A =/= x -> ( ( { A , x } e. E /\ { x , C } e. E ) -> ( x e. V -> ( A e. V -> ( A. u e. V A. v e. ( V \ { u } ) E. y e. V ( { u , y } e. E /\ { y , v } e. E ) -> ( x e. V -> E. b e. V E. c e. V ( { A , b } e. E /\ { b , c } e. E /\ { c , A } e. E ) ) ) ) ) ) )
84 83 adantr 
 |-  ( ( A =/= x /\ x =/= C ) -> ( ( { A , x } e. E /\ { x , C } e. E ) -> ( x e. V -> ( A e. V -> ( A. u e. V A. v e. ( V \ { u } ) E. y e. V ( { u , y } e. E /\ { y , v } e. E ) -> ( x e. V -> E. b e. V E. c e. V ( { A , b } e. E /\ { b , c } e. E /\ { c , A } e. E ) ) ) ) ) ) )
85 84 impcom 
 |-  ( ( ( { A , x } e. E /\ { x , C } e. E ) /\ ( A =/= x /\ x =/= C ) ) -> ( x e. V -> ( A e. V -> ( A. u e. V A. v e. ( V \ { u } ) E. y e. V ( { u , y } e. E /\ { y , v } e. E ) -> ( x e. V -> E. b e. V E. c e. V ( { A , b } e. E /\ { b , c } e. E /\ { c , A } e. E ) ) ) ) ) )
86 85 com15 
 |-  ( x e. V -> ( x e. V -> ( A e. V -> ( A. u e. V A. v e. ( V \ { u } ) E. y e. V ( { u , y } e. E /\ { y , v } e. E ) -> ( ( ( { A , x } e. E /\ { x , C } e. E ) /\ ( A =/= x /\ x =/= C ) ) -> E. b e. V E. c e. V ( { A , b } e. E /\ { b , c } e. E /\ { c , A } e. E ) ) ) ) ) )
87 86 pm2.43i 
 |-  ( x e. V -> ( A e. V -> ( A. u e. V A. v e. ( V \ { u } ) E. y e. V ( { u , y } e. E /\ { y , v } e. E ) -> ( ( ( { A , x } e. E /\ { x , C } e. E ) /\ ( A =/= x /\ x =/= C ) ) -> E. b e. V E. c e. V ( { A , b } e. E /\ { b , c } e. E /\ { c , A } e. E ) ) ) ) )
88 87 com12 
 |-  ( A e. V -> ( x e. V -> ( A. u e. V A. v e. ( V \ { u } ) E. y e. V ( { u , y } e. E /\ { y , v } e. E ) -> ( ( ( { A , x } e. E /\ { x , C } e. E ) /\ ( A =/= x /\ x =/= C ) ) -> E. b e. V E. c e. V ( { A , b } e. E /\ { b , c } e. E /\ { c , A } e. E ) ) ) ) )
89 88 ad2antrr 
 |-  ( ( ( A e. V /\ C e. V ) /\ A =/= C ) -> ( x e. V -> ( A. u e. V A. v e. ( V \ { u } ) E. y e. V ( { u , y } e. E /\ { y , v } e. E ) -> ( ( ( { A , x } e. E /\ { x , C } e. E ) /\ ( A =/= x /\ x =/= C ) ) -> E. b e. V E. c e. V ( { A , b } e. E /\ { b , c } e. E /\ { c , A } e. E ) ) ) ) )
90 89 com4t 
 |-  ( A. u e. V A. v e. ( V \ { u } ) E. y e. V ( { u , y } e. E /\ { y , v } e. E ) -> ( ( ( { A , x } e. E /\ { x , C } e. E ) /\ ( A =/= x /\ x =/= C ) ) -> ( ( ( A e. V /\ C e. V ) /\ A =/= C ) -> ( x e. V -> E. b e. V E. c e. V ( { A , b } e. E /\ { b , c } e. E /\ { c , A } e. E ) ) ) ) )
91 32 90 syl 
 |-  ( G e. FriendGraph -> ( ( ( { A , x } e. E /\ { x , C } e. E ) /\ ( A =/= x /\ x =/= C ) ) -> ( ( ( A e. V /\ C e. V ) /\ A =/= C ) -> ( x e. V -> E. b e. V E. c e. V ( { A , b } e. E /\ { b , c } e. E /\ { c , A } e. E ) ) ) ) )
92 91 com14 
 |-  ( x e. V -> ( ( ( { A , x } e. E /\ { x , C } e. E ) /\ ( A =/= x /\ x =/= C ) ) -> ( ( ( A e. V /\ C e. V ) /\ A =/= C ) -> ( G e. FriendGraph -> E. b e. V E. c e. V ( { A , b } e. E /\ { b , c } e. E /\ { c , A } e. E ) ) ) ) )
93 92 rexlimiv 
 |-  ( E. x e. V ( ( { A , x } e. E /\ { x , C } e. E ) /\ ( A =/= x /\ x =/= C ) ) -> ( ( ( A e. V /\ C e. V ) /\ A =/= C ) -> ( G e. FriendGraph -> E. b e. V E. c e. V ( { A , b } e. E /\ { b , c } e. E /\ { c , A } e. E ) ) ) )
94 31 93 syl6 
 |-  ( ( ( A e. V /\ C e. V ) /\ A =/= C ) -> ( A. a e. V A. z e. ( V \ { a } ) E. x e. V ( ( { a , x } e. E /\ { x , z } e. E ) /\ ( a =/= x /\ x =/= z ) ) -> ( ( ( A e. V /\ C e. V ) /\ A =/= C ) -> ( G e. FriendGraph -> E. b e. V E. c e. V ( { A , b } e. E /\ { b , c } e. E /\ { c , A } e. E ) ) ) ) )
95 94 pm2.43a 
 |-  ( ( ( A e. V /\ C e. V ) /\ A =/= C ) -> ( A. a e. V A. z e. ( V \ { a } ) E. x e. V ( ( { a , x } e. E /\ { x , z } e. E ) /\ ( a =/= x /\ x =/= z ) ) -> ( G e. FriendGraph -> E. b e. V E. c e. V ( { A , b } e. E /\ { b , c } e. E /\ { c , A } e. E ) ) ) )
96 95 ex 
 |-  ( ( A e. V /\ C e. V ) -> ( A =/= C -> ( A. a e. V A. z e. ( V \ { a } ) E. x e. V ( ( { a , x } e. E /\ { x , z } e. E ) /\ ( a =/= x /\ x =/= z ) ) -> ( G e. FriendGraph -> E. b e. V E. c e. V ( { A , b } e. E /\ { b , c } e. E /\ { c , A } e. E ) ) ) ) )
97 96 com4t 
 |-  ( A. a e. V A. z e. ( V \ { a } ) E. x e. V ( ( { a , x } e. E /\ { x , z } e. E ) /\ ( a =/= x /\ x =/= z ) ) -> ( G e. FriendGraph -> ( ( A e. V /\ C e. V ) -> ( A =/= C -> E. b e. V E. c e. V ( { A , b } e. E /\ { b , c } e. E /\ { c , A } e. E ) ) ) ) )
98 3 97 mpcom 
 |-  ( G e. FriendGraph -> ( ( A e. V /\ C e. V ) -> ( A =/= C -> E. b e. V E. c e. V ( { A , b } e. E /\ { b , c } e. E /\ { c , A } e. E ) ) ) )
99 98 3imp 
 |-  ( ( G e. FriendGraph /\ ( A e. V /\ C e. V ) /\ A =/= C ) -> E. b e. V E. c e. V ( { A , b } e. E /\ { b , c } e. E /\ { c , A } e. E ) )