Metamath Proof Explorer

Theorem frgrregorufr0

Description: In a friendship graph there are either no vertices having degree K , or all vertices have degree K for any (nonnegative integer) K , unless there is a universal friend. This corresponds to claim 2 in Huneke p. 2: "... all vertices have degree k, unless there is a universal friend." (Contributed by Alexander van der Vekens, 1-Jan-2018) (Revised by AV, 11-May-2021) (Proof shortened by AV, 3-Jan-2022)

Ref Expression
Hypotheses frgrregorufr0.v 
|- V = ( Vtx ` G )
frgrregorufr0.e 
|- E = ( Edg ` G )
frgrregorufr0.d 
|- D = ( VtxDeg ` G )
Assertion frgrregorufr0 
|- ( G e. FriendGraph -> ( A. v e. V ( D ` v ) = K \/ A. v e. V ( D ` v ) =/= K \/ E. v e. V A. w e. ( V \ { v } ) { v , w } e. E ) )

Proof

Step Hyp Ref Expression
1 frgrregorufr0.v 
 |-  V = ( Vtx ` G )
2 frgrregorufr0.e 
 |-  E = ( Edg ` G )
3 frgrregorufr0.d 
 |-  D = ( VtxDeg ` G )
4 fveqeq2 
 |-  ( x = y -> ( ( D ` x ) = K <-> ( D ` y ) = K ) )
5 4 cbvrabv 
 |-  { x e. V | ( D ` x ) = K } = { y e. V | ( D ` y ) = K }
6 eqid 
 |-  ( V \ { x e. V | ( D ` x ) = K } ) = ( V \ { x e. V | ( D ` x ) = K } )
