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 \in FriendGraph \land V \neq \emptyset \land V \in Fin) \to \exists v \in V \forall w \in (V ∖ \{v\}) \{v, w\} \in Edg (G)$

Proof

Step	Hyp	Ref	Expression
1		friendship.v	$⊢ V = Vtx (G)$
2		simpr1	$⊢ (3 < \|V\| \land (G \in FriendGraph \land V \neq \emptyset \land V \in Fin)) \to G \in FriendGraph$
3		simpr3	$⊢ (3 < \|V\| \land (G \in FriendGraph \land V \neq \emptyset \land V \in Fin)) \to V \in Fin$
4		simpl	$⊢ (3 < \|V\| \land (G \in FriendGraph \land V \neq \emptyset \land V \in Fin)) \to 3 < \|V\|$
5	1	friendshipgt3	$⊢ (G \in FriendGraph \land V \in Fin \land 3 < \|V\|) \to \exists v \in V \forall w \in (V ∖ \{v\}) \{v, w\} \in Edg (G)$
6	2 3 4 5	syl3anc	$⊢ (3 < \|V\| \land (G \in FriendGraph \land V \neq \emptyset \land V \in Fin)) \to \exists v \in V \forall w \in (V ∖ \{v\}) \{v, w\} \in Edg (G)$
7	6	ex	$⊢ 3 < \|V\| \to ((G \in FriendGraph \land V \neq \emptyset \land V \in Fin) \to \exists v \in V \forall w \in (V ∖ \{v\}) \{v, w\} \in Edg (G))$
8		hashcl	$⊢ V \in Fin \to \|V\| \in ℕ_{0}$
9		simplr	$⊢ ((\|V\| \in ℕ_{0} \land V \in Fin) \land (\neg 3 < \|V\| \land V \neq \emptyset)) \to V \in Fin$
10		hashge1	$⊢ (V \in Fin \land V \neq \emptyset) \to 1 \leq \|V\|$
11	10	ad2ant2l	$⊢ ((\|V\| \in ℕ_{0} \land V \in Fin) \land (\neg 3 < \|V\| \land V \neq \emptyset)) \to 1 \leq \|V\|$
12		nn0re	$⊢ \|V\| \in ℕ_{0} \to \|V\| \in ℝ$
13		3re	$⊢ 3 \in ℝ$
14		lenlt	$⊢ (\|V\| \in ℝ \land 3 \in ℝ) \to (\|V\| \leq 3 \leftrightarrow \neg 3 < \|V\|)$
15	12 13 14	sylancl	$⊢ \|V\| \in ℕ_{0} \to (\|V\| \leq 3 \leftrightarrow \neg 3 < \|V\|)$
16	15	biimprd	$⊢ \|V\| \in ℕ_{0} \to (\neg 3 < \|V\| \to \|V\| \leq 3)$
17	16	adantr	$⊢ (\|V\| \in ℕ_{0} \land V \in Fin) \to (\neg 3 < \|V\| \to \|V\| \leq 3)$
18	17	com12	$⊢ \neg 3 < \|V\| \to ((\|V\| \in ℕ_{0} \land V \in Fin) \to \|V\| \leq 3)$
19	18	adantr	$⊢ (\neg 3 < \|V\| \land V \neq \emptyset) \to ((\|V\| \in ℕ_{0} \land V \in Fin) \to \|V\| \leq 3)$
20	19	impcom	$⊢ ((\|V\| \in ℕ_{0} \land V \in Fin) \land (\neg 3 < \|V\| \land V \neq \emptyset)) \to \|V\| \leq 3$
21	9 11 20	3jca	$⊢ ((\|V\| \in ℕ_{0} \land V \in Fin) \land (\neg 3 < \|V\| \land V \neq \emptyset)) \to (V \in Fin \land 1 \leq \|V\| \land \|V\| \leq 3)$
22	21	exp31	$⊢ \|V\| \in ℕ_{0} \to (V \in Fin \to ((\neg 3 < \|V\| \land V \neq \emptyset) \to (V \in Fin \land 1 \leq \|V\| \land \|V\| \leq 3)))$
23	8 22	mpcom	$⊢ V \in Fin \to ((\neg 3 < \|V\| \land V \neq \emptyset) \to (V \in Fin \land 1 \leq \|V\| \land \|V\| \leq 3))$
24	23	impcom	$⊢ ((\neg 3 < \|V\| \land V \neq \emptyset) \land V \in Fin) \to (V \in Fin \land 1 \leq \|V\| \land \|V\| \leq 3)$
25		hash1to3	$⊢ (V \in Fin \land 1 \leq \|V\| \land \|V\| \leq 3) \to \exists a \exists b \exists c (V = \{a\} \lor V = \{a, b\} \lor V = \{a, b, c\})$
26		vex	$⊢ a \in V$
27		eqid	$⊢ Edg (G) = Edg (G)$
28	1 27	1to3vfriendship	$⊢ (a \in V \land (V = \{a\} \lor V = \{a, b\} \lor V = \{a, b, c\})) \to (G \in FriendGraph \to \exists v \in V \forall w \in (V ∖ \{v\}) \{v, w\} \in Edg (G))$
29	26 28	mpan	$⊢ (V = \{a\} \lor V = \{a, b\} \lor V = \{a, b, c\}) \to (G \in FriendGraph \to \exists v \in V \forall w \in (V ∖ \{v\}) \{v, w\} \in Edg (G))$
30	29	exlimiv	$⊢ \exists c (V = \{a\} \lor V = \{a, b\} \lor V = \{a, b, c\}) \to (G \in FriendGraph \to \exists v \in V \forall w \in (V ∖ \{v\}) \{v, w\} \in Edg (G))$
31	30	exlimivv	$⊢ \exists a \exists b \exists c (V = \{a\} \lor V = \{a, b\} \lor V = \{a, b, c\}) \to (G \in FriendGraph \to \exists v \in V \forall w \in (V ∖ \{v\}) \{v, w\} \in Edg (G))$
32	24 25 31	3syl	$⊢ ((\neg 3 < \|V\| \land V \neq \emptyset) \land V \in Fin) \to (G \in FriendGraph \to \exists v \in V \forall w \in (V ∖ \{v\}) \{v, w\} \in Edg (G))$
33	32	exp31	$⊢ \neg 3 < \|V\| \to (V \neq \emptyset \to (V \in Fin \to (G \in FriendGraph \to \exists v \in V \forall w \in (V ∖ \{v\}) \{v, w\} \in Edg (G))))$
34	33	com14	$⊢ G \in FriendGraph \to (V \neq \emptyset \to (V \in Fin \to (\neg 3 < \|V\| \to \exists v \in V \forall w \in (V ∖ \{v\}) \{v, w\} \in Edg (G))))$
35	34	3imp	$⊢ (G \in FriendGraph \land V \neq \emptyset \land V \in Fin) \to (\neg 3 < \|V\| \to \exists v \in V \forall w \in (V ∖ \{v\}) \{v, w\} \in Edg (G))$
36	35	com12	$⊢ \neg 3 < \|V\| \to ((G \in FriendGraph \land V \neq \emptyset \land V \in Fin) \to \exists v \in V \forall w \in (V ∖ \{v\}) \{v, w\} \in Edg (G))$
37	7 36	pm2.61i	$⊢ (G \in FriendGraph \land V \neq \emptyset \land V \in Fin) \to \exists v \in V \forall w \in (V ∖ \{v\}) \{v, w\} \in Edg (G)$

Metamath Proof Explorer

Theorem friendship

Proof