Metamath Proof Explorer

Theorem friendshipgt3

Description: The friendship theorem for big graphs: In every finite friendship graph with order greater than 3 there is a vertex which is adjacent to all other vertices. (Contributed by Alexander van der Vekens, 9-Oct-2018) (Revised by AV, 4-Jun-2021)

Ref Expression
Hypothesis frgrreggt1.v 
|- V = ( Vtx ` G )
Assertion friendshipgt3 
|- ( ( G e. FriendGraph /\ V e. Fin /\ 3 < ( # ` V ) ) -> E. v e. V A. w e. ( V \ { v } ) { v , w } e. ( Edg ` G ) )

Proof

Step Hyp Ref Expression
1 frgrreggt1.v 
 |-  V = ( Vtx ` G )
2 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
3 1 2 frgrregorufrg 
 |-  ( G e. FriendGraph -> A. k e. NN0 ( E. u e. V ( ( VtxDeg ` G ) ` u ) = k -> ( G RegUSGraph k \/ E. v e. V A. w e. ( V \ { v } ) { v , w } e. ( Edg ` G ) ) ) )
4 3 3ad2ant1 
 |-  ( ( G e. FriendGraph /\ V e. Fin /\ 3 < ( # ` V ) ) -> A. k e. NN0 ( E. u e. V ( ( VtxDeg ` G ) ` u ) = k -> ( G RegUSGraph k \/ E. v e. V A. w e. ( V \ { v } ) { v , w } e. ( Edg ` G ) ) ) )
5 1 frgrogt3nreg 
 |-  ( ( G e. FriendGraph /\ V e. Fin /\ 3 < ( # ` V ) ) -> A. k e. NN0 -. G RegUSGraph k )
6 frgrusgr 
 |-  ( G e. FriendGraph -> G e. USGraph )
7 6 anim1i 
 |-  ( ( G e. FriendGraph /\ V e. Fin ) -> ( G e. USGraph /\ V e. Fin ) )
8 1 isfusgr 
 |-  ( G e. FinUSGraph <-> ( G e. USGraph /\ V e. Fin ) )
9 7 8 sylibr 
 |-  ( ( G e. FriendGraph /\ V e. Fin ) -> G e. FinUSGraph )
10 9 3adant3 
 |-  ( ( G e. FriendGraph /\ V e. Fin /\ 3 < ( # ` V ) ) -> G e. FinUSGraph )
11 0red 
 |-  ( ( V e. Fin /\ 3 < ( # ` V ) ) -> 0 e. RR )
12 3re 
 |-  3 e. RR
13 12 a1i 
 |-  ( ( V e. Fin /\ 3 < ( # ` V ) ) -> 3 e. RR )
14 hashcl 
 |-  ( V e. Fin -> ( # ` V ) e. NN0 )
15 14 nn0red 
 |-  ( V e. Fin -> ( # ` V ) e. RR )
16 15 adantr 
 |-  ( ( V e. Fin /\ 3 < ( # ` V ) ) -> ( # ` V ) e. RR )
17 3pos 
 |-  0 < 3
18 17 a1i 
 |-  ( ( V e. Fin /\ 3 < ( # ` V ) ) -> 0 < 3 )
19 simpr 
 |-  ( ( V e. Fin /\ 3 < ( # ` V ) ) -> 3 < ( # ` V ) )
20 11 13 16 18 19 lttrd 
 |-  ( ( V e. Fin /\ 3 < ( # ` V ) ) -> 0 < ( # ` V ) )
21 20 gt0ne0d 
 |-  ( ( V e. Fin /\ 3 < ( # ` V ) ) -> ( # ` V ) =/= 0 )
22 hasheq0 
 |-  ( V e. Fin -> ( ( # ` V ) = 0 <-> V = (/) ) )
23 22 adantr 
 |-  ( ( V e. Fin /\ 3 < ( # ` V ) ) -> ( ( # ` V ) = 0 <-> V = (/) ) )
24 23 necon3bid 
 |-  ( ( V e. Fin /\ 3 < ( # ` V ) ) -> ( ( # ` V ) =/= 0 <-> V =/= (/) ) )
25 21 24 mpbid 
 |-  ( ( V e. Fin /\ 3 < ( # ` V ) ) -> V =/= (/) )
26 25 3adant1 
 |-  ( ( G e. FriendGraph /\ V e. Fin /\ 3 < ( # ` V ) ) -> V =/= (/) )
27 1 fusgrn0degnn0 
 |-  ( ( G e. FinUSGraph /\ V =/= (/) ) -> E. t e. V E. m e. NN0 ( ( VtxDeg ` G ) ` t ) = m )
28 10 26 27 syl2anc 
 |-  ( ( G e. FriendGraph /\ V e. Fin /\ 3 < ( # ` V ) ) -> E. t e. V E. m e. NN0 ( ( VtxDeg ` G ) ` t ) = m )
29 r19.26 
 |-  ( A. k e. NN0 ( ( E. u e. V ( ( VtxDeg ` G ) ` u ) = k -> ( G RegUSGraph k \/ E. v e. V A. w e. ( V \ { v } ) { v , w } e. ( Edg ` G ) ) ) /\ -. G RegUSGraph k ) <-> ( A. k e. NN0 ( E. u e. V ( ( VtxDeg ` G ) ` u ) = k -> ( G RegUSGraph k \/ E. v e. V A. w e. ( V \ { v } ) { v , w } e. ( Edg ` G ) ) ) /\ A. k e. NN0 -. G RegUSGraph k ) )
30 simpllr 
 |-  ( ( ( ( t e. V /\ m e. NN0 ) /\ ( ( VtxDeg ` G ) ` t ) = m ) /\ ( G e. FriendGraph /\ V e. Fin /\ 3 < ( # ` V ) ) ) -> m e. NN0 )
31 fveqeq2 
 |-  ( u = t -> ( ( ( VtxDeg ` G ) ` u ) = m <-> ( ( VtxDeg ` G ) ` t ) = m ) )
32 31 rspcev 
 |-  ( ( t e. V /\ ( ( VtxDeg ` G ) ` t ) = m ) -> E. u e. V ( ( VtxDeg ` G ) ` u ) = m )
33 32 ad4ant13 
 |-  ( ( ( ( t e. V /\ m e. NN0 ) /\ ( ( VtxDeg ` G ) ` t ) = m ) /\ ( G e. FriendGraph /\ V e. Fin /\ 3 < ( # ` V ) ) ) -> E. u e. V ( ( VtxDeg ` G ) ` u ) = m )
34 ornld 
 |-  ( E. u e. V ( ( VtxDeg ` G ) ` u ) = m -> ( ( ( E. u e. V ( ( VtxDeg ` G ) ` u ) = m -> ( G RegUSGraph m \/ E. v e. V A. w e. ( V \ { v } ) { v , w } e. ( Edg ` G ) ) ) /\ -. G RegUSGraph m ) -> E. v e. V A. w e. ( V \ { v } ) { v , w } e. ( Edg ` G ) ) )
35 33 34 syl 
 |-  ( ( ( ( t e. V /\ m e. NN0 ) /\ ( ( VtxDeg ` G ) ` t ) = m ) /\ ( G e. FriendGraph /\ V e. Fin /\ 3 < ( # ` V ) ) ) -> ( ( ( E. u e. V ( ( VtxDeg ` G ) ` u ) = m -> ( G RegUSGraph m \/ E. v e. V A. w e. ( V \ { v } ) { v , w } e. ( Edg ` G ) ) ) /\ -. G RegUSGraph m ) -> E. v e. V A. w e. ( V \ { v } ) { v , w } e. ( Edg ` G ) ) )
36 35 adantr 
 |-  ( ( ( ( ( t e. V /\ m e. NN0 ) /\ ( ( VtxDeg ` G ) ` t ) = m ) /\ ( G e. FriendGraph /\ V e. Fin /\ 3 < ( # ` V ) ) ) /\ k = m ) -> ( ( ( E. u e. V ( ( VtxDeg ` G ) ` u ) = m -> ( G RegUSGraph m \/ E. v e. V A. w e. ( V \ { v } ) { v , w } e. ( Edg ` G ) ) ) /\ -. G RegUSGraph m ) -> E. v e. V A. w e. ( V \ { v } ) { v , w } e. ( Edg ` G ) ) )
37 eqeq2 
 |-  ( k = m -> ( ( ( VtxDeg ` G ) ` u ) = k <-> ( ( VtxDeg ` G ) ` u ) = m ) )
38 37 rexbidv 
 |-  ( k = m -> ( E. u e. V ( ( VtxDeg ` G ) ` u ) = k <-> E. u e. V ( ( VtxDeg ` G ) ` u ) = m ) )
39 breq2 
 |-  ( k = m -> ( G RegUSGraph k <-> G RegUSGraph m ) )
40 39 orbi1d 
 |-  ( k = m -> ( ( G RegUSGraph k \/ E. v e. V A. w e. ( V \ { v } ) { v , w } e. ( Edg ` G ) ) <-> ( G RegUSGraph m \/ E. v e. V A. w e. ( V \ { v } ) { v , w } e. ( Edg ` G ) ) ) )
41 38 40 imbi12d 
 |-  ( k = m -> ( ( E. u e. V ( ( VtxDeg ` G ) ` u ) = k -> ( G RegUSGraph k \/ E. v e. V A. w e. ( V \ { v } ) { v , w } e. ( Edg ` G ) ) ) <-> ( E. u e. V ( ( VtxDeg ` G ) ` u ) = m -> ( G RegUSGraph m \/ E. v e. V A. w e. ( V \ { v } ) { v , w } e. ( Edg ` G ) ) ) ) )
42 39 notbid 
 |-  ( k = m -> ( -. G RegUSGraph k <-> -. G RegUSGraph m ) )
43 41 42 anbi12d 
 |-  ( k = m -> ( ( ( E. u e. V ( ( VtxDeg ` G ) ` u ) = k -> ( G RegUSGraph k \/ E. v e. V A. w e. ( V \ { v } ) { v , w } e. ( Edg ` G ) ) ) /\ -. G RegUSGraph k ) <-> ( ( E. u e. V ( ( VtxDeg ` G ) ` u ) = m -> ( G RegUSGraph m \/ E. v e. V A. w e. ( V \ { v } ) { v , w } e. ( Edg ` G ) ) ) /\ -. G RegUSGraph m ) ) )
44 43 imbi1d 
 |-  ( k = m -> ( ( ( ( E. u e. V ( ( VtxDeg ` G ) ` u ) = k -> ( G RegUSGraph k \/ E. v e. V A. w e. ( V \ { v } ) { v , w } e. ( Edg ` G ) ) ) /\ -. G RegUSGraph k ) -> E. v e. V A. w e. ( V \ { v } ) { v , w } e. ( Edg ` G ) ) <-> ( ( ( E. u e. V ( ( VtxDeg ` G ) ` u ) = m -> ( G RegUSGraph m \/ E. v e. V A. w e. ( V \ { v } ) { v , w } e. ( Edg ` G ) ) ) /\ -. G RegUSGraph m ) -> E. v e. V A. w e. ( V \ { v } ) { v , w } e. ( Edg ` G ) ) ) )
45 44 adantl 
 |-  ( ( ( ( ( t e. V /\ m e. NN0 ) /\ ( ( VtxDeg ` G ) ` t ) = m ) /\ ( G e. FriendGraph /\ V e. Fin /\ 3 < ( # ` V ) ) ) /\ k = m ) -> ( ( ( ( E. u e. V ( ( VtxDeg ` G ) ` u ) = k -> ( G RegUSGraph k \/ E. v e. V A. w e. ( V \ { v } ) { v , w } e. ( Edg ` G ) ) ) /\ -. G RegUSGraph k ) -> E. v e. V A. w e. ( V \ { v } ) { v , w } e. ( Edg ` G ) ) <-> ( ( ( E. u e. V ( ( VtxDeg ` G ) ` u ) = m -> ( G RegUSGraph m \/ E. v e. V A. w e. ( V \ { v } ) { v , w } e. ( Edg ` G ) ) ) /\ -. G RegUSGraph m ) -> E. v e. V A. w e. ( V \ { v } ) { v , w } e. ( Edg ` G ) ) ) )
46 36 45 mpbird 
 |-  ( ( ( ( ( t e. V /\ m e. NN0 ) /\ ( ( VtxDeg ` G ) ` t ) = m ) /\ ( G e. FriendGraph /\ V e. Fin /\ 3 < ( # ` V ) ) ) /\ k = m ) -> ( ( ( E. u e. V ( ( VtxDeg ` G ) ` u ) = k -> ( G RegUSGraph k \/ E. v e. V A. w e. ( V \ { v } ) { v , w } e. ( Edg ` G ) ) ) /\ -. G RegUSGraph k ) -> E. v e. V A. w e. ( V \ { v } ) { v , w } e. ( Edg ` G ) ) )
47 30 46 rspcimdv 
 |-  ( ( ( ( t e. V /\ m e. NN0 ) /\ ( ( VtxDeg ` G ) ` t ) = m ) /\ ( G e. FriendGraph /\ V e. Fin /\ 3 < ( # ` V ) ) ) -> ( A. k e. NN0 ( ( E. u e. V ( ( VtxDeg ` G ) ` u ) = k -> ( G RegUSGraph k \/ E. v e. V A. w e. ( V \ { v } ) { v , w } e. ( Edg ` G ) ) ) /\ -. G RegUSGraph k ) -> E. v e. V A. w e. ( V \ { v } ) { v , w } e. ( Edg ` G ) ) )
48 47 com12 
 |-  ( A. k e. NN0 ( ( E. u e. V ( ( VtxDeg ` G ) ` u ) = k -> ( G RegUSGraph k \/ E. v e. V A. w e. ( V \ { v } ) { v , w } e. ( Edg ` G ) ) ) /\ -. G RegUSGraph k ) -> ( ( ( ( t e. V /\ m e. NN0 ) /\ ( ( VtxDeg ` G ) ` t ) = m ) /\ ( G e. FriendGraph /\ V e. Fin /\ 3 < ( # ` V ) ) ) -> E. v e. V A. w e. ( V \ { v } ) { v , w } e. ( Edg ` G ) ) )
49 29 48 sylbir 
 |-  ( ( A. k e. NN0 ( E. u e. V ( ( VtxDeg ` G ) ` u ) = k -> ( G RegUSGraph k \/ E. v e. V A. w e. ( V \ { v } ) { v , w } e. ( Edg ` G ) ) ) /\ A. k e. NN0 -. G RegUSGraph k ) -> ( ( ( ( t e. V /\ m e. NN0 ) /\ ( ( VtxDeg ` G ) ` t ) = m ) /\ ( G e. FriendGraph /\ V e. Fin /\ 3 < ( # ` V ) ) ) -> E. v e. V A. w e. ( V \ { v } ) { v , w } e. ( Edg ` G ) ) )
50 49 expcom 
 |-  ( A. k e. NN0 -. G RegUSGraph k -> ( A. k e. NN0 ( E. u e. V ( ( VtxDeg ` G ) ` u ) = k -> ( G RegUSGraph k \/ E. v e. V A. w e. ( V \ { v } ) { v , w } e. ( Edg ` G ) ) ) -> ( ( ( ( t e. V /\ m e. NN0 ) /\ ( ( VtxDeg ` G ) ` t ) = m ) /\ ( G e. FriendGraph /\ V e. Fin /\ 3 < ( # ` V ) ) ) -> E. v e. V A. w e. ( V \ { v } ) { v , w } e. ( Edg ` G ) ) ) )
51 50 com13 
 |-  ( ( ( ( t e. V /\ m e. NN0 ) /\ ( ( VtxDeg ` G ) ` t ) = m ) /\ ( G e. FriendGraph /\ V e. Fin /\ 3 < ( # ` V ) ) ) -> ( A. k e. NN0 ( E. u e. V ( ( VtxDeg ` G ) ` u ) = k -> ( G RegUSGraph k \/ E. v e. V A. w e. ( V \ { v } ) { v , w } e. ( Edg ` G ) ) ) -> ( A. k e. NN0 -. G RegUSGraph k -> E. v e. V A. w e. ( V \ { v } ) { v , w } e. ( Edg ` G ) ) ) )
52 51 exp31 
 |-  ( ( t e. V /\ m e. NN0 ) -> ( ( ( VtxDeg ` G ) ` t ) = m -> ( ( G e. FriendGraph /\ V e. Fin /\ 3 < ( # ` V ) ) -> ( A. k e. NN0 ( E. u e. V ( ( VtxDeg ` G ) ` u ) = k -> ( G RegUSGraph k \/ E. v e. V A. w e. ( V \ { v } ) { v , w } e. ( Edg ` G ) ) ) -> ( A. k e. NN0 -. G RegUSGraph k -> E. v e. V A. w e. ( V \ { v } ) { v , w } e. ( Edg ` G ) ) ) ) ) )
53 52 rexlimivv 
 |-  ( E. t e. V E. m e. NN0 ( ( VtxDeg ` G ) ` t ) = m -> ( ( G e. FriendGraph /\ V e. Fin /\ 3 < ( # ` V ) ) -> ( A. k e. NN0 ( E. u e. V ( ( VtxDeg ` G ) ` u ) = k -> ( G RegUSGraph k \/ E. v e. V A. w e. ( V \ { v } ) { v , w } e. ( Edg ` G ) ) ) -> ( A. k e. NN0 -. G RegUSGraph k -> E. v e. V A. w e. ( V \ { v } ) { v , w } e. ( Edg ` G ) ) ) ) )
54 28 53 mpcom 
 |-  ( ( G e. FriendGraph /\ V e. Fin /\ 3 < ( # ` V ) ) -> ( A. k e. NN0 ( E. u e. V ( ( VtxDeg ` G ) ` u ) = k -> ( G RegUSGraph k \/ E. v e. V A. w e. ( V \ { v } ) { v , w } e. ( Edg ` G ) ) ) -> ( A. k e. NN0 -. G RegUSGraph k -> E. v e. V A. w e. ( V \ { v } ) { v , w } e. ( Edg ` G ) ) ) )
55 4 5 54 mp2d 
 |-  ( ( G e. FriendGraph /\ V e. Fin /\ 3 < ( # ` V ) ) -> E. v e. V A. w e. ( V \ { v } ) { v , w } e. ( Edg ` G ) )