Metamath Proof Explorer

Theorem frgrwopreglem4a

Description: In a friendship graph any two vertices with different degrees are connected. Alternate version of frgrwopreglem4 without a fixed degree and without using the sets A and B . (Contributed by Alexander van der Vekens, 30-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 frgrwopreglem4a 
|- ( ( G e. FriendGraph /\ ( X e. V /\ Y e. V ) /\ ( D ` X ) =/= ( D ` Y ) ) -> { X , Y } 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 fveq2 
 |-  ( X = Y -> ( D ` X ) = ( D ` Y ) )
5 4 a1i 
 |-  ( ( X e. V /\ Y e. V ) -> ( X = Y -> ( D ` X ) = ( D ` Y ) ) )
6 5 necon3d 
 |-  ( ( X e. V /\ Y e. V ) -> ( ( D ` X ) =/= ( D ` Y ) -> X =/= Y ) )
7 6 imp 
 |-  ( ( ( X e. V /\ Y e. V ) /\ ( D ` X ) =/= ( D ` Y ) ) -> X =/= Y )
8 7 3adant1 
 |-  ( ( G e. FriendGraph /\ ( X e. V /\ Y e. V ) /\ ( D ` X ) =/= ( D ` Y ) ) -> X =/= Y )
9 1 2 frgrncvvdeq 
 |-  ( G e. FriendGraph -> A. x e. V A. y e. ( V \ { x } ) ( y e/ ( G NeighbVtx x ) -> ( D ` x ) = ( D ` y ) ) )
10 oveq2 
 |-  ( x = X -> ( G NeighbVtx x ) = ( G NeighbVtx X ) )
11 neleq2 
 |-  ( ( G NeighbVtx x ) = ( G NeighbVtx X ) -> ( y e/ ( G NeighbVtx x ) <-> y e/ ( G NeighbVtx X ) ) )
12 10 11 syl 
 |-  ( x = X -> ( y e/ ( G NeighbVtx x ) <-> y e/ ( G NeighbVtx X ) ) )
13 fveqeq2 
 |-  ( x = X -> ( ( D ` x ) = ( D ` y ) <-> ( D ` X ) = ( D ` y ) ) )
14 12 13 imbi12d 
 |-  ( x = X -> ( ( y e/ ( G NeighbVtx x ) -> ( D ` x ) = ( D ` y ) ) <-> ( y e/ ( G NeighbVtx X ) -> ( D ` X ) = ( D ` y ) ) ) )
15 neleq1 
 |-  ( y = Y -> ( y e/ ( G NeighbVtx X ) <-> Y e/ ( G NeighbVtx X ) ) )
16 fveq2 
 |-  ( y = Y -> ( D ` y ) = ( D ` Y ) )
17 16 eqeq2d 
 |-  ( y = Y -> ( ( D ` X ) = ( D ` y ) <-> ( D ` X ) = ( D ` Y ) ) )
18 15 17 imbi12d 
 |-  ( y = Y -> ( ( y e/ ( G NeighbVtx X ) -> ( D ` X ) = ( D ` y ) ) <-> ( Y e/ ( G NeighbVtx X ) -> ( D ` X ) = ( D ` Y ) ) ) )
19 simpll 
 |-  ( ( ( X e. V /\ Y e. V ) /\ X =/= Y ) -> X e. V )
20 sneq 
 |-  ( x = X -> { x } = { X } )
21 20 difeq2d 
 |-  ( x = X -> ( V \ { x } ) = ( V \ { X } ) )
22 21 adantl 
 |-  ( ( ( ( X e. V /\ Y e. V ) /\ X =/= Y ) /\ x = X ) -> ( V \ { x } ) = ( V \ { X } ) )
23 simpr 
 |-  ( ( X e. V /\ Y e. V ) -> Y e. V )
24 necom 
 |-  ( X =/= Y <-> Y =/= X )
25 24 biimpi 
 |-  ( X =/= Y -> Y =/= X )
26 23 25 anim12i 
 |-  ( ( ( X e. V /\ Y e. V ) /\ X =/= Y ) -> ( Y e. V /\ Y =/= X ) )
27 eldifsn 
 |-  ( Y e. ( V \ { X } ) <-> ( Y e. V /\ Y =/= X ) )
28 26 27 sylibr 
 |-  ( ( ( X e. V /\ Y e. V ) /\ X =/= Y ) -> Y e. ( V \ { X } ) )
29 14 18 19 22 28 rspc2vd 
 |-  ( ( ( X e. V /\ Y e. V ) /\ X =/= Y ) -> ( A. x e. V A. y e. ( V \ { x } ) ( y e/ ( G NeighbVtx x ) -> ( D ` x ) = ( D ` y ) ) -> ( Y e/ ( G NeighbVtx X ) -> ( D ` X ) = ( D ` Y ) ) ) )
30 nnel 
 |-  ( -. Y e/ ( G NeighbVtx X ) <-> Y e. ( G NeighbVtx X ) )
31 nbgrsym 
 |-  ( Y e. ( G NeighbVtx X ) <-> X e. ( G NeighbVtx Y ) )
32 frgrusgr 
 |-  ( G e. FriendGraph -> G e. USGraph )
33 3 nbusgreledg 
 |-  ( G e. USGraph -> ( X e. ( G NeighbVtx Y ) <-> { X , Y } e. E ) )
34 32 33 syl 
 |-  ( G e. FriendGraph -> ( X e. ( G NeighbVtx Y ) <-> { X , Y } e. E ) )
35 34 biimpd 
 |-  ( G e. FriendGraph -> ( X e. ( G NeighbVtx Y ) -> { X , Y } e. E ) )
36 31 35 syl5bi 
 |-  ( G e. FriendGraph -> ( Y e. ( G NeighbVtx X ) -> { X , Y } e. E ) )
37 36 imp 
 |-  ( ( G e. FriendGraph /\ Y e. ( G NeighbVtx X ) ) -> { X , Y } e. E )
38 37 a1d 
 |-  ( ( G e. FriendGraph /\ Y e. ( G NeighbVtx X ) ) -> ( ( D ` X ) =/= ( D ` Y ) -> { X , Y } e. E ) )
39 38 expcom 
 |-  ( Y e. ( G NeighbVtx X ) -> ( G e. FriendGraph -> ( ( D ` X ) =/= ( D ` Y ) -> { X , Y } e. E ) ) )
40 39 a1d 
 |-  ( Y e. ( G NeighbVtx X ) -> ( ( ( X e. V /\ Y e. V ) /\ X =/= Y ) -> ( G e. FriendGraph -> ( ( D ` X ) =/= ( D ` Y ) -> { X , Y } e. E ) ) ) )
41 30 40 sylbi 
 |-  ( -. Y e/ ( G NeighbVtx X ) -> ( ( ( X e. V /\ Y e. V ) /\ X =/= Y ) -> ( G e. FriendGraph -> ( ( D ` X ) =/= ( D ` Y ) -> { X , Y } e. E ) ) ) )
42 eqneqall 
 |-  ( ( D ` X ) = ( D ` Y ) -> ( ( D ` X ) =/= ( D ` Y ) -> { X , Y } e. E ) )
43 42 2a1d 
 |-  ( ( D ` X ) = ( D ` Y ) -> ( ( ( X e. V /\ Y e. V ) /\ X =/= Y ) -> ( G e. FriendGraph -> ( ( D ` X ) =/= ( D ` Y ) -> { X , Y } e. E ) ) ) )
44 41 43 ja 
 |-  ( ( Y e/ ( G NeighbVtx X ) -> ( D ` X ) = ( D ` Y ) ) -> ( ( ( X e. V /\ Y e. V ) /\ X =/= Y ) -> ( G e. FriendGraph -> ( ( D ` X ) =/= ( D ` Y ) -> { X , Y } e. E ) ) ) )
45 44 com12 
 |-  ( ( ( X e. V /\ Y e. V ) /\ X =/= Y ) -> ( ( Y e/ ( G NeighbVtx X ) -> ( D ` X ) = ( D ` Y ) ) -> ( G e. FriendGraph -> ( ( D ` X ) =/= ( D ` Y ) -> { X , Y } e. E ) ) ) )
46 29 45 syld 
 |-  ( ( ( X e. V /\ Y e. V ) /\ X =/= Y ) -> ( A. x e. V A. y e. ( V \ { x } ) ( y e/ ( G NeighbVtx x ) -> ( D ` x ) = ( D ` y ) ) -> ( G e. FriendGraph -> ( ( D ` X ) =/= ( D ` Y ) -> { X , Y } e. E ) ) ) )
47 46 com3l 
 |-  ( A. x e. V A. y e. ( V \ { x } ) ( y e/ ( G NeighbVtx x ) -> ( D ` x ) = ( D ` y ) ) -> ( G e. FriendGraph -> ( ( ( X e. V /\ Y e. V ) /\ X =/= Y ) -> ( ( D ` X ) =/= ( D ` Y ) -> { X , Y } e. E ) ) ) )
48 9 47 mpcom 
 |-  ( G e. FriendGraph -> ( ( ( X e. V /\ Y e. V ) /\ X =/= Y ) -> ( ( D ` X ) =/= ( D ` Y ) -> { X , Y } e. E ) ) )
49 48 expd 
 |-  ( G e. FriendGraph -> ( ( X e. V /\ Y e. V ) -> ( X =/= Y -> ( ( D ` X ) =/= ( D ` Y ) -> { X , Y } e. E ) ) ) )
50 49 com34 
 |-  ( G e. FriendGraph -> ( ( X e. V /\ Y e. V ) -> ( ( D ` X ) =/= ( D ` Y ) -> ( X =/= Y -> { X , Y } e. E ) ) ) )
51 50 3imp 
 |-  ( ( G e. FriendGraph /\ ( X e. V /\ Y e. V ) /\ ( D ` X ) =/= ( D ` Y ) ) -> ( X =/= Y -> { X , Y } e. E ) )
52 8 51 mpd 
 |-  ( ( G e. FriendGraph /\ ( X e. V /\ Y e. V ) /\ ( D ` X ) =/= ( D ` Y ) ) -> { X , Y } e. E )