7 1 3 5 6 frgrwopreg 
 |-  ( G e. FriendGraph -> ( ( ( # ` { x e. V | ( D ` x ) = K } ) = 1 \/ { x e. V | ( D ` x ) = K } = (/) ) \/ ( ( # ` ( V \ { x e. V | ( D ` x ) = K } ) ) = 1 \/ ( V \ { x e. V | ( D ` x ) = K } ) = (/) ) ) )
8 1 3 5 6 2 frgrwopreg1 
 |-  ( ( G e. FriendGraph /\ ( # ` { x e. V | ( D ` x ) = K } ) = 1 ) -> E. v e. V A. w e. ( V \ { v } ) { v , w } e. E )
9 8 3mix3d 
 |-  ( ( G e. FriendGraph /\ ( # ` { x e. V | ( D ` x ) = K } ) = 1 ) -> ( A. v e. V ( D ` v ) = K \/ A. v e. V ( D ` v ) =/= K \/ E. v e. V A. w e. ( V \ { v } ) { v , w } e. E ) )
10 9 expcom 
 |-  ( ( # ` { x e. V | ( D ` x ) = K } ) = 1 -> ( G e. FriendGraph -> ( A. v e. V ( D ` v ) = K \/ A. v e. V ( D ` v ) =/= K \/ E. v e. V A. w e. ( V \ { v } ) { v , w } e. E ) ) )
11 fveqeq2 
 |-  ( x = v -> ( ( D ` x ) = K <-> ( D ` v ) = K ) )
12 11 cbvrabv 
 |-  { x e. V | ( D ` x ) = K } = { v e. V | ( D ` v ) = K }
13 12 eqeq1i 
 |-  ( { x e. V | ( D ` x ) = K } = (/) <-> { v e. V | ( D ` v ) = K } = (/) )
14 rabeq0 
 |-  ( { v e. V | ( D ` v ) = K } = (/) <-> A. v e. V -. ( D ` v ) = K )
15 13 14 bitri 
 |-  ( { x e. V | ( D ` x ) = K } = (/) <-> A. v e. V -. ( D ` v ) = K )
16 neqne 
 |-  ( -. ( D ` v ) = K -> ( D ` v ) =/= K )
17 16 ralimi 
 |-  ( A. v e. V -. ( D ` v ) = K -> A. v e. V ( D ` v ) =/= K )
18 17 3mix2d 
 |-  ( A. v e. V -. ( D ` v ) = K -> ( A. v e. V ( D ` v ) = K \/ A. v e. V ( D ` v ) =/= K \/ E. v e. V A. w e. ( V \ { v } ) { v , w } e. E ) )
19 18 a1d 
 |-  ( A. v e. V -. ( D ` v ) = K -> ( G e. FriendGraph -> ( A. v e. V ( D ` v ) = K \/ A. v e. V ( D ` v ) =/= K \/ E. v e. V A. w e. ( V \ { v } ) { v , w } e. E ) ) )
20 15 19 sylbi 
 |-  ( { x e. V | ( D ` x ) = K } = (/) -> ( G e. FriendGraph -> ( A. v e. V ( D ` v ) = K \/ A. v e. V ( D ` v ) =/= K \/ E. v e. V A. w e. ( V \ { v } ) { v , w } e. E ) ) )
21 10 20 jaoi 
 |-  ( ( ( # ` { x e. V | ( D ` x ) = K } ) = 1 \/ { x e. V | ( D ` x ) = K } = (/) ) -> ( G e. FriendGraph -> ( A. v e. V ( D ` v ) = K \/ A. v e. V ( D ` v ) =/= K \/ E. v e. V A. w e. ( V \ { v } ) { v , w } e. E ) ) )
22 1 3 5 6 2 frgrwopreg2 
 |-  ( ( G e. FriendGraph /\ ( # ` ( V \ { x e. V | ( D ` x ) = K } ) ) = 1 ) -> E. v e. V A. w e. ( V \ { v } ) { v , w } e. E )
23 22 3mix3d 
 |-  ( ( G e. FriendGraph /\ ( # ` ( V \ { x e. V | ( D ` x ) = K } ) ) = 1 ) -> ( A. v e. V ( D ` v ) = K \/ A. v e. V ( D ` v ) =/= K \/ E. v e. V A. w e. ( V \ { v } ) { v , w } e. E ) )
24 23 expcom 
 |-  ( ( # ` ( V \ { x e. V | ( D ` x ) = K } ) ) = 1 -> ( G e. FriendGraph -> ( A. v e. V ( D ` v ) = K \/ A. v e. V ( D ` v ) =/= K \/ E. v e. V A. w e. ( V \ { v } ) { v , w } e. E ) ) )
25 difrab0eq 
 |-  ( ( V \ { x e. V | ( D ` x ) = K } ) = (/) <-> V = { x e. V | ( D ` x ) = K } )
26 12 eqeq2i 
 |-  ( V = { x e. V | ( D ` x ) = K } <-> V = { v e. V | ( D ` v ) = K } )
27 rabid2 
 |-  ( V = { v e. V | ( D ` v ) = K } <-> A. v e. V ( D ` v ) = K )
28 26 27 bitri 
 |-  ( V = { x e. V | ( D ` x ) = K } <-> A. v e. V ( D ` v ) = K )
29 3mix1 
 |-  ( A. v e. V ( D ` v ) = K -> ( A. v e. V ( D ` v ) = K \/ A. v e. V ( D ` v ) =/= K \/ E. v e. V A. w e. ( V \ { v } ) { v , w } e. E ) )
30 29 a1d 
 |-  ( A. v e. V ( D ` v ) = K -> ( G e. FriendGraph -> ( A. v e. V ( D ` v ) = K \/ A. v e. V ( D ` v ) =/= K \/ E. v e. V A. w e. ( V \ { v } ) { v , w } e. E ) ) )
31 28 30 sylbi 
 |-  ( V = { x e. V | ( D ` x ) = K } -> ( G e. FriendGraph -> ( A. v e. V ( D ` v ) = K \/ A. v e. V ( D ` v ) =/= K \/ E. v e. V A. w e. ( V \ { v } ) { v , w } e. E ) ) )
32 25 31 sylbi 
 |-  ( ( V \ { x e. V | ( D ` x ) = K } ) = (/) -> ( G e. FriendGraph -> ( A. v e. V ( D ` v ) = K \/ A. v e. V ( D ` v ) =/= K \/ E. v e. V A. w e. ( V \ { v } ) { v , w } e. E ) ) )
33 24 32 jaoi 
 |-  ( ( ( # ` ( V \ { x e. V | ( D ` x ) = K } ) ) = 1 \/ ( V \ { x e. V | ( D ` x ) = K } ) = (/) ) -> ( G e. FriendGraph -> ( A. v e. V ( D ` v ) = K \/ A. v e. V ( D ` v ) =/= K \/ E. v e. V A. w e. ( V \ { v } ) { v , w } e. E ) ) )
34 21 33 jaoi 
 |-  ( ( ( ( # ` { x e. V | ( D ` x ) = K } ) = 1 \/ { x e. V | ( D ` x ) = K } = (/) ) \/ ( ( # ` ( V \ { x e. V | ( D ` x ) = K } ) ) = 1 \/ ( V \ { x e. V | ( D ` x ) = K } ) = (/) ) ) -> ( G e. FriendGraph -> ( A. v e. V ( D ` v ) = K \/ A. v e. V ( D ` v ) =/= K \/ E. v e. V A. w e. ( V \ { v } ) { v , w } e. E ) ) )
35 7 34 mpcom 
 |-  ( G e. FriendGraph -> ( A. v e. V ( D ` v ) = K \/ A. v e. V ( D ` v ) =/= K \/ E. v e. V A. w e. ( V \ { v } ) { v , w } e. E ) )