usgr2pth0

Description: In a simply graph, there is a path of length 2 iff there are three distinct vertices so that one of them is connected to each of the two others by an edge. (Contributed by Alexander van der Vekens, 27-Jan-2018) (Revised by AV, 5-Jun-2021)

	Ref	Expression
Hypotheses	usgr2pthlem.v	$⊢ V = Vtx (G)$
	usgr2pthlem.i	$⊢ I = iEdg (G)$
Assertion	usgr2pth0	$⊢ G \in USGraph \to ((F Paths (G) P \land \|F\| = 2) \leftrightarrow (F : (0 ..^2) \underset{1-1}{⟶} dom I \land P : (0 \dots 2) \underset{1-1}{⟶} V \land \exists x \in V \exists y \in (V ∖ \{x\}) \exists z \in (V ∖ \{x, y\}) ((P (0) = x \land P (1) = z \land P (2) = y) \land (I (F (0)) = \{x, z\} \land I (F (1)) = \{z, y\}))))$

Proof

Step	Hyp	Ref	Expression
1		usgr2pthlem.v	$⊢ V = Vtx (G)$
2		usgr2pthlem.i	$⊢ I = iEdg (G)$
3	1 2	usgr2pth	$⊢ G \in USGraph \to ((F Paths (G) P \land \|F\| = 2) \leftrightarrow (F : (0 ..^2) \underset{1-1}{⟶} dom I \land P : (0 \dots 2) \underset{1-1}{⟶} V \land \exists x \in V \exists z \in (V ∖ \{x\}) \exists y \in (V ∖ \{x, z\}) ((P (0) = x \land P (1) = z \land P (2) = y) \land (I (F (0)) = \{x, z\} \land I (F (1)) = \{z, y\}))))$
4		r19.42v	$⊢ \exists y \in (V ∖ \{x, z\}) (z \neq x \land ((P (0) = x \land P (1) = z \land P (2) = y) \land (I (F (0)) = \{x, z\} \land I (F (1)) = \{z, y\}))) \leftrightarrow (z \neq x \land \exists y \in (V ∖ \{x, z\}) ((P (0) = x \land P (1) = z \land P (2) = y) \land (I (F (0)) = \{x, z\} \land I (F (1)) = \{z, y\})))$
5		rexdifpr	$⊢ \exists y \in (V ∖ \{x, z\}) (z \neq x \land ((P (0) = x \land P (1) = z \land P (2) = y) \land (I (F (0)) = \{x, z\} \land I (F (1)) = \{z, y\}))) \leftrightarrow \exists y \in V (y \neq x \land y \neq z \land (z \neq x \land ((P (0) = x \land P (1) = z \land P (2) = y) \land (I (F (0)) = \{x, z\} \land I (F (1)) = \{z, y\}))))$
6	4 5	bitr3i	$⊢ (z \neq x \land \exists y \in (V ∖ \{x, z\}) ((P (0) = x \land P (1) = z \land P (2) = y) \land (I (F (0)) = \{x, z\} \land I (F (1)) = \{z, y\}))) \leftrightarrow \exists y \in V (y \neq x \land y \neq z \land (z \neq x \land ((P (0) = x \land P (1) = z \land P (2) = y) \land (I (F (0)) = \{x, z\} \land I (F (1)) = \{z, y\}))))$
7	6	rexbii	$⊢ \exists z \in V (z \neq x \land \exists y \in (V ∖ \{x, z\}) ((P (0) = x \land P (1) = z \land P (2) = y) \land (I (F (0)) = \{x, z\} \land I (F (1)) = \{z, y\}))) \leftrightarrow \exists z \in V \exists y \in V (y \neq x \land y \neq z \land (z \neq x \land ((P (0) = x \land P (1) = z \land P (2) = y) \land (I (F (0)) = \{x, z\} \land I (F (1)) = \{z, y\}))))$
8		rexcom	$⊢ \exists z \in V \exists y \in V (y \neq x \land y \neq z \land (z \neq x \land ((P (0) = x \land P (1) = z \land P (2) = y) \land (I (F (0)) = \{x, z\} \land I (F (1)) = \{z, y\})))) \leftrightarrow \exists y \in V \exists z \in V (y \neq x \land y \neq z \land (z \neq x \land ((P (0) = x \land P (1) = z \land P (2) = y) \land (I (F (0)) = \{x, z\} \land I (F (1)) = \{z, y\}))))$
9		df-3an	$⊢ (y \neq x \land y \neq z \land (z \neq x \land ((P (0) = x \land P (1) = z \land P (2) = y) \land (I (F (0)) = \{x, z\} \land I (F (1)) = \{z, y\})))) \leftrightarrow ((y \neq x \land y \neq z) \land (z \neq x \land ((P (0) = x \land P (1) = z \land P (2) = y) \land (I (F (0)) = \{x, z\} \land I (F (1)) = \{z, y\}))))$
10		anass	$⊢ (((y \neq x \land y \neq z) \land z \neq x) \land ((P (0) = x \land P (1) = z \land P (2) = y) \land (I (F (0)) = \{x, z\} \land I (F (1)) = \{z, y\}))) \leftrightarrow ((y \neq x \land y \neq z) \land (z \neq x \land ((P (0) = x \land P (1) = z \land P (2) = y) \land (I (F (0)) = \{x, z\} \land I (F (1)) = \{z, y\}))))$
11		anass	$⊢ (((z \neq x \land z \neq y) \land y \neq x) \land ((P (0) = x \land P (1) = z \land P (2) = y) \land (I (F (0)) = \{x, z\} \land I (F (1)) = \{z, y\}))) \leftrightarrow ((z \neq x \land z \neq y) \land (y \neq x \land ((P (0) = x \land P (1) = z \land P (2) = y) \land (I (F (0)) = \{x, z\} \land I (F (1)) = \{z, y\}))))$
12		anass	$⊢ ((y \neq x \land y \neq z) \land z \neq x) \leftrightarrow (y \neq x \land (y \neq z \land z \neq x))$
13		ancom	$⊢ (y \neq x \land (y \neq z \land z \neq x)) \leftrightarrow ((y \neq z \land z \neq x) \land y \neq x)$
14		necom	$⊢ y \neq z \leftrightarrow z \neq y$
15	14	anbi2ci	$⊢ (y \neq z \land z \neq x) \leftrightarrow (z \neq x \land z \neq y)$
16	15	anbi1i	$⊢ ((y \neq z \land z \neq x) \land y \neq x) \leftrightarrow ((z \neq x \land z \neq y) \land y \neq x)$
17	12 13 16	3bitri	$⊢ ((y \neq x \land y \neq z) \land z \neq x) \leftrightarrow ((z \neq x \land z \neq y) \land y \neq x)$
18	17	anbi1i	$⊢ (((y \neq x \land y \neq z) \land z \neq x) \land ((P (0) = x \land P (1) = z \land P (2) = y) \land (I (F (0)) = \{x, z\} \land I (F (1)) = \{z, y\}))) \leftrightarrow (((z \neq x \land z \neq y) \land y \neq x) \land ((P (0) = x \land P (1) = z \land P (2) = y) \land (I (F (0)) = \{x, z\} \land I (F (1)) = \{z, y\})))$
19		df-3an	$⊢ (z \neq x \land z \neq y \land (y \neq x \land ((P (0) = x \land P (1) = z \land P (2) = y) \land (I (F (0)) = \{x, z\} \land I (F (1)) = \{z, y\})))) \leftrightarrow ((z \neq x \land z \neq y) \land (y \neq x \land ((P (0) = x \land P (1) = z \land P (2) = y) \land (I (F (0)) = \{x, z\} \land I (F (1)) = \{z, y\}))))$
20	11 18 19	3bitr4i	$⊢ (((y \neq x \land y \neq z) \land z \neq x) \land ((P (0) = x \land P (1) = z \land P (2) = y) \land (I (F (0)) = \{x, z\} \land I (F (1)) = \{z, y\}))) \leftrightarrow (z \neq x \land z \neq y \land (y \neq x \land ((P (0) = x \land P (1) = z \land P (2) = y) \land (I (F (0)) = \{x, z\} \land I (F (1)) = \{z, y\}))))$
21	9 10 20	3bitr2i	$⊢ (y \neq x \land y \neq z \land (z \neq x \land ((P (0) = x \land P (1) = z \land P (2) = y) \land (I (F (0)) = \{x, z\} \land I (F (1)) = \{z, y\})))) \leftrightarrow (z \neq x \land z \neq y \land (y \neq x \land ((P (0) = x \land P (1) = z \land P (2) = y) \land (I (F (0)) = \{x, z\} \land I (F (1)) = \{z, y\}))))$
22	21	rexbii	$⊢ \exists z \in V (y \neq x \land y \neq z \land (z \neq x \land ((P (0) = x \land P (1) = z \land P (2) = y) \land (I (F (0)) = \{x, z\} \land I (F (1)) = \{z, y\})))) \leftrightarrow \exists z \in V (z \neq x \land z \neq y \land (y \neq x \land ((P (0) = x \land P (1) = z \land P (2) = y) \land (I (F (0)) = \{x, z\} \land I (F (1)) = \{z, y\}))))$
23		rexdifpr	$⊢ \exists z \in (V ∖ \{x, y\}) (y \neq x \land ((P (0) = x \land P (1) = z \land P (2) = y) \land (I (F (0)) = \{x, z\} \land I (F (1)) = \{z, y\}))) \leftrightarrow \exists z \in V (z \neq x \land z \neq y \land (y \neq x \land ((P (0) = x \land P (1) = z \land P (2) = y) \land (I (F (0)) = \{x, z\} \land I (F (1)) = \{z, y\}))))$
24		r19.42v	$⊢ \exists z \in (V ∖ \{x, y\}) (y \neq x \land ((P (0) = x \land P (1) = z \land P (2) = y) \land (I (F (0)) = \{x, z\} \land I (F (1)) = \{z, y\}))) \leftrightarrow (y \neq x \land \exists z \in (V ∖ \{x, y\}) ((P (0) = x \land P (1) = z \land P (2) = y) \land (I (F (0)) = \{x, z\} \land I (F (1)) = \{z, y\})))$
25	22 23 24	3bitr2i	$⊢ \exists z \in V (y \neq x \land y \neq z \land (z \neq x \land ((P (0) = x \land P (1) = z \land P (2) = y) \land (I (F (0)) = \{x, z\} \land I (F (1)) = \{z, y\})))) \leftrightarrow (y \neq x \land \exists z \in (V ∖ \{x, y\}) ((P (0) = x \land P (1) = z \land P (2) = y) \land (I (F (0)) = \{x, z\} \land I (F (1)) = \{z, y\})))$
26	25	rexbii	$⊢ \exists y \in V \exists z \in V (y \neq x \land y \neq z \land (z \neq x \land ((P (0) = x \land P (1) = z \land P (2) = y) \land (I (F (0)) = \{x, z\} \land I (F (1)) = \{z, y\})))) \leftrightarrow \exists y \in V (y \neq x \land \exists z \in (V ∖ \{x, y\}) ((P (0) = x \land P (1) = z \land P (2) = y) \land (I (F (0)) = \{x, z\} \land I (F (1)) = \{z, y\})))$
27	7 8 26	3bitri	$⊢ \exists z \in V (z \neq x \land \exists y \in (V ∖ \{x, z\}) ((P (0) = x \land P (1) = z \land P (2) = y) \land (I (F (0)) = \{x, z\} \land I (F (1)) = \{z, y\}))) \leftrightarrow \exists y \in V (y \neq x \land \exists z \in (V ∖ \{x, y\}) ((P (0) = x \land P (1) = z \land P (2) = y) \land (I (F (0)) = \{x, z\} \land I (F (1)) = \{z, y\})))$
28		rexdifsn	$⊢ \exists z \in (V ∖ \{x\}) \exists y \in (V ∖ \{x, z\}) ((P (0) = x \land P (1) = z \land P (2) = y) \land (I (F (0)) = \{x, z\} \land I (F (1)) = \{z, y\})) \leftrightarrow \exists z \in V (z \neq x \land \exists y \in (V ∖ \{x, z\}) ((P (0) = x \land P (1) = z \land P (2) = y) \land (I (F (0)) = \{x, z\} \land I (F (1)) = \{z, y\})))$
29		rexdifsn	$⊢ \exists y \in (V ∖ \{x\}) \exists z \in (V ∖ \{x, y\}) ((P (0) = x \land P (1) = z \land P (2) = y) \land (I (F (0)) = \{x, z\} \land I (F (1)) = \{z, y\})) \leftrightarrow \exists y \in V (y \neq x \land \exists z \in (V ∖ \{x, y\}) ((P (0) = x \land P (1) = z \land P (2) = y) \land (I (F (0)) = \{x, z\} \land I (F (1)) = \{z, y\})))$
30	27 28 29	3bitr4i	$⊢ \exists z \in (V ∖ \{x\}) \exists y \in (V ∖ \{x, z\}) ((P (0) = x \land P (1) = z \land P (2) = y) \land (I (F (0)) = \{x, z\} \land I (F (1)) = \{z, y\})) \leftrightarrow \exists y \in (V ∖ \{x\}) \exists z \in (V ∖ \{x, y\}) ((P (0) = x \land P (1) = z \land P (2) = y) \land (I (F (0)) = \{x, z\} \land I (F (1)) = \{z, y\}))$
31	30	a1i	$⊢ (G \in USGraph \land x \in V) \to (\exists z \in (V ∖ \{x\}) \exists y \in (V ∖ \{x, z\}) ((P (0) = x \land P (1) = z \land P (2) = y) \land (I (F (0)) = \{x, z\} \land I (F (1)) = \{z, y\})) \leftrightarrow \exists y \in (V ∖ \{x\}) \exists z \in (V ∖ \{x, y\}) ((P (0) = x \land P (1) = z \land P (2) = y) \land (I (F (0)) = \{x, z\} \land I (F (1)) = \{z, y\})))$
32	31	rexbidva	$⊢ G \in USGraph \to (\exists x \in V \exists z \in (V ∖ \{x\}) \exists y \in (V ∖ \{x, z\}) ((P (0) = x \land P (1) = z \land P (2) = y) \land (I (F (0)) = \{x, z\} \land I (F (1)) = \{z, y\})) \leftrightarrow \exists x \in V \exists y \in (V ∖ \{x\}) \exists z \in (V ∖ \{x, y\}) ((P (0) = x \land P (1) = z \land P (2) = y) \land (I (F (0)) = \{x, z\} \land I (F (1)) = \{z, y\})))$
33	32	3anbi3d	$⊢ G \in USGraph \to ((F : (0 ..^2) \underset{1-1}{⟶} dom I \land P : (0 \dots 2) \underset{1-1}{⟶} V \land \exists x \in V \exists z \in (V ∖ \{x\}) \exists y \in (V ∖ \{x, z\}) ((P (0) = x \land P (1) = z \land P (2) = y) \land (I (F (0)) = \{x, z\} \land I (F (1)) = \{z, y\}))) \leftrightarrow (F : (0 ..^2) \underset{1-1}{⟶} dom I \land P : (0 \dots 2) \underset{1-1}{⟶} V \land \exists x \in V \exists y \in (V ∖ \{x\}) \exists z \in (V ∖ \{x, y\}) ((P (0) = x \land P (1) = z \land P (2) = y) \land (I (F (0)) = \{x, z\} \land I (F (1)) = \{z, y\}))))$
34	3 33	bitrd	$⊢ G \in USGraph \to ((F Paths (G) P \land \|F\| = 2) \leftrightarrow (F : (0 ..^2) \underset{1-1}{⟶} dom I \land P : (0 \dots 2) \underset{1-1}{⟶} V \land \exists x \in V \exists y \in (V ∖ \{x\}) \exists z \in (V ∖ \{x, y\}) ((P (0) = x \land P (1) = z \land P (2) = y) \land (I (F (0)) = \{x, z\} \land I (F (1)) = \{z, y\}))))$

Metamath Proof Explorer

Theorem usgr2pth0

Proof