Metamath Proof Explorer

Theorem 3cyclfrgr

Description: Every vertex in a friendship graph (with more than 1 vertex) is part of a 3-cycle. (Contributed by Alexander van der Vekens, 19-Nov-2017) (Revised by AV, 2-Apr-2021)

		Ref	Expression
	Hypothesis	3cyclfrgr.v	$⊢ V = Vtx (G)$
	Assertion	3cyclfrgr	$⊢ (G \in FriendGraph \land 1 < \|V\|) \to \forall v \in V \exists f \exists p (f Cycles (G) p \land \|f\| = 3 \land p (0) = v)$

Proof

Step	Hyp	Ref	Expression
1		3cyclfrgr.v	$⊢ V = Vtx (G)$
2		eqid	$⊢ Edg (G) = Edg (G)$
3	1 2	3cyclfrgrrn	$⊢ (G \in FriendGraph \land 1 < \|V\|) \to \forall v \in V \exists b \in V \exists c \in V (\{v, b\} \in Edg (G) \land \{b, c\} \in Edg (G) \land \{c, v\} \in Edg (G))$
4		frgrusgr	$⊢ G \in FriendGraph \to G \in USGraph$
5		usgrumgr	$⊢ G \in USGraph \to G \in UMGraph$
6	4 5	syl	$⊢ G \in FriendGraph \to G \in UMGraph$
7	6	ad4antr	$⊢ ((((G \in FriendGraph \land 1 < \|V\|) \land v \in V) \land (b \in V \land c \in V)) \land (\{v, b\} \in Edg (G) \land \{b, c\} \in Edg (G) \land \{c, v\} \in Edg (G))) \to G \in UMGraph$
8		simpr	$⊢ ((G \in FriendGraph \land 1 < \|V\|) \land v \in V) \to v \in V$
9	8	anim1i	$⊢ (((G \in FriendGraph \land 1 < \|V\|) \land v \in V) \land (b \in V \land c \in V)) \to (v \in V \land (b \in V \land c \in V))$
10		3anass	$⊢ (v \in V \land b \in V \land c \in V) \leftrightarrow (v \in V \land (b \in V \land c \in V))$
11	9 10	sylibr	$⊢ (((G \in FriendGraph \land 1 < \|V\|) \land v \in V) \land (b \in V \land c \in V)) \to (v \in V \land b \in V \land c \in V)$
12	11	adantr	$⊢ ((((G \in FriendGraph \land 1 < \|V\|) \land v \in V) \land (b \in V \land c \in V)) \land (\{v, b\} \in Edg (G) \land \{b, c\} \in Edg (G) \land \{c, v\} \in Edg (G))) \to (v \in V \land b \in V \land c \in V)$
13		simpr	$⊢ ((((G \in FriendGraph \land 1 < \|V\|) \land v \in V) \land (b \in V \land c \in V)) \land (\{v, b\} \in Edg (G) \land \{b, c\} \in Edg (G) \land \{c, v\} \in Edg (G))) \to (\{v, b\} \in Edg (G) \land \{b, c\} \in Edg (G) \land \{c, v\} \in Edg (G))$
14	1 2	umgr3cyclex	$⊢ (G \in UMGraph \land (v \in V \land b \in V \land c \in V) \land (\{v, b\} \in Edg (G) \land \{b, c\} \in Edg (G) \land \{c, v\} \in Edg (G))) \to \exists f \exists p (f Cycles (G) p \land \|f\| = 3 \land p (0) = v)$
15	7 12 13 14	syl3anc	$⊢ ((((G \in FriendGraph \land 1 < \|V\|) \land v \in V) \land (b \in V \land c \in V)) \land (\{v, b\} \in Edg (G) \land \{b, c\} \in Edg (G) \land \{c, v\} \in Edg (G))) \to \exists f \exists p (f Cycles (G) p \land \|f\| = 3 \land p (0) = v)$
16	15	ex	$⊢ (((G \in FriendGraph \land 1 < \|V\|) \land v \in V) \land (b \in V \land c \in V)) \to ((\{v, b\} \in Edg (G) \land \{b, c\} \in Edg (G) \land \{c, v\} \in Edg (G)) \to \exists f \exists p (f Cycles (G) p \land \|f\| = 3 \land p (0) = v))$
17	16	rexlimdvva	$⊢ ((G \in FriendGraph \land 1 < \|V\|) \land v \in V) \to (\exists b \in V \exists c \in V (\{v, b\} \in Edg (G) \land \{b, c\} \in Edg (G) \land \{c, v\} \in Edg (G)) \to \exists f \exists p (f Cycles (G) p \land \|f\| = 3 \land p (0) = v))$
18	17	ralimdva	$⊢ (G \in FriendGraph \land 1 < \|V\|) \to (\forall v \in V \exists b \in V \exists c \in V (\{v, b\} \in Edg (G) \land \{b, c\} \in Edg (G) \land \{c, v\} \in Edg (G)) \to \forall v \in V \exists f \exists p (f Cycles (G) p \land \|f\| = 3 \land p (0) = v))$
19	3 18	mpd	$⊢ (G \in FriendGraph \land 1 < \|V\|) \to \forall v \in V \exists f \exists p (f Cycles (G) p \land \|f\| = 3 \land p (0) = v)$