2pthfrgr

Description: Between any two (different) vertices in a friendship graph, there is a 2-path (simple path of length 2), see Proposition 1(b) of MertziosUnger p. 153 : "A friendship graph G ..., as well as the distance between any two nodes in G is at most two". (Contributed by Alexander van der Vekens, 6-Dec-2017) (Revised by AV, 1-Apr-2021)

		Ref	Expression
	Hypothesis	2pthfrgr.v	$⊢ V = Vtx (G)$
	Assertion	2pthfrgr	$⊢ G \in FriendGraph \to \forall a \in V \forall b \in (V ∖ \{a\}) \exists f \exists p (f (a SPathsOn (G) b) p \land \|f\| = 2)$

Proof

Step	Hyp	Ref	Expression
1		2pthfrgr.v	$⊢ V = Vtx (G)$
2		eqid	$⊢ Edg (G) = Edg (G)$
3	1 2	2pthfrgrrn2	$⊢ G \in FriendGraph \to \forall a \in V \forall b \in (V ∖ \{a\}) \exists m \in V ((\{a, m\} \in Edg (G) \land \{m, b\} \in Edg (G)) \land (a \neq m \land m \neq b))$
4		frgrusgr	$⊢ G \in FriendGraph \to G \in USGraph$
5		usgruhgr	$⊢ G \in USGraph \to G \in UHGraph$
6	4 5	syl	$⊢ G \in FriendGraph \to G \in UHGraph$
7	6	adantr	$⊢ (G \in FriendGraph \land a \in V) \to G \in UHGraph$
8	7	adantr	$⊢ ((G \in FriendGraph \land a \in V) \land b \in (V ∖ \{a\})) \to G \in UHGraph$
9	8	adantr	$⊢ (((G \in FriendGraph \land a \in V) \land b \in (V ∖ \{a\})) \land m \in V) \to G \in UHGraph$
10		simpllr	$⊢ (((G \in FriendGraph \land a \in V) \land b \in (V ∖ \{a\})) \land m \in V) \to a \in V$
11		simpr	$⊢ (((G \in FriendGraph \land a \in V) \land b \in (V ∖ \{a\})) \land m \in V) \to m \in V$
12		eldifi	$⊢ b \in (V ∖ \{a\}) \to b \in V$
13	12	ad2antlr	$⊢ (((G \in FriendGraph \land a \in V) \land b \in (V ∖ \{a\})) \land m \in V) \to b \in V$
14	10 11 13	3jca	$⊢ (((G \in FriendGraph \land a \in V) \land b \in (V ∖ \{a\})) \land m \in V) \to (a \in V \land m \in V \land b \in V)$
15	9 14	jca	$⊢ (((G \in FriendGraph \land a \in V) \land b \in (V ∖ \{a\})) \land m \in V) \to (G \in UHGraph \land (a \in V \land m \in V \land b \in V))$
16	15	adantr	$⊢ ((((G \in FriendGraph \land a \in V) \land b \in (V ∖ \{a\})) \land m \in V) \land ((\{a, m\} \in Edg (G) \land \{m, b\} \in Edg (G)) \land (a \neq m \land m \neq b))) \to (G \in UHGraph \land (a \in V \land m \in V \land b \in V))$
17		simprrl	$⊢ ((((G \in FriendGraph \land a \in V) \land b \in (V ∖ \{a\})) \land m \in V) \land ((\{a, m\} \in Edg (G) \land \{m, b\} \in Edg (G)) \land (a \neq m \land m \neq b))) \to a \neq m$
18		eldifsn	$⊢ b \in (V ∖ \{a\}) \leftrightarrow (b \in V \land b \neq a)$
19		necom	$⊢ b \neq a \leftrightarrow a \neq b$
20	19	biimpi	$⊢ b \neq a \to a \neq b$
21	18 20	simplbiim	$⊢ b \in (V ∖ \{a\}) \to a \neq b$
22	21	ad3antlr	$⊢ ((((G \in FriendGraph \land a \in V) \land b \in (V ∖ \{a\})) \land m \in V) \land ((\{a, m\} \in Edg (G) \land \{m, b\} \in Edg (G)) \land (a \neq m \land m \neq b))) \to a \neq b$
23		simprrr	$⊢ ((((G \in FriendGraph \land a \in V) \land b \in (V ∖ \{a\})) \land m \in V) \land ((\{a, m\} \in Edg (G) \land \{m, b\} \in Edg (G)) \land (a \neq m \land m \neq b))) \to m \neq b$
24		simprl	$⊢ ((((G \in FriendGraph \land a \in V) \land b \in (V ∖ \{a\})) \land m \in V) \land ((\{a, m\} \in Edg (G) \land \{m, b\} \in Edg (G)) \land (a \neq m \land m \neq b))) \to (\{a, m\} \in Edg (G) \land \{m, b\} \in Edg (G))$
25	1 2	2pthon3v	$⊢ ((G \in UHGraph \land (a \in V \land m \in V \land b \in V)) \land (a \neq m \land a \neq b \land m \neq b) \land (\{a, m\} \in Edg (G) \land \{m, b\} \in Edg (G))) \to \exists f \exists p (f (a SPathsOn (G) b) p \land \|f\| = 2)$
26	16 17 22 23 24 25	syl131anc	$⊢ ((((G \in FriendGraph \land a \in V) \land b \in (V ∖ \{a\})) \land m \in V) \land ((\{a, m\} \in Edg (G) \land \{m, b\} \in Edg (G)) \land (a \neq m \land m \neq b))) \to \exists f \exists p (f (a SPathsOn (G) b) p \land \|f\| = 2)$
27	26	rexlimdva2	$⊢ ((G \in FriendGraph \land a \in V) \land b \in (V ∖ \{a\})) \to (\exists m \in V ((\{a, m\} \in Edg (G) \land \{m, b\} \in Edg (G)) \land (a \neq m \land m \neq b)) \to \exists f \exists p (f (a SPathsOn (G) b) p \land \|f\| = 2))$
28	27	ralimdva	$⊢ (G \in FriendGraph \land a \in V) \to (\forall b \in (V ∖ \{a\}) \exists m \in V ((\{a, m\} \in Edg (G) \land \{m, b\} \in Edg (G)) \land (a \neq m \land m \neq b)) \to \forall b \in (V ∖ \{a\}) \exists f \exists p (f (a SPathsOn (G) b) p \land \|f\| = 2))$
29	28	ralimdva	$⊢ G \in FriendGraph \to (\forall a \in V \forall b \in (V ∖ \{a\}) \exists m \in V ((\{a, m\} \in Edg (G) \land \{m, b\} \in Edg (G)) \land (a \neq m \land m \neq b)) \to \forall a \in V \forall b \in (V ∖ \{a\}) \exists f \exists p (f (a SPathsOn (G) b) p \land \|f\| = 2))$
30	3 29	mpd	$⊢ G \in FriendGraph \to \forall a \in V \forall b \in (V ∖ \{a\}) \exists f \exists p (f (a SPathsOn (G) b) p \land \|f\| = 2)$

Metamath Proof Explorer

Theorem 2pthfrgr

Proof