Metamath Proof Explorer

Theorem frgrwopreglem5

Description: Lemma 5 for frgrwopreg . If A as well as B contain at least two vertices, there is a 4-cycle in a friendship graph. This corresponds to statement 6 in Huneke p. 2: "... otherwise, there are two different vertices in A, and they have two common neighbors in B, ...". (Contributed by Alexander van der Vekens, 31-Dec-2017) (Proof shortened by AV, 5-Feb-2022)

Ref Expression
Hypotheses frgrwopreg.v 
|- V = ( Vtx ` G )
frgrwopreg.d 
|- D = ( VtxDeg ` G )
frgrwopreg.a 
|- A = { x e. V | ( D ` x ) = K }
frgrwopreg.b 
|- B = ( V \ A )
frgrwopreg.e 
|- E = ( Edg ` G )
Assertion frgrwopreglem5 
|- ( ( G e. FriendGraph /\ 1 < ( # ` A ) /\ 1 < ( # ` B ) ) -> E. a e. A E. x e. A E. b e. B E. y e. B ( ( a =/= x /\ b =/= y ) /\ ( { a , b } e. E /\ { b , x } e. E ) /\ ( { x , y } e. E /\ { y , a } e. E ) ) )

Proof

Step Hyp Ref Expression
1 frgrwopreg.v 
 |-  V = ( Vtx ` G )
2 frgrwopreg.d 
 |-  D = ( VtxDeg ` G )
3 frgrwopreg.a 
 |-  A = { x e. V | ( D ` x ) = K }
4 frgrwopreg.b 
 |-  B = ( V \ A )
5 frgrwopreg.e 
 |-  E = ( Edg ` G )
6 simpllr 
 |-  ( ( ( ( G e. FriendGraph /\ a =/= x ) /\ ( a e. A /\ x e. A ) ) /\ ( b e. B /\ y e. B ) ) -> a =/= x )
7 6 anim1i 
 |-  ( ( ( ( ( G e. FriendGraph /\ a =/= x ) /\ ( a e. A /\ x e. A ) ) /\ ( b e. B /\ y e. B ) ) /\ b =/= y ) -> ( a =/= x /\ b =/= y ) )
8 simplll 
 |-  ( ( ( ( G e. FriendGraph /\ a =/= x ) /\ ( a e. A /\ x e. A ) ) /\ ( b e. B /\ y e. B ) ) -> G e. FriendGraph )
9 fveqeq2 
 |-  ( x = a -> ( ( D ` x ) = K <-> ( D ` a ) = K ) )
10 9 3 elrab2 
 |-  ( a e. A <-> ( a e. V /\ ( D ` a ) = K ) )
11 10 simplbi 
 |-  ( a e. A -> a e. V )
12 rabidim1 
 |-  ( x e. { x e. V | ( D ` x ) = K } -> x e. V )
13 12 3 eleq2s 
 |-  ( x e. A -> x e. V )
14 11 13 anim12i 
 |-  ( ( a e. A /\ x e. A ) -> ( a e. V /\ x e. V ) )
15 14 adantl 
 |-  ( ( ( G e. FriendGraph /\ a =/= x ) /\ ( a e. A /\ x e. A ) ) -> ( a e. V /\ x e. V ) )
16 eldifi 
 |-  ( b e. ( V \ A ) -> b e. V )
17 16 4 eleq2s 
 |-  ( b e. B -> b e. V )
18 eldifi 
 |-  ( y e. ( V \ A ) -> y e. V )
19 18 4 eleq2s 
 |-  ( y e. B -> y e. V )
20 17 19 anim12i 
 |-  ( ( b e. B /\ y e. B ) -> ( b e. V /\ y e. V ) )
21 15 20 anim12i 
 |-  ( ( ( ( G e. FriendGraph /\ a =/= x ) /\ ( a e. A /\ x e. A ) ) /\ ( b e. B /\ y e. B ) ) -> ( ( a e. V /\ x e. V ) /\ ( b e. V /\ y e. V ) ) )
22 1 2 3 4 5 frgrwopreglem5lem 
 |-  ( ( ( a e. A /\ x e. A ) /\ ( b e. B /\ y e. B ) ) -> ( ( D ` a ) = ( D ` x ) /\ ( D ` a ) =/= ( D ` b ) /\ ( D ` x ) =/= ( D ` y ) ) )
23 22 adantll 
 |-  ( ( ( ( G e. FriendGraph /\ a =/= x ) /\ ( a e. A /\ x e. A ) ) /\ ( b e. B /\ y e. B ) ) -> ( ( D ` a ) = ( D ` x ) /\ ( D ` a ) =/= ( D ` b ) /\ ( D ` x ) =/= ( D ` y ) ) )
24 8 21 23 3jca 
 |-  ( ( ( ( G e. FriendGraph /\ a =/= x ) /\ ( a e. A /\ x e. A ) ) /\ ( b e. B /\ y e. B ) ) -> ( G e. FriendGraph /\ ( ( a e. V /\ x e. V ) /\ ( b e. V /\ y e. V ) ) /\ ( ( D ` a ) = ( D ` x ) /\ ( D ` a ) =/= ( D ` b ) /\ ( D ` x ) =/= ( D ` y ) ) ) )
25 24 adantr 
 |-  ( ( ( ( ( G e. FriendGraph /\ a =/= x ) /\ ( a e. A /\ x e. A ) ) /\ ( b e. B /\ y e. B ) ) /\ b =/= y ) -> ( G e. FriendGraph /\ ( ( a e. V /\ x e. V ) /\ ( b e. V /\ y e. V ) ) /\ ( ( D ` a ) = ( D ` x ) /\ ( D ` a ) =/= ( D ` b ) /\ ( D ` x ) =/= ( D ` y ) ) ) )
26 1 2 5 frgrwopreglem5a 
 |-  ( ( G e. FriendGraph /\ ( ( a e. V /\ x e. V ) /\ ( b e. V /\ y e. V ) ) /\ ( ( D ` a ) = ( D ` x ) /\ ( D ` a ) =/= ( D ` b ) /\ ( D ` x ) =/= ( D ` y ) ) ) -> ( ( { a , b } e. E /\ { b , x } e. E ) /\ ( { x , y } e. E /\ { y , a } e. E ) ) )
27 25 26 syl 
 |-  ( ( ( ( ( G e. FriendGraph /\ a =/= x ) /\ ( a e. A /\ x e. A ) ) /\ ( b e. B /\ y e. B ) ) /\ b =/= y ) -> ( ( { a , b } e. E /\ { b , x } e. E ) /\ ( { x , y } e. E /\ { y , a } e. E ) ) )
28 3anass 
 |-  ( ( ( a =/= x /\ b =/= y ) /\ ( { a , b } e. E /\ { b , x } e. E ) /\ ( { x , y } e. E /\ { y , a } e. E ) ) <-> ( ( a =/= x /\ b =/= y ) /\ ( ( { a , b } e. E /\ { b , x } e. E ) /\ ( { x , y } e. E /\ { y , a } e. E ) ) ) )
29 7 27 28 sylanbrc 
 |-  ( ( ( ( ( G e. FriendGraph /\ a =/= x ) /\ ( a e. A /\ x e. A ) ) /\ ( b e. B /\ y e. B ) ) /\ b =/= y ) -> ( ( a =/= x /\ b =/= y ) /\ ( { a , b } e. E /\ { b , x } e. E ) /\ ( { x , y } e. E /\ { y , a } e. E ) ) )
30 29 ex 
 |-  ( ( ( ( G e. FriendGraph /\ a =/= x ) /\ ( a e. A /\ x e. A ) ) /\ ( b e. B /\ y e. B ) ) -> ( b =/= y -> ( ( a =/= x /\ b =/= y ) /\ ( { a , b } e. E /\ { b , x } e. E ) /\ ( { x , y } e. E /\ { y , a } e. E ) ) ) )
31 30 reximdvva 
 |-  ( ( ( G e. FriendGraph /\ a =/= x ) /\ ( a e. A /\ x e. A ) ) -> ( E. b e. B E. y e. B b =/= y -> E. b e. B E. y e. B ( ( a =/= x /\ b =/= y ) /\ ( { a , b } e. E /\ { b , x } e. E ) /\ ( { x , y } e. E /\ { y , a } e. E ) ) ) )
32 31 exp31 
 |-  ( G e. FriendGraph -> ( a =/= x -> ( ( a e. A /\ x e. A ) -> ( E. b e. B E. y e. B b =/= y -> E. b e. B E. y e. B ( ( a =/= x /\ b =/= y ) /\ ( { a , b } e. E /\ { b , x } e. E ) /\ ( { x , y } e. E /\ { y , a } e. E ) ) ) ) ) )
33 32 com24 
 |-  ( G e. FriendGraph -> ( E. b e. B E. y e. B b =/= y -> ( ( a e. A /\ x e. A ) -> ( a =/= x -> E. b e. B E. y e. B ( ( a =/= x /\ b =/= y ) /\ ( { a , b } e. E /\ { b , x } e. E ) /\ ( { x , y } e. E /\ { y , a } e. E ) ) ) ) ) )
34 33 imp31 
 |-  ( ( ( G e. FriendGraph /\ E. b e. B E. y e. B b =/= y ) /\ ( a e. A /\ x e. A ) ) -> ( a =/= x -> E. b e. B E. y e. B ( ( a =/= x /\ b =/= y ) /\ ( { a , b } e. E /\ { b , x } e. E ) /\ ( { x , y } e. E /\ { y , a } e. E ) ) ) )
35 34 reximdvva 
 |-  ( ( G e. FriendGraph /\ E. b e. B E. y e. B b =/= y ) -> ( E. a e. A E. x e. A a =/= x -> E. a e. A E. x e. A E. b e. B E. y e. B ( ( a =/= x /\ b =/= y ) /\ ( { a , b } e. E /\ { b , x } e. E ) /\ ( { x , y } e. E /\ { y , a } e. E ) ) ) )
36 35 ex 
 |-  ( G e. FriendGraph -> ( E. b e. B E. y e. B b =/= y -> ( E. a e. A E. x e. A a =/= x -> E. a e. A E. x e. A E. b e. B E. y e. B ( ( a =/= x /\ b =/= y ) /\ ( { a , b } e. E /\ { b , x } e. E ) /\ ( { x , y } e. E /\ { y , a } e. E ) ) ) ) )
37 36 com13 
 |-  ( E. a e. A E. x e. A a =/= x -> ( E. b e. B E. y e. B b =/= y -> ( G e. FriendGraph -> E. a e. A E. x e. A E. b e. B E. y e. B ( ( a =/= x /\ b =/= y ) /\ ( { a , b } e. E /\ { b , x } e. E ) /\ ( { x , y } e. E /\ { y , a } e. E ) ) ) ) )
38 37 imp 
 |-  ( ( E. a e. A E. x e. A a =/= x /\ E. b e. B E. y e. B b =/= y ) -> ( G e. FriendGraph -> E. a e. A E. x e. A E. b e. B E. y e. B ( ( a =/= x /\ b =/= y ) /\ ( { a , b } e. E /\ { b , x } e. E ) /\ ( { x , y } e. E /\ { y , a } e. E ) ) ) )
39 1 2 3 4 frgrwopreglem1 
 |-  ( A e. _V /\ B e. _V )
40 hashgt12el 
 |-  ( ( A e. _V /\ 1 < ( # ` A ) ) -> E. a e. A E. x e. A a =/= x )
41 40 ex 
 |-  ( A e. _V -> ( 1 < ( # ` A ) -> E. a e. A E. x e. A a =/= x ) )
42 hashgt12el 
 |-  ( ( B e. _V /\ 1 < ( # ` B ) ) -> E. b e. B E. y e. B b =/= y )
43 42 ex 
 |-  ( B e. _V -> ( 1 < ( # ` B ) -> E. b e. B E. y e. B b =/= y ) )
44 41 43 im2anan9 
 |-  ( ( A e. _V /\ B e. _V ) -> ( ( 1 < ( # ` A ) /\ 1 < ( # ` B ) ) -> ( E. a e. A E. x e. A a =/= x /\ E. b e. B E. y e. B b =/= y ) ) )
45 39 44 ax-mp 
 |-  ( ( 1 < ( # ` A ) /\ 1 < ( # ` B ) ) -> ( E. a e. A E. x e. A a =/= x /\ E. b e. B E. y e. B b =/= y ) )
46 38 45 syl11 
 |-  ( G e. FriendGraph -> ( ( 1 < ( # ` A ) /\ 1 < ( # ` B ) ) -> E. a e. A E. x e. A E. b e. B E. y e. B ( ( a =/= x /\ b =/= y ) /\ ( { a , b } e. E /\ { b , x } e. E ) /\ ( { x , y } e. E /\ { y , a } e. E ) ) ) )
47 46 3impib 
 |-  ( ( G e. FriendGraph /\ 1 < ( # ` A ) /\ 1 < ( # ` B ) ) -> E. a e. A E. x e. A E. b e. B E. y e. B ( ( a =/= x /\ b =/= y ) /\ ( { a , b } e. E /\ { b , x } e. E ) /\ ( { x , y } e. E /\ { y , a } e. E ) ) )