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

Proof

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

Metamath Proof Explorer

Theorem friendshipgt3

Proof