Metamath Proof Explorer

Theorem frgrwopreg

Description: In a friendship graph there are either no vertices ( A = (/) ) or exactly one vertex ( ( #A ) = 1 ) having degree K , or all ( B = (/) ) or all except one vertices ( ( #B ) = 1 ) have degree K . (Contributed by Alexander van der Vekens, 31-Dec-2017) (Revised by AV, 10-May-2021) (Proof shortened by AV, 3-Jan-2022)

Ref Expression
Hypotheses frgrwopreg.v ⊢V=Vtx⁡G
frgrwopreg.d ⊢D=VtxDeg⁡G
frgrwopreg.a ⊢A=x∈V|D⁡x=K
frgrwopreg.b ⊢B=V∖A
Assertion frgrwopreg ⊢G∈FriendGraph→A=1∨A=∅∨B=1∨B=∅

Proof

Step Hyp Ref Expression
1 frgrwopreg.v ⊢V=Vtx⁡G
2 frgrwopreg.d ⊢D=VtxDeg⁡G
3 frgrwopreg.a ⊢A=x∈V|D⁡x=K
4 frgrwopreg.b ⊢B=V∖A
5 1 2 3 4 frgrwopreglem1 ⊢A∈V∧B∈V
6 hashv01gt1 ⊢A∈V→A=0∨A=1∨1<A
7 hasheq0 ⊢A∈V→A=0↔A=∅
8 biidd ⊢A∈V→A=1↔A=1
9 biidd ⊢A∈V→1<A↔1<A
10 7 8 9 3orbi123d ⊢A∈V→A=0∨A=1∨1<A↔A=∅∨A=1∨1<A
11 hashv01gt1 ⊢B∈V→B=0∨B=1∨1<B
12 hasheq0 ⊢B∈V→B=0↔B=∅
13 biidd ⊢B∈V→B=1↔B=1
14 biidd ⊢B∈V→1<B↔1<B
15 12 13 14 3orbi123d ⊢B∈V→B=0∨B=1∨1<B↔B=∅∨B=1∨1<B
16 olc ⊢B=∅→B=1∨B=∅
17 16 olcd ⊢B=∅→A=1∨A=∅∨B=1∨B=∅
18 17 2a1d ⊢B=∅→A=∅∨A=1∨1<A→G∈FriendGraph→A=1∨A=∅∨B=1∨B=∅
19 orc ⊢B=1→B=1∨B=∅
20 19 olcd ⊢B=1→A=1∨A=∅∨B=1∨B=∅
21 20 2a1d ⊢B=1→A=∅∨A=1∨1<A→G∈FriendGraph→A=1∨A=∅∨B=1∨B=∅
22 olc ⊢A=∅→A=1∨A=∅
23 22 orcd ⊢A=∅→A=1∨A=∅∨B=1∨B=∅
24 23 2a1d ⊢A=∅→1<B→G∈FriendGraph→A=1∨A=∅∨B=1∨B=∅
25 orc ⊢A=1→A=1∨A=∅
26 25 orcd ⊢A=1→A=1∨A=∅∨B=1∨B=∅
27 26 2a1d ⊢A=1→1<B→G∈FriendGraph→A=1∨A=∅∨B=1∨B=∅
28 eqid ⊢Edg⁡G=Edg⁡G
29 1 2 3 4 28 frgrwopreglem5 ⊢G∈FriendGraph∧1<A∧1<B→∃a∈A∃x∈A∃b∈B∃y∈Ba≠x∧b≠y∧ab∈Edg⁡G∧bx∈Edg⁡G∧xy∈Edg⁡G∧ya∈Edg⁡G
30 frgrusgr ⊢G∈FriendGraph→G∈USGraph
31 simplll ⊢G∈USGraph∧a∈A∧x∈A∧b∈B∧y∈B∧a≠x∧b≠y→G∈USGraph
32 elrabi ⊢a∈x∈V|D⁡x=K→a∈V
33 32 3 eleq2s ⊢a∈A→a∈V
34 33 adantr ⊢a∈A∧x∈A→a∈V
35 34 ad3antlr ⊢G∈USGraph∧a∈A∧x∈A∧b∈B∧y∈B∧a≠x∧b≠y→a∈V
36 rabidim1 ⊢x∈x∈V|D⁡x=K→x∈V
37 36 3 eleq2s ⊢x∈A→x∈V
38 37 adantl ⊢a∈A∧x∈A→x∈V
39 38 ad3antlr ⊢G∈USGraph∧a∈A∧x∈A∧b∈B∧y∈B∧a≠x∧b≠y→x∈V
40 simprl ⊢G∈USGraph∧a∈A∧x∈A∧b∈B∧y∈B∧a≠x∧b≠y→a≠x
41 eldifi ⊢b∈V∖A→b∈V
42 41 4 eleq2s ⊢b∈B→b∈V
43 42 adantr ⊢b∈B∧y∈B→b∈V
44 43 ad2antlr ⊢G∈USGraph∧a∈A∧x∈A∧b∈B∧y∈B∧a≠x∧b≠y→b∈V
45 eldifi ⊢y∈V∖A→y∈V
46 45 4 eleq2s ⊢y∈B→y∈V
47 46 adantl ⊢b∈B∧y∈B→y∈V
48 47 ad2antlr ⊢G∈USGraph∧a∈A∧x∈A∧b∈B∧y∈B∧a≠x∧b≠y→y∈V
49 simprr ⊢G∈USGraph∧a∈A∧x∈A∧b∈B∧y∈B∧a≠x∧b≠y→b≠y
50 1 28 4cyclusnfrgr ⊢G∈USGraph∧a∈V∧x∈V∧a≠x∧b∈V∧y∈V∧b≠y→ab∈Edg⁡G∧bx∈Edg⁡G∧xy∈Edg⁡G∧ya∈Edg⁡G→G∉FriendGraph
51 31 35 39 40 44 48 49 50 syl133anc ⊢G∈USGraph∧a∈A∧x∈A∧b∈B∧y∈B∧a≠x∧b≠y→ab∈Edg⁡G∧bx∈Edg⁡G∧xy∈Edg⁡G∧ya∈Edg⁡G→G∉FriendGraph
52 51 exp4b ⊢G∈USGraph∧a∈A∧x∈A∧b∈B∧y∈B→a≠x∧b≠y→ab∈Edg⁡G∧bx∈Edg⁡G→xy∈Edg⁡G∧ya∈Edg⁡G→G∉FriendGraph
53 52 3impd ⊢G∈USGraph∧a∈A∧x∈A∧b∈B∧y∈B→a≠x∧b≠y∧ab∈Edg⁡G∧bx∈Edg⁡G∧xy∈Edg⁡G∧ya∈Edg⁡G→G∉FriendGraph
54 df-nel ⊢G∉FriendGraph↔¬G∈FriendGraph
55 pm2.21 ⊢¬G∈FriendGraph→G∈FriendGraph→A=1∨A=∅∨B=1∨B=∅
56 54 55 sylbi ⊢G∉FriendGraph→G∈FriendGraph→A=1∨A=∅∨B=1∨B=∅
57 53 56 syl6 ⊢G∈USGraph∧a∈A∧x∈A∧b∈B∧y∈B→a≠x∧b≠y∧ab∈Edg⁡G∧bx∈Edg⁡G∧xy∈Edg⁡G∧ya∈Edg⁡G→G∈FriendGraph→A=1∨A=∅∨B=1∨B=∅
58 57 rexlimdvva ⊢G∈USGraph∧a∈A∧x∈A→∃b∈B∃y∈Ba≠x∧b≠y∧ab∈Edg⁡G∧bx∈Edg⁡G∧xy∈Edg⁡G∧ya∈Edg⁡G→G∈FriendGraph→A=1∨A=∅∨B=1∨B=∅
59 58 rexlimdvva ⊢G∈USGraph→∃a∈A∃x∈A∃b∈B∃y∈Ba≠x∧b≠y∧ab∈Edg⁡G∧bx∈Edg⁡G∧xy∈Edg⁡G∧ya∈Edg⁡G→G∈FriendGraph→A=1∨A=∅∨B=1∨B=∅
60 59 com23 ⊢G∈USGraph→G∈FriendGraph→∃a∈A∃x∈A∃b∈B∃y∈Ba≠x∧b≠y∧ab∈Edg⁡G∧bx∈Edg⁡G∧xy∈Edg⁡G∧ya∈Edg⁡G→A=1∨A=∅∨B=1∨B=∅
61 30 60 mpcom ⊢G∈FriendGraph→∃a∈A∃x∈A∃b∈B∃y∈Ba≠x∧b≠y∧ab∈Edg⁡G∧bx∈Edg⁡G∧xy∈Edg⁡G∧ya∈Edg⁡G→A=1∨A=∅∨B=1∨B=∅
62 61 3ad2ant1 ⊢G∈FriendGraph∧1<A∧1<B→∃a∈A∃x∈A∃b∈B∃y∈Ba≠x∧b≠y∧ab∈Edg⁡G∧bx∈Edg⁡G∧xy∈Edg⁡G∧ya∈Edg⁡G→A=1∨A=∅∨B=1∨B=∅
63 29 62 mpd ⊢G∈FriendGraph∧1<A∧1<B→A=1∨A=∅∨B=1∨B=∅
64 63 3exp ⊢G∈FriendGraph→1<A→1<B→A=1∨A=∅∨B=1∨B=∅
65 64 com3l ⊢1<A→1<B→G∈FriendGraph→A=1∨A=∅∨B=1∨B=∅
66 24 27 65 3jaoi ⊢A=∅∨A=1∨1<A→1<B→G∈FriendGraph→A=1∨A=∅∨B=1∨B=∅
67 66 com12 ⊢1<B→A=∅∨A=1∨1<A→G∈FriendGraph→A=1∨A=∅∨B=1∨B=∅
68 18 21 67 3jaoi ⊢B=∅∨B=1∨1<B→A=∅∨A=1∨1<A→G∈FriendGraph→A=1∨A=∅∨B=1∨B=∅
69 15 68 syl6bi ⊢B∈V→B=0∨B=1∨1<B→A=∅∨A=1∨1<A→G∈FriendGraph→A=1∨A=∅∨B=1∨B=∅
70 11 69 mpd ⊢B∈V→A=∅∨A=1∨1<A→G∈FriendGraph→A=1∨A=∅∨B=1∨B=∅
71 70 com12 ⊢A=∅∨A=1∨1<A→B∈V→G∈FriendGraph→A=1∨A=∅∨B=1∨B=∅
72 10 71 syl6bi ⊢A∈V→A=0∨A=1∨1<A→B∈V→G∈FriendGraph→A=1∨A=∅∨B=1∨B=∅
73 6 72 mpd ⊢A∈V→B∈V→G∈FriendGraph→A=1∨A=∅∨B=1∨B=∅
74 73 imp ⊢A∈V∧B∈V→G∈FriendGraph→A=1∨A=∅∨B=1∨B=∅
75 5 74 ax-mp ⊢G∈FriendGraph→A=1∨A=∅∨B=1∨B=∅