Metamath Proof Explorer

Theorem vdgn1frgrv2

Description: Any vertex in a friendship graph does not have degree 1, see remark 2 in MertziosUnger p. 153 (after Proposition 1): "... no node v of it [a friendship graph] may have deg(v) = 1.". (Contributed by Alexander van der Vekens, 10-Dec-2017) (Revised by AV, 4-Apr-2021)

Ref Expression
Hypothesis vdn1frgrv2.v 
|- V = ( Vtx ` G )
Assertion vdgn1frgrv2 
|- ( ( G e. FriendGraph /\ N e. V ) -> ( 1 < ( # ` V ) -> ( ( VtxDeg ` G ) ` N ) =/= 1 ) )

Proof

Step Hyp Ref Expression
1 vdn1frgrv2.v 
 |-  V = ( Vtx ` G )
2 frgrusgr 
 |-  ( G e. FriendGraph -> G e. USGraph )
3 2 anim1i 
 |-  ( ( G e. FriendGraph /\ N e. V ) -> ( G e. USGraph /\ N e. V ) )
4 3 adantr 
 |-  ( ( ( G e. FriendGraph /\ N e. V ) /\ 1 < ( # ` V ) ) -> ( G e. USGraph /\ N e. V ) )
5 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
6 eqid 
 |-  dom ( iEdg ` G ) = dom ( iEdg ` G )
7 eqid 
 |-  ( VtxDeg ` G ) = ( VtxDeg ` G )
