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 e. V | ( D ` x ) = K }
frgrwopreg.b 
|- B = ( V \ A )
Assertion frgrwopreg 
|- ( G e. 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 e. V | ( D ` x ) = K }
4 frgrwopreg.b 
 |-  B = ( V \ A )
5 1 2 3 4 frgrwopreglem1 
 |-  ( A e. _V /\ B e. _V )
6 hashv01gt1 
 |-  ( A e. _V -> ( ( # ` A ) = 0 \/ ( # ` A ) = 1 \/ 1 < ( # ` A ) ) )
7 hasheq0 
 |-  ( A e. _V -> ( ( # ` A ) = 0 <-> A = (/) ) )
8 biidd 
 |-  ( A e. _V -> ( ( # ` A ) = 1 <-> ( # ` A ) = 1 ) )
9 biidd 
 |-  ( A e. _V -> ( 1 < ( # ` A ) <-> 1 < ( # ` A ) ) )
10 7 8 9 3orbi123d 
 |-  ( A e. _V -> ( ( ( # ` A ) = 0 \/ ( # ` A ) = 1 \/ 1 < ( # ` A ) ) <-> ( A = (/) \/ ( # ` A ) = 1 \/ 1 < ( # ` A ) ) ) )
11 hashv01gt1 
 |-  ( B e. _V -> ( ( # ` B ) = 0 \/ ( # ` B ) = 1 \/ 1 < ( # ` B ) ) )
12 hasheq0 
 |-  ( B e. _V -> ( ( # ` B ) = 0 <-> B = (/) ) )
13 biidd 
 |-  ( B e. _V -> ( ( # ` B ) = 1 <-> ( # ` B ) = 1 ) )
14 biidd 
 |-  ( B e. _V -> ( 1 < ( # ` B ) <-> 1 < ( # ` B ) ) )
15 12 13 14 3orbi123d 
 |-  ( B e. _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 e. 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 e. 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 e. 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 e. FriendGraph -> ( ( ( # ` A ) = 1 \/ A = (/) ) \/ ( ( # ` B ) = 1 \/ B = (/) ) ) ) ) )
28 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
29 1 2 3 4 28 frgrwopreglem5 
 |-  ( ( G e. FriendGraph /\ 1 < ( # ` A ) /\ 1 < ( # ` B ) ) -> E. a e. A E. x e. A E. b e. B E. y e. B ( ( a =/= x /\ b =/= y ) /\ ( { a , b } e. ( Edg ` G ) /\ { b , x } e. ( Edg ` G ) ) /\ ( { x , y } e. ( Edg ` G ) /\ { y , a } e. ( Edg ` G ) ) ) )
30 frgrusgr 
 |-  ( G e. FriendGraph -> G e. USGraph )
31 simplll 
 |-  ( ( ( ( G e. USGraph /\ ( a e. A /\ x e. A ) ) /\ ( b e. B /\ y e. B ) ) /\ ( a =/= x /\ b =/= y ) ) -> G e. USGraph )
32 elrabi 
 |-  ( a e. { x e. V | ( D ` x ) = K } -> a e. V )
33 32 3 eleq2s 
 |-  ( a e. A -> a e. V )
34 33 adantr 
 |-  ( ( a e. A /\ x e. A ) -> a e. V )
35 34 ad3antlr 
 |-  ( ( ( ( G e. USGraph /\ ( a e. A /\ x e. A ) ) /\ ( b e. B /\ y e. B ) ) /\ ( a =/= x /\ b =/= y ) ) -> a e. V )
36 rabidim1 
 |-  ( x e. { x e. V | ( D ` x ) = K } -> x e. V )
37 36 3 eleq2s 
 |-  ( x e. A -> x e. V )
38 37 adantl 
 |-  ( ( a e. A /\ x e. A ) -> x e. V )
39 38 ad3antlr 
 |-  ( ( ( ( G e. USGraph /\ ( a e. A /\ x e. A ) ) /\ ( b e. B /\ y e. B ) ) /\ ( a =/= x /\ b =/= y ) ) -> x e. V )
40 simprl 
 |-  ( ( ( ( G e. USGraph /\ ( a e. A /\ x e. A ) ) /\ ( b e. B /\ y e. B ) ) /\ ( a =/= x /\ b =/= y ) ) -> a =/= x )
41 eldifi 
 |-  ( b e. ( V \ A ) -> b e. V )
42 41 4 eleq2s 
 |-  ( b e. B -> b e. V )
43 42 adantr 
 |-  ( ( b e. B /\ y e. B ) -> b e. V )
44 43 ad2antlr 
 |-  ( ( ( ( G e. USGraph /\ ( a e. A /\ x e. A ) ) /\ ( b e. B /\ y e. B ) ) /\ ( a =/= x /\ b =/= y ) ) -> b e. V )
45 eldifi 
 |-  ( y e. ( V \ A ) -> y e. V )
46 45 4 eleq2s 
 |-  ( y e. B -> y e. V )
47 46 adantl 
 |-  ( ( b e. B /\ y e. B ) -> y e. V )
48 47 ad2antlr 
 |-  ( ( ( ( G e. USGraph /\ ( a e. A /\ x e. A ) ) /\ ( b e. B /\ y e. B ) ) /\ ( a =/= x /\ b =/= y ) ) -> y e. V )
49 simprr 
 |-  ( ( ( ( G e. USGraph /\ ( a e. A /\ x e. A ) ) /\ ( b e. B /\ y e. B ) ) /\ ( a =/= x /\ b =/= y ) ) -> b =/= y )
50 1 28 4cyclusnfrgr 
 |-  ( ( G e. USGraph /\ ( a e. V /\ x e. V /\ a =/= x ) /\ ( b e. V /\ y e. V /\ b =/= y ) ) -> ( ( ( { a , b } e. ( Edg ` G ) /\ { b , x } e. ( Edg ` G ) ) /\ ( { x , y } e. ( Edg ` G ) /\ { y , a } e. ( Edg ` G ) ) ) -> G e/ FriendGraph ) )
51 31 35 39 40 44 48 49 50 syl133anc 
 |-  ( ( ( ( G e. USGraph /\ ( a e. A /\ x e. A ) ) /\ ( b e. B /\ y e. B ) ) /\ ( a =/= x /\ b =/= y ) ) -> ( ( ( { a , b } e. ( Edg ` G ) /\ { b , x } e. ( Edg ` G ) ) /\ ( { x , y } e. ( Edg ` G ) /\ { y , a } e. ( Edg ` G ) ) ) -> G e/ FriendGraph ) )
52 51 exp4b 
 |-  ( ( ( G e. USGraph /\ ( a e. A /\ x e. A ) ) /\ ( b e. B /\ y e. B ) ) -> ( ( a =/= x /\ b =/= y ) -> ( ( { a , b } e. ( Edg ` G ) /\ { b , x } e. ( Edg ` G ) ) -> ( ( { x , y } e. ( Edg ` G ) /\ { y , a } e. ( Edg ` G ) ) -> G e/ FriendGraph ) ) ) )
53 52 3impd 
 |-  ( ( ( G e. USGraph /\ ( a e. A /\ x e. A ) ) /\ ( b e. B /\ y e. B ) ) -> ( ( ( a =/= x /\ b =/= y ) /\ ( { a , b } e. ( Edg ` G ) /\ { b , x } e. ( Edg ` G ) ) /\ ( { x , y } e. ( Edg ` G ) /\ { y , a } e. ( Edg ` G ) ) ) -> G e/ FriendGraph ) )
54 df-nel 
 |-  ( G e/ FriendGraph <-> -. G e. FriendGraph )
55 pm2.21 
 |-  ( -. G e. FriendGraph -> ( G e. FriendGraph -> ( ( ( # ` A ) = 1 \/ A = (/) ) \/ ( ( # ` B ) = 1 \/ B = (/) ) ) ) )
56 54 55 sylbi 
 |-  ( G e/ FriendGraph -> ( G e. FriendGraph -> ( ( ( # ` A ) = 1 \/ A = (/) ) \/ ( ( # ` B ) = 1 \/ B = (/) ) ) ) )
57 53 56 syl6 
 |-  ( ( ( G e. USGraph /\ ( a e. A /\ x e. A ) ) /\ ( b e. B /\ y e. B ) ) -> ( ( ( a =/= x /\ b =/= y ) /\ ( { a , b } e. ( Edg ` G ) /\ { b , x } e. ( Edg ` G ) ) /\ ( { x , y } e. ( Edg ` G ) /\ { y , a } e. ( Edg ` G ) ) ) -> ( G e. FriendGraph -> ( ( ( # ` A ) = 1 \/ A = (/) ) \/ ( ( # ` B ) = 1 \/ B = (/) ) ) ) ) )
58 57 rexlimdvva 
 |-  ( ( G e. USGraph /\ ( a e. A /\ x e. A ) ) -> ( E. b e. B E. y e. B ( ( a =/= x /\ b =/= y ) /\ ( { a , b } e. ( Edg ` G ) /\ { b , x } e. ( Edg ` G ) ) /\ ( { x , y } e. ( Edg ` G ) /\ { y , a } e. ( Edg ` G ) ) ) -> ( G e. FriendGraph -> ( ( ( # ` A ) = 1 \/ A = (/) ) \/ ( ( # ` B ) = 1 \/ B = (/) ) ) ) ) )
59 58 rexlimdvva 
 |-  ( G e. USGraph -> ( E. a e. A E. x e. A E. b e. B E. y e. B ( ( a =/= x /\ b =/= y ) /\ ( { a , b } e. ( Edg ` G ) /\ { b , x } e. ( Edg ` G ) ) /\ ( { x , y } e. ( Edg ` G ) /\ { y , a } e. ( Edg ` G ) ) ) -> ( G e. FriendGraph -> ( ( ( # ` A ) = 1 \/ A = (/) ) \/ ( ( # ` B ) = 1 \/ B = (/) ) ) ) ) )
60 59 com23 
 |-  ( G e. USGraph -> ( G e. FriendGraph -> ( E. a e. A E. x e. A E. b e. B E. y e. B ( ( a =/= x /\ b =/= y ) /\ ( { a , b } e. ( Edg ` G ) /\ { b , x } e. ( Edg ` G ) ) /\ ( { x , y } e. ( Edg ` G ) /\ { y , a } e. ( Edg ` G ) ) ) -> ( ( ( # ` A ) = 1 \/ A = (/) ) \/ ( ( # ` B ) = 1 \/ B = (/) ) ) ) ) )
61 30 60 mpcom 
 |-  ( G e. FriendGraph -> ( E. a e. A E. x e. A E. b e. B E. y e. B ( ( a =/= x /\ b =/= y ) /\ ( { a , b } e. ( Edg ` G ) /\ { b , x } e. ( Edg ` G ) ) /\ ( { x , y } e. ( Edg ` G ) /\ { y , a } e. ( Edg ` G ) ) ) -> ( ( ( # ` A ) = 1 \/ A = (/) ) \/ ( ( # ` B ) = 1 \/ B = (/) ) ) ) )
62 61 3ad2ant1 
 |-  ( ( G e. FriendGraph /\ 1 < ( # ` A ) /\ 1 < ( # ` B ) ) -> ( E. a e. A E. x e. A E. b e. B E. y e. B ( ( a =/= x /\ b =/= y ) /\ ( { a , b } e. ( Edg ` G ) /\ { b , x } e. ( Edg ` G ) ) /\ ( { x , y } e. ( Edg ` G ) /\ { y , a } e. ( Edg ` G ) ) ) -> ( ( ( # ` A ) = 1 \/ A = (/) ) \/ ( ( # ` B ) = 1 \/ B = (/) ) ) ) )
63 29 62 mpd 
 |-  ( ( G e. FriendGraph /\ 1 < ( # ` A ) /\ 1 < ( # ` B ) ) -> ( ( ( # ` A ) = 1 \/ A = (/) ) \/ ( ( # ` B ) = 1 \/ B = (/) ) ) )
64 63 3exp 
 |-  ( G e. FriendGraph -> ( 1 < ( # ` A ) -> ( 1 < ( # ` B ) -> ( ( ( # ` A ) = 1 \/ A = (/) ) \/ ( ( # ` B ) = 1 \/ B = (/) ) ) ) ) )
65 64 com3l 
 |-  ( 1 < ( # ` A ) -> ( 1 < ( # ` B ) -> ( G e. FriendGraph -> ( ( ( # ` A ) = 1 \/ A = (/) ) \/ ( ( # ` B ) = 1 \/ B = (/) ) ) ) ) )
66 24 27 65 3jaoi 
 |-  ( ( A = (/) \/ ( # ` A ) = 1 \/ 1 < ( # ` A ) ) -> ( 1 < ( # ` B ) -> ( G e. FriendGraph -> ( ( ( # ` A ) = 1 \/ A = (/) ) \/ ( ( # ` B ) = 1 \/ B = (/) ) ) ) ) )
67 66 com12 
 |-  ( 1 < ( # ` B ) -> ( ( A = (/) \/ ( # ` A ) = 1 \/ 1 < ( # ` A ) ) -> ( G e. FriendGraph -> ( ( ( # ` A ) = 1 \/ A = (/) ) \/ ( ( # ` B ) = 1 \/ B = (/) ) ) ) ) )
68 18 21 67 3jaoi 
 |-  ( ( B = (/) \/ ( # ` B ) = 1 \/ 1 < ( # ` B ) ) -> ( ( A = (/) \/ ( # ` A ) = 1 \/ 1 < ( # ` A ) ) -> ( G e. FriendGraph -> ( ( ( # ` A ) = 1 \/ A = (/) ) \/ ( ( # ` B ) = 1 \/ B = (/) ) ) ) ) )
69 15 68 biimtrdi 
 |-  ( B e. _V -> ( ( ( # ` B ) = 0 \/ ( # ` B ) = 1 \/ 1 < ( # ` B ) ) -> ( ( A = (/) \/ ( # ` A ) = 1 \/ 1 < ( # ` A ) ) -> ( G e. FriendGraph -> ( ( ( # ` A ) = 1 \/ A = (/) ) \/ ( ( # ` B ) = 1 \/ B = (/) ) ) ) ) ) )
70 11 69 mpd 
 |-  ( B e. _V -> ( ( A = (/) \/ ( # ` A ) = 1 \/ 1 < ( # ` A ) ) -> ( G e. FriendGraph -> ( ( ( # ` A ) = 1 \/ A = (/) ) \/ ( ( # ` B ) = 1 \/ B = (/) ) ) ) ) )
71 70 com12 
 |-  ( ( A = (/) \/ ( # ` A ) = 1 \/ 1 < ( # ` A ) ) -> ( B e. _V -> ( G e. FriendGraph -> ( ( ( # ` A ) = 1 \/ A = (/) ) \/ ( ( # ` B ) = 1 \/ B = (/) ) ) ) ) )
72 10 71 biimtrdi 
 |-  ( A e. _V -> ( ( ( # ` A ) = 0 \/ ( # ` A ) = 1 \/ 1 < ( # ` A ) ) -> ( B e. _V -> ( G e. FriendGraph -> ( ( ( # ` A ) = 1 \/ A = (/) ) \/ ( ( # ` B ) = 1 \/ B = (/) ) ) ) ) ) )
73 6 72 mpd 
 |-  ( A e. _V -> ( B e. _V -> ( G e. FriendGraph -> ( ( ( # ` A ) = 1 \/ A = (/) ) \/ ( ( # ` B ) = 1 \/ B = (/) ) ) ) ) )
74 73 imp 
 |-  ( ( A e. _V /\ B e. _V ) -> ( G e. FriendGraph -> ( ( ( # ` A ) = 1 \/ A = (/) ) \/ ( ( # ` B ) = 1 \/ B = (/) ) ) ) )
75 5 74 ax-mp 
 |-  ( G e. FriendGraph -> ( ( ( # ` A ) = 1 \/ A = (/) ) \/ ( ( # ` B ) = 1 \/ B = (/) ) ) )