2pthon3v

Description: For a vertex adjacent to two other vertices there is a simple path of length 2 between these other vertices in a hypergraph. (Contributed by Alexander van der Vekens, 4-Dec-2017) (Revised by AV, 24-Jan-2021)

	Ref	Expression
Hypotheses	2pthon3v.v	$⊢ V = Vtx (G)$
	2pthon3v.e	$⊢ E = Edg (G)$
Assertion	2pthon3v	$⊢ ((G \in UHGraph \land (A \in V \land B \in V \land C \in V)) \land (A \neq B \land A \neq C \land B \neq C) \land (\{A, B\} \in E \land \{B, C\} \in E)) \to \exists f \exists p (f (A SPathsOn (G) C) p \land \|f\| = 2)$

Proof

Step	Hyp	Ref	Expression
1		2pthon3v.v	$⊢ V = Vtx (G)$
2		2pthon3v.e	$⊢ E = Edg (G)$
3		edgval	$⊢ Edg (G) = ran iEdg (G)$
4	2 3	eqtri	$⊢ E = ran iEdg (G)$
5	4	eleq2i	$⊢ \{A, B\} \in E \leftrightarrow \{A, B\} \in ran iEdg (G)$
6		eqid	$⊢ iEdg (G) = iEdg (G)$
7	1 6	uhgrf	$⊢ G \in UHGraph \to iEdg (G) : dom iEdg (G) ⟶ 𝒫 V ∖ \{\emptyset\}$
8	7	ffnd	$⊢ G \in UHGraph \to iEdg (G) Fn dom iEdg (G)$
9		fvelrnb	$⊢ iEdg (G) Fn dom iEdg (G) \to (\{A, B\} \in ran iEdg (G) \leftrightarrow \exists i \in dom iEdg (G) iEdg (G) (i) = \{A, B\})$
10	8 9	syl	$⊢ G \in UHGraph \to (\{A, B\} \in ran iEdg (G) \leftrightarrow \exists i \in dom iEdg (G) iEdg (G) (i) = \{A, B\})$
11	5 10	syl5bb	$⊢ G \in UHGraph \to (\{A, B\} \in E \leftrightarrow \exists i \in dom iEdg (G) iEdg (G) (i) = \{A, B\})$
12	4	eleq2i	$⊢ \{B, C\} \in E \leftrightarrow \{B, C\} \in ran iEdg (G)$
13		fvelrnb	$⊢ iEdg (G) Fn dom iEdg (G) \to (\{B, C\} \in ran iEdg (G) \leftrightarrow \exists j \in dom iEdg (G) iEdg (G) (j) = \{B, C\})$
14	8 13	syl	$⊢ G \in UHGraph \to (\{B, C\} \in ran iEdg (G) \leftrightarrow \exists j \in dom iEdg (G) iEdg (G) (j) = \{B, C\})$
15	12 14	syl5bb	$⊢ G \in UHGraph \to (\{B, C\} \in E \leftrightarrow \exists j \in dom iEdg (G) iEdg (G) (j) = \{B, C\})$
16	11 15	anbi12d	$⊢ G \in UHGraph \to ((\{A, B\} \in E \land \{B, C\} \in E) \leftrightarrow (\exists i \in dom iEdg (G) iEdg (G) (i) = \{A, B\} \land \exists j \in dom iEdg (G) iEdg (G) (j) = \{B, C\}))$
17	16	adantr	$⊢ (G \in UHGraph \land (A \in V \land B \in V \land C \in V)) \to ((\{A, B\} \in E \land \{B, C\} \in E) \leftrightarrow (\exists i \in dom iEdg (G) iEdg (G) (i) = \{A, B\} \land \exists j \in dom iEdg (G) iEdg (G) (j) = \{B, C\}))$
18	17	adantr	$⊢ ((G \in UHGraph \land (A \in V \land B \in V \land C \in V)) \land (A \neq B \land A \neq C \land B \neq C)) \to ((\{A, B\} \in E \land \{B, C\} \in E) \leftrightarrow (\exists i \in dom iEdg (G) iEdg (G) (i) = \{A, B\} \land \exists j \in dom iEdg (G) iEdg (G) (j) = \{B, C\}))$
19		reeanv	$⊢ \exists i \in dom iEdg (G) \exists j \in dom iEdg (G) (iEdg (G) (i) = \{A, B\} \land iEdg (G) (j) = \{B, C\}) \leftrightarrow (\exists i \in dom iEdg (G) iEdg (G) (i) = \{A, B\} \land \exists j \in dom iEdg (G) iEdg (G) (j) = \{B, C\})$
20	18 19	bitr4di	$⊢ ((G \in UHGraph \land (A \in V \land B \in V \land C \in V)) \land (A \neq B \land A \neq C \land B \neq C)) \to ((\{A, B\} \in E \land \{B, C\} \in E) \leftrightarrow \exists i \in dom iEdg (G) \exists j \in dom iEdg (G) (iEdg (G) (i) = \{A, B\} \land iEdg (G) (j) = \{B, C\}))$
21		df-s2	$⊢ ⟨“ i j ”⟩ = ⟨“ i ”⟩ ++ ⟨“ j ”⟩$
22	21	ovexi	$⊢ ⟨“ i j ”⟩ \in V$
23		df-s3	$⊢ ⟨“ A B C ”⟩ = ⟨“ A B ”⟩ ++ ⟨“ C ”⟩$
24	23	ovexi	$⊢ ⟨“ A B C ”⟩ \in V$
25	22 24	pm3.2i	$⊢ (⟨“ i j ”⟩ \in V \land ⟨“ A B C ”⟩ \in V)$
26		eqid	$⊢ ⟨“ A B C ”⟩ = ⟨“ A B C ”⟩$
27		eqid	$⊢ ⟨“ i j ”⟩ = ⟨“ i j ”⟩$
28		simp-4r	$⊢ ((((G \in UHGraph \land (A \in V \land B \in V \land C \in V)) \land (A \neq B \land A \neq C \land B \neq C)) \land (i \in dom iEdg (G) \land j \in dom iEdg (G))) \land (iEdg (G) (i) = \{A, B\} \land iEdg (G) (j) = \{B, C\})) \to (A \in V \land B \in V \land C \in V)$
29		3simpb	$⊢ (A \neq B \land A \neq C \land B \neq C) \to (A \neq B \land B \neq C)$
30	29	ad3antlr	$⊢ ((((G \in UHGraph \land (A \in V \land B \in V \land C \in V)) \land (A \neq B \land A \neq C \land B \neq C)) \land (i \in dom iEdg (G) \land j \in dom iEdg (G))) \land (iEdg (G) (i) = \{A, B\} \land iEdg (G) (j) = \{B, C\})) \to (A \neq B \land B \neq C)$
31		eqimss2	$⊢ iEdg (G) (i) = \{A, B\} \to \{A, B\} \subseteq iEdg (G) (i)$
32		eqimss2	$⊢ iEdg (G) (j) = \{B, C\} \to \{B, C\} \subseteq iEdg (G) (j)$
33	31 32	anim12i	$⊢ (iEdg (G) (i) = \{A, B\} \land iEdg (G) (j) = \{B, C\}) \to (\{A, B\} \subseteq iEdg (G) (i) \land \{B, C\} \subseteq iEdg (G) (j))$
34	33	adantl	$⊢ ((((G \in UHGraph \land (A \in V \land B \in V \land C \in V)) \land (A \neq B \land A \neq C \land B \neq C)) \land (i \in dom iEdg (G) \land j \in dom iEdg (G))) \land (iEdg (G) (i) = \{A, B\} \land iEdg (G) (j) = \{B, C\})) \to (\{A, B\} \subseteq iEdg (G) (i) \land \{B, C\} \subseteq iEdg (G) (j))$
35		fveqeq2	$⊢ i = j \to (iEdg (G) (i) = \{A, B\} \leftrightarrow iEdg (G) (j) = \{A, B\})$
36	35	anbi1d	$⊢ i = j \to ((iEdg (G) (i) = \{A, B\} \land iEdg (G) (j) = \{B, C\}) \leftrightarrow (iEdg (G) (j) = \{A, B\} \land iEdg (G) (j) = \{B, C\}))$
37		eqtr2	$⊢ (iEdg (G) (j) = \{A, B\} \land iEdg (G) (j) = \{B, C\}) \to \{A, B\} = \{B, C\}$
38		3simpa	$⊢ (A \in V \land B \in V \land C \in V) \to (A \in V \land B \in V)$
39		3simpc	$⊢ (A \in V \land B \in V \land C \in V) \to (B \in V \land C \in V)$
40		preq12bg	$⊢ ((A \in V \land B \in V) \land (B \in V \land C \in V)) \to (\{A, B\} = \{B, C\} \leftrightarrow ((A = B \land B = C) \lor (A = C \land B = B)))$
41	38 39 40	syl2anc	$⊢ (A \in V \land B \in V \land C \in V) \to (\{A, B\} = \{B, C\} \leftrightarrow ((A = B \land B = C) \lor (A = C \land B = B)))$
42		eqneqall	$⊢ A = B \to (A \neq B \to i \neq j)$
43	42	com12	$⊢ A \neq B \to (A = B \to i \neq j)$
44	43	3ad2ant1	$⊢ (A \neq B \land A \neq C \land B \neq C) \to (A = B \to i \neq j)$
45	44	com12	$⊢ A = B \to ((A \neq B \land A \neq C \land B \neq C) \to i \neq j)$
46	45	adantr	$⊢ (A = B \land B = C) \to ((A \neq B \land A \neq C \land B \neq C) \to i \neq j)$
47		eqneqall	$⊢ A = C \to (A \neq C \to i \neq j)$
48	47	com12	$⊢ A \neq C \to (A = C \to i \neq j)$
49	48	3ad2ant2	$⊢ (A \neq B \land A \neq C \land B \neq C) \to (A = C \to i \neq j)$
50	49	com12	$⊢ A = C \to ((A \neq B \land A \neq C \land B \neq C) \to i \neq j)$
51	50	adantr	$⊢ (A = C \land B = B) \to ((A \neq B \land A \neq C \land B \neq C) \to i \neq j)$
52	46 51	jaoi	$⊢ ((A = B \land B = C) \lor (A = C \land B = B)) \to ((A \neq B \land A \neq C \land B \neq C) \to i \neq j)$
53	41 52	syl6bi	$⊢ (A \in V \land B \in V \land C \in V) \to (\{A, B\} = \{B, C\} \to ((A \neq B \land A \neq C \land B \neq C) \to i \neq j))$
54	53	com23	$⊢ (A \in V \land B \in V \land C \in V) \to ((A \neq B \land A \neq C \land B \neq C) \to (\{A, B\} = \{B, C\} \to i \neq j))$
55	54	adantl	$⊢ (G \in UHGraph \land (A \in V \land B \in V \land C \in V)) \to ((A \neq B \land A \neq C \land B \neq C) \to (\{A, B\} = \{B, C\} \to i \neq j))$
56	55	imp	$⊢ ((G \in UHGraph \land (A \in V \land B \in V \land C \in V)) \land (A \neq B \land A \neq C \land B \neq C)) \to (\{A, B\} = \{B, C\} \to i \neq j)$
57	56	com12	$⊢ \{A, B\} = \{B, C\} \to (((G \in UHGraph \land (A \in V \land B \in V \land C \in V)) \land (A \neq B \land A \neq C \land B \neq C)) \to i \neq j)$
58	37 57	syl	$⊢ (iEdg (G) (j) = \{A, B\} \land iEdg (G) (j) = \{B, C\}) \to (((G \in UHGraph \land (A \in V \land B \in V \land C \in V)) \land (A \neq B \land A \neq C \land B \neq C)) \to i \neq j)$
59	36 58	syl6bi	$⊢ i = j \to ((iEdg (G) (i) = \{A, B\} \land iEdg (G) (j) = \{B, C\}) \to (((G \in UHGraph \land (A \in V \land B \in V \land C \in V)) \land (A \neq B \land A \neq C \land B \neq C)) \to i \neq j))$
60	59	com23	$⊢ i = j \to (((G \in UHGraph \land (A \in V \land B \in V \land C \in V)) \land (A \neq B \land A \neq C \land B \neq C)) \to ((iEdg (G) (i) = \{A, B\} \land iEdg (G) (j) = \{B, C\}) \to i \neq j))$
61		2a1	$⊢ i \neq j \to (((G \in UHGraph \land (A \in V \land B \in V \land C \in V)) \land (A \neq B \land A \neq C \land B \neq C)) \to ((iEdg (G) (i) = \{A, B\} \land iEdg (G) (j) = \{B, C\}) \to i \neq j))$
62	60 61	pm2.61ine	$⊢ ((G \in UHGraph \land (A \in V \land B \in V \land C \in V)) \land (A \neq B \land A \neq C \land B \neq C)) \to ((iEdg (G) (i) = \{A, B\} \land iEdg (G) (j) = \{B, C\}) \to i \neq j)$
63	62	adantr	$⊢ (((G \in UHGraph \land (A \in V \land B \in V \land C \in V)) \land (A \neq B \land A \neq C \land B \neq C)) \land (i \in dom iEdg (G) \land j \in dom iEdg (G))) \to ((iEdg (G) (i) = \{A, B\} \land iEdg (G) (j) = \{B, C\}) \to i \neq j)$
64	63	imp	$⊢ ((((G \in UHGraph \land (A \in V \land B \in V \land C \in V)) \land (A \neq B \land A \neq C \land B \neq C)) \land (i \in dom iEdg (G) \land j \in dom iEdg (G))) \land (iEdg (G) (i) = \{A, B\} \land iEdg (G) (j) = \{B, C\})) \to i \neq j$
65		simplr2	$⊢ (((G \in UHGraph \land (A \in V \land B \in V \land C \in V)) \land (A \neq B \land A \neq C \land B \neq C)) \land (i \in dom iEdg (G) \land j \in dom iEdg (G))) \to A \neq C$
66	65	adantr	$⊢ ((((G \in UHGraph \land (A \in V \land B \in V \land C \in V)) \land (A \neq B \land A \neq C \land B \neq C)) \land (i \in dom iEdg (G) \land j \in dom iEdg (G))) \land (iEdg (G) (i) = \{A, B\} \land iEdg (G) (j) = \{B, C\})) \to A \neq C$
67	26 27 28 30 34 1 6 64 66	2pthond	$⊢ ((((G \in UHGraph \land (A \in V \land B \in V \land C \in V)) \land (A \neq B \land A \neq C \land B \neq C)) \land (i \in dom iEdg (G) \land j \in dom iEdg (G))) \land (iEdg (G) (i) = \{A, B\} \land iEdg (G) (j) = \{B, C\})) \to ⟨“ i j ”⟩ (A SPathsOn (G) C) ⟨“ A B C ”⟩$
68		s2len	$⊢ \|⟨“ i j ”⟩\| = 2$
69	67 68	jctir	$⊢ ((((G \in UHGraph \land (A \in V \land B \in V \land C \in V)) \land (A \neq B \land A \neq C \land B \neq C)) \land (i \in dom iEdg (G) \land j \in dom iEdg (G))) \land (iEdg (G) (i) = \{A, B\} \land iEdg (G) (j) = \{B, C\})) \to (⟨“ i j ”⟩ (A SPathsOn (G) C) ⟨“ A B C ”⟩ \land \|⟨“ i j ”⟩\| = 2)$
70		breq12	$⊢ (f = ⟨“ i j ”⟩ \land p = ⟨“ A B C ”⟩) \to (f (A SPathsOn (G) C) p \leftrightarrow ⟨“ i j ”⟩ (A SPathsOn (G) C) ⟨“ A B C ”⟩)$
71		fveqeq2	$⊢ f = ⟨“ i j ”⟩ \to (\|f\| = 2 \leftrightarrow \|⟨“ i j ”⟩\| = 2)$
72	71	adantr	$⊢ (f = ⟨“ i j ”⟩ \land p = ⟨“ A B C ”⟩) \to (\|f\| = 2 \leftrightarrow \|⟨“ i j ”⟩\| = 2)$
73	70 72	anbi12d	$⊢ (f = ⟨“ i j ”⟩ \land p = ⟨“ A B C ”⟩) \to ((f (A SPathsOn (G) C) p \land \|f\| = 2) \leftrightarrow (⟨“ i j ”⟩ (A SPathsOn (G) C) ⟨“ A B C ”⟩ \land \|⟨“ i j ”⟩\| = 2))$
74	73	spc2egv	$⊢ (⟨“ i j ”⟩ \in V \land ⟨“ A B C ”⟩ \in V) \to ((⟨“ i j ”⟩ (A SPathsOn (G) C) ⟨“ A B C ”⟩ \land \|⟨“ i j ”⟩\| = 2) \to \exists f \exists p (f (A SPathsOn (G) C) p \land \|f\| = 2))$
75	25 69 74	mpsyl	$⊢ ((((G \in UHGraph \land (A \in V \land B \in V \land C \in V)) \land (A \neq B \land A \neq C \land B \neq C)) \land (i \in dom iEdg (G) \land j \in dom iEdg (G))) \land (iEdg (G) (i) = \{A, B\} \land iEdg (G) (j) = \{B, C\})) \to \exists f \exists p (f (A SPathsOn (G) C) p \land \|f\| = 2)$
76	75	ex	$⊢ (((G \in UHGraph \land (A \in V \land B \in V \land C \in V)) \land (A \neq B \land A \neq C \land B \neq C)) \land (i \in dom iEdg (G) \land j \in dom iEdg (G))) \to ((iEdg (G) (i) = \{A, B\} \land iEdg (G) (j) = \{B, C\}) \to \exists f \exists p (f (A SPathsOn (G) C) p \land \|f\| = 2))$
77	76	rexlimdvva	$⊢ ((G \in UHGraph \land (A \in V \land B \in V \land C \in V)) \land (A \neq B \land A \neq C \land B \neq C)) \to (\exists i \in dom iEdg (G) \exists j \in dom iEdg (G) (iEdg (G) (i) = \{A, B\} \land iEdg (G) (j) = \{B, C\}) \to \exists f \exists p (f (A SPathsOn (G) C) p \land \|f\| = 2))$
78	20 77	sylbid	$⊢ ((G \in UHGraph \land (A \in V \land B \in V \land C \in V)) \land (A \neq B \land A \neq C \land B \neq C)) \to ((\{A, B\} \in E \land \{B, C\} \in E) \to \exists f \exists p (f (A SPathsOn (G) C) p \land \|f\| = 2))$
79	78	3impia	$⊢ ((G \in UHGraph \land (A \in V \land B \in V \land C \in V)) \land (A \neq B \land A \neq C \land B \neq C) \land (\{A, B\} \in E \land \{B, C\} \in E)) \to \exists f \exists p (f (A SPathsOn (G) C) p \land \|f\| = 2)$

Metamath Proof Explorer

Theorem 2pthon3v

Proof