8 1 5 6 7 vtxdusgrval 
 |-  ( ( G e. USGraph /\ N e. V ) -> ( ( VtxDeg ` G ) ` N ) = ( # ` { x e. dom ( iEdg ` G ) | N e. ( ( iEdg ` G ) ` x ) } ) )
9 4 8 syl 
 |-  ( ( ( G e. FriendGraph /\ N e. V ) /\ 1 < ( # ` V ) ) -> ( ( VtxDeg ` G ) ` N ) = ( # ` { x e. dom ( iEdg ` G ) | N e. ( ( iEdg ` G ) ` x ) } ) )
10 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
11 1 10 3cyclfrgrrn2 
 |-  ( ( G e. FriendGraph /\ 1 < ( # ` V ) ) -> A. a e. V E. b e. V E. c e. V ( b =/= c /\ ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) /\ { c , a } e. ( Edg ` G ) ) ) )
12 11 adantlr 
 |-  ( ( ( G e. FriendGraph /\ N e. V ) /\ 1 < ( # ` V ) ) -> A. a e. V E. b e. V E. c e. V ( b =/= c /\ ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) /\ { c , a } e. ( Edg ` G ) ) ) )
13 preq1 
 |-  ( a = N -> { a , b } = { N , b } )
14 13 eleq1d 
 |-  ( a = N -> ( { a , b } e. ( Edg ` G ) <-> { N , b } e. ( Edg ` G ) ) )
15 preq2 
 |-  ( a = N -> { c , a } = { c , N } )
16 15 eleq1d 
 |-  ( a = N -> ( { c , a } e. ( Edg ` G ) <-> { c , N } e. ( Edg ` G ) ) )
17 14 16 3anbi13d 
 |-  ( a = N -> ( ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) /\ { c , a } e. ( Edg ` G ) ) <-> ( { N , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) /\ { c , N } e. ( Edg ` G ) ) ) )
18 17 anbi2d 
 |-  ( a = N -> ( ( b =/= c /\ ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) /\ { c , a } e. ( Edg ` G ) ) ) <-> ( b =/= c /\ ( { N , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) /\ { c , N } e. ( Edg ` G ) ) ) ) )
19 18 2rexbidv 
 |-  ( a = N -> ( E. b e. V E. c e. V ( b =/= c /\ ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) /\ { c , a } e. ( Edg ` G ) ) ) <-> E. b e. V E. c e. V ( b =/= c /\ ( { N , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) /\ { c , N } e. ( Edg ` G ) ) ) ) )
20 19 rspcva 
 |-  ( ( N e. V /\ A. a e. V E. b e. V E. c e. V ( b =/= c /\ ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) /\ { c , a } e. ( Edg ` G ) ) ) ) -> E. b e. V E. c e. V ( b =/= c /\ ( { N , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) /\ { c , N } e. ( Edg ` G ) ) ) )
21 2 adantl 
 |-  ( ( ( ( b =/= c /\ ( { N , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) /\ { c , N } e. ( Edg ` G ) ) ) /\ N e. V ) /\ G e. FriendGraph ) -> G e. USGraph )
22 simplll 
 |-  ( ( ( ( b =/= c /\ ( { N , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) /\ { c , N } e. ( Edg ` G ) ) ) /\ N e. V ) /\ G e. FriendGraph ) -> b =/= c )
23 3simpb 
 |-  ( ( { N , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) /\ { c , N } e. ( Edg ` G ) ) -> ( { N , b } e. ( Edg ` G ) /\ { c , N } e. ( Edg ` G ) ) )
24 23 ad3antlr 
 |-  ( ( ( ( b =/= c /\ ( { N , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) /\ { c , N } e. ( Edg ` G ) ) ) /\ N e. V ) /\ G e. FriendGraph ) -> ( { N , b } e. ( Edg ` G ) /\ { c , N } e. ( Edg ` G ) ) )
25 5 10 usgr2edg1 
 |-  ( ( ( G e. USGraph /\ b =/= c ) /\ ( { N , b } e. ( Edg ` G ) /\ { c , N } e. ( Edg ` G ) ) ) -> -. E! x e. dom ( iEdg ` G ) N e. ( ( iEdg ` G ) ` x ) )
26 21 22 24 25 syl21anc 
 |-  ( ( ( ( b =/= c /\ ( { N , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) /\ { c , N } e. ( Edg ` G ) ) ) /\ N e. V ) /\ G e. FriendGraph ) -> -. E! x e. dom ( iEdg ` G ) N e. ( ( iEdg ` G ) ` x ) )
27 26 a1d 
 |-  ( ( ( ( b =/= c /\ ( { N , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) /\ { c , N } e. ( Edg ` G ) ) ) /\ N e. V ) /\ G e. FriendGraph ) -> ( 1 < ( # ` V ) -> -. E! x e. dom ( iEdg ` G ) N e. ( ( iEdg ` G ) ` x ) ) )
28 27 ex 
 |-  ( ( ( b =/= c /\ ( { N , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) /\ { c , N } e. ( Edg ` G ) ) ) /\ N e. V ) -> ( G e. FriendGraph -> ( 1 < ( # ` V ) -> -. E! x e. dom ( iEdg ` G ) N e. ( ( iEdg ` G ) ` x ) ) ) )
29 28 ex 
 |-  ( ( b =/= c /\ ( { N , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) /\ { c , N } e. ( Edg ` G ) ) ) -> ( N e. V -> ( G e. FriendGraph -> ( 1 < ( # ` V ) -> -. E! x e. dom ( iEdg ` G ) N e. ( ( iEdg ` G ) ` x ) ) ) ) )
30 29 a1i 
 |-  ( ( b e. V /\ c e. V ) -> ( ( b =/= c /\ ( { N , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) /\ { c , N } e. ( Edg ` G ) ) ) -> ( N e. V -> ( G e. FriendGraph -> ( 1 < ( # ` V ) -> -. E! x e. dom ( iEdg ` G ) N e. ( ( iEdg ` G ) ` x ) ) ) ) ) )
31 30 rexlimivv 
 |-  ( E. b e. V E. c e. V ( b =/= c /\ ( { N , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) /\ { c , N } e. ( Edg ` G ) ) ) -> ( N e. V -> ( G e. FriendGraph -> ( 1 < ( # ` V ) -> -. E! x e. dom ( iEdg ` G ) N e. ( ( iEdg ` G ) ` x ) ) ) ) )
32 20 31 syl 
 |-  ( ( N e. V /\ A. a e. V E. b e. V E. c e. V ( b =/= c /\ ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) /\ { c , a } e. ( Edg ` G ) ) ) ) -> ( N e. V -> ( G e. FriendGraph -> ( 1 < ( # ` V ) -> -. E! x e. dom ( iEdg ` G ) N e. ( ( iEdg ` G ) ` x ) ) ) ) )
33 32 ex 
 |-  ( N e. V -> ( A. a e. V E. b e. V E. c e. V ( b =/= c /\ ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) /\ { c , a } e. ( Edg ` G ) ) ) -> ( N e. V -> ( G e. FriendGraph -> ( 1 < ( # ` V ) -> -. E! x e. dom ( iEdg ` G ) N e. ( ( iEdg ` G ) ` x ) ) ) ) ) )
34 33 pm2.43a 
 |-  ( N e. V -> ( A. a e. V E. b e. V E. c e. V ( b =/= c /\ ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) /\ { c , a } e. ( Edg ` G ) ) ) -> ( G e. FriendGraph -> ( 1 < ( # ` V ) -> -. E! x e. dom ( iEdg ` G ) N e. ( ( iEdg ` G ) ` x ) ) ) ) )
35 34 com24 
 |-  ( N e. V -> ( 1 < ( # ` V ) -> ( G e. FriendGraph -> ( A. a e. V E. b e. V E. c e. V ( b =/= c /\ ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) /\ { c , a } e. ( Edg ` G ) ) ) -> -. E! x e. dom ( iEdg ` G ) N e. ( ( iEdg ` G ) ` x ) ) ) ) )
36 35 com3r 
 |-  ( G e. FriendGraph -> ( N e. V -> ( 1 < ( # ` V ) -> ( A. a e. V E. b e. V E. c e. V ( b =/= c /\ ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) /\ { c , a } e. ( Edg ` G ) ) ) -> -. E! x e. dom ( iEdg ` G ) N e. ( ( iEdg ` G ) ` x ) ) ) ) )
37 36 imp31 
 |-  ( ( ( G e. FriendGraph /\ N e. V ) /\ 1 < ( # ` V ) ) -> ( A. a e. V E. b e. V E. c e. V ( b =/= c /\ ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) /\ { c , a } e. ( Edg ` G ) ) ) -> -. E! x e. dom ( iEdg ` G ) N e. ( ( iEdg ` G ) ` x ) ) )
38 12 37 mpd 
 |-  ( ( ( G e. FriendGraph /\ N e. V ) /\ 1 < ( # ` V ) ) -> -. E! x e. dom ( iEdg ` G ) N e. ( ( iEdg ` G ) ` x ) )
39 fvex 
 |-  ( iEdg ` G ) e. _V
40 39 dmex 
 |-  dom ( iEdg ` G ) e. _V
41 40 a1i 
 |-  ( ( ( G e. FriendGraph /\ N e. V ) /\ 1 < ( # ` V ) ) -> dom ( iEdg ` G ) e. _V )
42 rabexg 
 |-  ( dom ( iEdg ` G ) e. _V -> { x e. dom ( iEdg ` G ) | N e. ( ( iEdg ` G ) ` x ) } e. _V )
43 hash1snb 
 |-  ( { x e. dom ( iEdg ` G ) | N e. ( ( iEdg ` G ) ` x ) } e. _V -> ( ( # ` { x e. dom ( iEdg ` G ) | N e. ( ( iEdg ` G ) ` x ) } ) = 1 <-> E. i { x e. dom ( iEdg ` G ) | N e. ( ( iEdg ` G ) ` x ) } = { i } ) )
44 41 42 43 3syl 
 |-  ( ( ( G e. FriendGraph /\ N e. V ) /\ 1 < ( # ` V ) ) -> ( ( # ` { x e. dom ( iEdg ` G ) | N e. ( ( iEdg ` G ) ` x ) } ) = 1 <-> E. i { x e. dom ( iEdg ` G ) | N e. ( ( iEdg ` G ) ` x ) } = { i } ) )
45 reusn 
 |-  ( E! x e. dom ( iEdg ` G ) N e. ( ( iEdg ` G ) ` x ) <-> E. i { x e. dom ( iEdg ` G ) | N e. ( ( iEdg ` G ) ` x ) } = { i } )
46 44 45 bitr4di 
 |-  ( ( ( G e. FriendGraph /\ N e. V ) /\ 1 < ( # ` V ) ) -> ( ( # ` { x e. dom ( iEdg ` G ) | N e. ( ( iEdg ` G ) ` x ) } ) = 1 <-> E! x e. dom ( iEdg ` G ) N e. ( ( iEdg ` G ) ` x ) ) )
47 46 necon3abid 
 |-  ( ( ( G e. FriendGraph /\ N e. V ) /\ 1 < ( # ` V ) ) -> ( ( # ` { x e. dom ( iEdg ` G ) | N e. ( ( iEdg ` G ) ` x ) } ) =/= 1 <-> -. E! x e. dom ( iEdg ` G ) N e. ( ( iEdg ` G ) ` x ) ) )
48 38 47 mpbird 
 |-  ( ( ( G e. FriendGraph /\ N e. V ) /\ 1 < ( # ` V ) ) -> ( # ` { x e. dom ( iEdg ` G ) | N e. ( ( iEdg ` G ) ` x ) } ) =/= 1 )
49 9 48 eqnetrd 
 |-  ( ( ( G e. FriendGraph /\ N e. V ) /\ 1 < ( # ` V ) ) -> ( ( VtxDeg ` G ) ` N ) =/= 1 )
50 49 ex 
 |-  ( ( G e. FriendGraph /\ N e. V ) -> ( 1 < ( # ` V ) -> ( ( VtxDeg ` G ) ` N ) =/= 1 ) )