Metamath Proof Explorer

Theorem friendship

Description: The friendship theorem: In every finite (nonempty) friendship graph there is a vertex which is adjacent to all other vertices. This is Metamath 100 proof #83. (Contributed by Alexander van der Vekens, 9-Oct-2018)

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

Proof

Step Hyp Ref Expression
1 friendship.v 
 |-  V = ( Vtx ` G )
2 simpr1 
 |-  ( ( 3 < ( # ` V ) /\ ( G e. FriendGraph /\ V =/= (/) /\ V e. Fin ) ) -> G e. FriendGraph )
3 simpr3 
 |-  ( ( 3 < ( # ` V ) /\ ( G e. FriendGraph /\ V =/= (/) /\ V e. Fin ) ) -> V e. Fin )
4 simpl 
 |-  ( ( 3 < ( # ` V ) /\ ( G e. FriendGraph /\ V =/= (/) /\ V e. Fin ) ) -> 3 < ( # ` V ) )
5 1 friendshipgt3 
 |-  ( ( G e. FriendGraph /\ V e. Fin /\ 3 < ( # ` V ) ) -> E. v e. V A. w e. ( V \ { v } ) { v , w } e. ( Edg ` G ) )
6 2 3 4 5 syl3anc 
 |-  ( ( 3 < ( # ` V ) /\ ( G e. FriendGraph /\ V =/= (/) /\ V e. Fin ) ) -> E. v e. V A. w e. ( V \ { v } ) { v , w } e. ( Edg ` G ) )
7 6 ex 
 |-  ( 3 < ( # ` V ) -> ( ( G e. FriendGraph /\ V =/= (/) /\ V e. Fin ) -> E. v e. V A. w e. ( V \ { v } ) { v , w } e. ( Edg ` G ) ) )
8 hashcl 
 |-  ( V e. Fin -> ( # ` V ) e. NN0 )
9 simplr 
 |-  ( ( ( ( # ` V ) e. NN0 /\ V e. Fin ) /\ ( -. 3 < ( # ` V ) /\ V =/= (/) ) ) -> V e. Fin )
10 hashge1 
 |-  ( ( V e. Fin /\ V =/= (/) ) -> 1 <_ ( # ` V ) )
11 10 ad2ant2l 
 |-  ( ( ( ( # ` V ) e. NN0 /\ V e. Fin ) /\ ( -. 3 < ( # ` V ) /\ V =/= (/) ) ) -> 1 <_ ( # ` V ) )
12 nn0re 
 |-  ( ( # ` V ) e. NN0 -> ( # ` V ) e. RR )
13 3re 
 |-  3 e. RR
14 lenlt 
 |-  ( ( ( # ` V ) e. RR /\ 3 e. RR ) -> ( ( # ` V ) <_ 3 <-> -. 3 < ( # ` V ) ) )
15 12 13 14 sylancl 
 |-  ( ( # ` V ) e. NN0 -> ( ( # ` V ) <_ 3 <-> -. 3 < ( # ` V ) ) )
16 15 biimprd 
 |-  ( ( # ` V ) e. NN0 -> ( -. 3 < ( # ` V ) -> ( # ` V ) <_ 3 ) )
17 16 adantr 
 |-  ( ( ( # ` V ) e. NN0 /\ V e. Fin ) -> ( -. 3 < ( # ` V ) -> ( # ` V ) <_ 3 ) )
18 17 com12 
 |-  ( -. 3 < ( # ` V ) -> ( ( ( # ` V ) e. NN0 /\ V e. Fin ) -> ( # ` V ) <_ 3 ) )
19 18 adantr 
 |-  ( ( -. 3 < ( # ` V ) /\ V =/= (/) ) -> ( ( ( # ` V ) e. NN0 /\ V e. Fin ) -> ( # ` V ) <_ 3 ) )
20 19 impcom 
 |-  ( ( ( ( # ` V ) e. NN0 /\ V e. Fin ) /\ ( -. 3 < ( # ` V ) /\ V =/= (/) ) ) -> ( # ` V ) <_ 3 )
21 9 11 20 3jca 
 |-  ( ( ( ( # ` V ) e. NN0 /\ V e. Fin ) /\ ( -. 3 < ( # ` V ) /\ V =/= (/) ) ) -> ( V e. Fin /\ 1 <_ ( # ` V ) /\ ( # ` V ) <_ 3 ) )
22 21 exp31 
 |-  ( ( # ` V ) e. NN0 -> ( V e. Fin -> ( ( -. 3 < ( # ` V ) /\ V =/= (/) ) -> ( V e. Fin /\ 1 <_ ( # ` V ) /\ ( # ` V ) <_ 3 ) ) ) )
23 8 22 mpcom 
 |-  ( V e. Fin -> ( ( -. 3 < ( # ` V ) /\ V =/= (/) ) -> ( V e. Fin /\ 1 <_ ( # ` V ) /\ ( # ` V ) <_ 3 ) ) )
24 23 impcom 
 |-  ( ( ( -. 3 < ( # ` V ) /\ V =/= (/) ) /\ V e. Fin ) -> ( V e. Fin /\ 1 <_ ( # ` V ) /\ ( # ` V ) <_ 3 ) )
25 hash1to3 
 |-  ( ( V e. Fin /\ 1 <_ ( # ` V ) /\ ( # ` V ) <_ 3 ) -> E. a E. b E. c ( V = { a } \/ V = { a , b } \/ V = { a , b , c } ) )
26 vex 
 |-  a e. _V
27 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
28 1 27 1to3vfriendship 
 |-  ( ( a e. _V /\ ( V = { a } \/ V = { a , b } \/ V = { a , b , c } ) ) -> ( G e. FriendGraph -> E. v e. V A. w e. ( V \ { v } ) { v , w } e. ( Edg ` G ) ) )
29 26 28 mpan 
 |-  ( ( V = { a } \/ V = { a , b } \/ V = { a , b , c } ) -> ( G e. FriendGraph -> E. v e. V A. w e. ( V \ { v } ) { v , w } e. ( Edg ` G ) ) )
30 29 exlimiv 
 |-  ( E. c ( V = { a } \/ V = { a , b } \/ V = { a , b , c } ) -> ( G e. FriendGraph -> E. v e. V A. w e. ( V \ { v } ) { v , w } e. ( Edg ` G ) ) )
31 30 exlimivv 
 |-  ( E. a E. b E. c ( V = { a } \/ V = { a , b } \/ V = { a , b , c } ) -> ( G e. FriendGraph -> E. v e. V A. w e. ( V \ { v } ) { v , w } e. ( Edg ` G ) ) )
32 24 25 31 3syl 
 |-  ( ( ( -. 3 < ( # ` V ) /\ V =/= (/) ) /\ V e. Fin ) -> ( G e. FriendGraph -> E. v e. V A. w e. ( V \ { v } ) { v , w } e. ( Edg ` G ) ) )
33 32 exp31 
 |-  ( -. 3 < ( # ` V ) -> ( V =/= (/) -> ( V e. Fin -> ( G e. FriendGraph -> E. v e. V A. w e. ( V \ { v } ) { v , w } e. ( Edg ` G ) ) ) ) )
34 33 com14 
 |-  ( G e. FriendGraph -> ( V =/= (/) -> ( V e. Fin -> ( -. 3 < ( # ` V ) -> E. v e. V A. w e. ( V \ { v } ) { v , w } e. ( Edg ` G ) ) ) ) )
35 34 3imp 
 |-  ( ( G e. FriendGraph /\ V =/= (/) /\ V e. Fin ) -> ( -. 3 < ( # ` V ) -> E. v e. V A. w e. ( V \ { v } ) { v , w } e. ( Edg ` G ) ) )
36 35 com12 
 |-  ( -. 3 < ( # ` V ) -> ( ( G e. FriendGraph /\ V =/= (/) /\ V e. Fin ) -> E. v e. V A. w e. ( V \ { v } ) { v , w } e. ( Edg ` G ) ) )
37 7 36 pm2.61i 
 |-  ( ( G e. FriendGraph /\ V =/= (/) /\ V e. Fin ) -> E. v e. V A. w e. ( V \ { v } ) { v , w } e. ( Edg ` G ) )