Metamath Proof Explorer

Theorem frgrwopreglem5a

Description: If a friendship graph has two vertices with the same degree and two other vertices with different degrees, then there is a 4-cycle in the graph. Alternate version of frgrwopreglem5 without a fixed degree and without using the sets A and B . (Contributed by Alexander van der Vekens, 31-Dec-2017) (Revised by AV, 4-Feb-2022)

Ref Expression
Hypotheses frgrncvvdeq.v 
|- V = ( Vtx ` G )
frgrncvvdeq.d 
|- D = ( VtxDeg ` G )
frgrwopreglem4a.e 
|- E = ( Edg ` G )
Assertion 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 ) ) )

Proof

Step Hyp Ref Expression
1 frgrncvvdeq.v 
 |-  V = ( Vtx ` G )
2 frgrncvvdeq.d 
 |-  D = ( VtxDeg ` G )
3 frgrwopreglem4a.e 
 |-  E = ( Edg ` G )
4 id 
 |-  ( G e. FriendGraph -> G e. FriendGraph )
5 simpl 
 |-  ( ( A e. V /\ X e. V ) -> A e. V )
6 simpl 
 |-  ( ( B e. V /\ Y e. V ) -> B e. V )
7 5 6 anim12i 
 |-  ( ( ( A e. V /\ X e. V ) /\ ( B e. V /\ Y e. V ) ) -> ( A e. V /\ B e. V ) )
8 simp2 
 |-  ( ( ( D ` A ) = ( D ` X ) /\ ( D ` A ) =/= ( D ` B ) /\ ( D ` X ) =/= ( D ` Y ) ) -> ( D ` A ) =/= ( D ` B ) )
9 1 2 3 frgrwopreglem4a 
 |-  ( ( G e. FriendGraph /\ ( A e. V /\ B e. V ) /\ ( D ` A ) =/= ( D ` B ) ) -> { A , B } e. E )
10 4 7 8 9 syl3an 
 |-  ( ( 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 )
11 simpr 
 |-  ( ( A e. V /\ X e. V ) -> X e. V )
12 11 6 anim12ci 
 |-  ( ( ( A e. V /\ X e. V ) /\ ( B e. V /\ Y e. V ) ) -> ( B e. V /\ X e. V ) )
13 pm13.18 
 |-  ( ( ( D ` A ) = ( D ` X ) /\ ( D ` A ) =/= ( D ` B ) ) -> ( D ` X ) =/= ( D ` B ) )
14 13 3adant3 
 |-  ( ( ( D ` A ) = ( D ` X ) /\ ( D ` A ) =/= ( D ` B ) /\ ( D ` X ) =/= ( D ` Y ) ) -> ( D ` X ) =/= ( D ` B ) )
15 14 necomd 
 |-  ( ( ( D ` A ) = ( D ` X ) /\ ( D ` A ) =/= ( D ` B ) /\ ( D ` X ) =/= ( D ` Y ) ) -> ( D ` B ) =/= ( D ` X ) )
16 1 2 3 frgrwopreglem4a 
 |-  ( ( G e. FriendGraph /\ ( B e. V /\ X e. V ) /\ ( D ` B ) =/= ( D ` X ) ) -> { B , X } e. E )
17 4 12 15 16 syl3an 
 |-  ( ( 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 ) ) ) -> { B , X } e. E )
18 simpr 
 |-  ( ( B e. V /\ Y e. V ) -> Y e. V )
19 11 18 anim12i 
 |-  ( ( ( A e. V /\ X e. V ) /\ ( B e. V /\ Y e. V ) ) -> ( X e. V /\ Y e. V ) )
20 simp3 
 |-  ( ( ( D ` A ) = ( D ` X ) /\ ( D ` A ) =/= ( D ` B ) /\ ( D ` X ) =/= ( D ` Y ) ) -> ( D ` X ) =/= ( D ` Y ) )
21 1 2 3 frgrwopreglem4a 
 |-  ( ( G e. FriendGraph /\ ( X e. V /\ Y e. V ) /\ ( D ` X ) =/= ( D ` Y ) ) -> { X , Y } e. E )
22 4 19 20 21 syl3an 
 |-  ( ( 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 ) ) ) -> { X , Y } e. E )
23 5 18 anim12ci 
 |-  ( ( ( A e. V /\ X e. V ) /\ ( B e. V /\ Y e. V ) ) -> ( Y e. V /\ A e. V ) )
24 pm13.181 
 |-  ( ( ( D ` A ) = ( D ` X ) /\ ( D ` X ) =/= ( D ` Y ) ) -> ( D ` A ) =/= ( D ` Y ) )
25 24 3adant2 
 |-  ( ( ( D ` A ) = ( D ` X ) /\ ( D ` A ) =/= ( D ` B ) /\ ( D ` X ) =/= ( D ` Y ) ) -> ( D ` A ) =/= ( D ` Y ) )
26 25 necomd 
 |-  ( ( ( D ` A ) = ( D ` X ) /\ ( D ` A ) =/= ( D ` B ) /\ ( D ` X ) =/= ( D ` Y ) ) -> ( D ` Y ) =/= ( D ` A ) )
27 1 2 3 frgrwopreglem4a 
 |-  ( ( G e. FriendGraph /\ ( Y e. V /\ A e. V ) /\ ( D ` Y ) =/= ( D ` A ) ) -> { Y , A } e. E )
28 4 23 26 27 syl3an 
 |-  ( ( 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 ) ) ) -> { Y , A } e. E )
29 22 28 jca 
 |-  ( ( 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 ) ) ) -> ( { X , Y } e. E /\ { Y , A } e. E ) )
30 10 17 29 jca31 
 |-  ( ( 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 ) ) )