usgr2pth

Description: In a simple 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) (Proof shortened by AV, 31-Oct-2021)

	Ref	Expression
Hypotheses	usgr2pthlem.v	$⊢ V = Vtx (G)$
	usgr2pthlem.i	$⊢ I = iEdg (G)$
Assertion	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 y \in (V ∖ \{x\}) \exists z \in (V ∖ \{x, y\}) ((P (0) = x \land P (1) = y \land P (2) = z) \land (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\}))))$

Proof

Step	Hyp	Ref	Expression
1		usgr2pthlem.v	$⊢ V = Vtx (G)$
2		usgr2pthlem.i	$⊢ I = iEdg (G)$
3		usgr2pthspth	$⊢ (G \in USGraph \land \|F\| = 2) \to (F Paths (G) P \leftrightarrow F SPaths (G) P)$
4		usgrupgr	$⊢ G \in USGraph \to G \in UPGraph$
5	4	adantr	$⊢ (G \in USGraph \land \|F\| = 2) \to G \in UPGraph$
6		isspth	$⊢ F SPaths (G) P \leftrightarrow (F Trails (G) P \land Fun P^{-1})$
7	6	a1i	$⊢ G \in UPGraph \to (F SPaths (G) P \leftrightarrow (F Trails (G) P \land Fun P^{-1}))$
8	1 2	upgrf1istrl	$⊢ G \in UPGraph \to (F Trails (G) P \leftrightarrow (F : (0 ..^\|F\|) \underset{1-1}{⟶} dom I \land P : (0 \dots \|F\|) ⟶ V \land \forall i \in (0 ..^\|F\|) I (F (i)) = \{P (i), P (i + 1)\}))$
9	8	anbi1d	$⊢ G \in UPGraph \to ((F Trails (G) P \land Fun P^{-1}) \leftrightarrow ((F : (0 ..^\|F\|) \underset{1-1}{⟶} dom I \land P : (0 \dots \|F\|) ⟶ V \land \forall i \in (0 ..^\|F\|) I (F (i)) = \{P (i), P (i + 1)\}) \land Fun P^{-1}))$
10		oveq2	$⊢ \|F\| = 2 \to (0 ..^\|F\|) = (0 ..^2)$
11		f1eq2	$⊢ (0 ..^\|F\|) = (0 ..^2) \to (F : (0 ..^\|F\|) \underset{1-1}{⟶} dom I \leftrightarrow F : (0 ..^2) \underset{1-1}{⟶} dom I)$
12	10 11	syl	$⊢ \|F\| = 2 \to (F : (0 ..^\|F\|) \underset{1-1}{⟶} dom I \leftrightarrow F : (0 ..^2) \underset{1-1}{⟶} dom I)$
13	12	biimpd	$⊢ \|F\| = 2 \to (F : (0 ..^\|F\|) \underset{1-1}{⟶} dom I \to F : (0 ..^2) \underset{1-1}{⟶} dom I)$
14	13	adantl	$⊢ (G \in USGraph \land \|F\| = 2) \to (F : (0 ..^\|F\|) \underset{1-1}{⟶} dom I \to F : (0 ..^2) \underset{1-1}{⟶} dom I)$
15	14	com12	$⊢ F : (0 ..^\|F\|) \underset{1-1}{⟶} dom I \to ((G \in USGraph \land \|F\| = 2) \to F : (0 ..^2) \underset{1-1}{⟶} dom I)$
16	15	3ad2ant1	$⊢ (F : (0 ..^\|F\|) \underset{1-1}{⟶} dom I \land P : (0 \dots \|F\|) ⟶ V \land \forall i \in (0 ..^\|F\|) I (F (i)) = \{P (i), P (i + 1)\}) \to ((G \in USGraph \land \|F\| = 2) \to F : (0 ..^2) \underset{1-1}{⟶} dom I)$
17	16	ad2antrl	$⊢ (G \in UPGraph \land ((F : (0 ..^\|F\|) \underset{1-1}{⟶} dom I \land P : (0 \dots \|F\|) ⟶ V \land \forall i \in (0 ..^\|F\|) I (F (i)) = \{P (i), P (i + 1)\}) \land Fun P^{-1})) \to ((G \in USGraph \land \|F\| = 2) \to F : (0 ..^2) \underset{1-1}{⟶} dom I)$
18		oveq2	$⊢ \|F\| = 2 \to (0 \dots \|F\|) = (0 \dots 2)$
19	18	feq2d	$⊢ \|F\| = 2 \to (P : (0 \dots \|F\|) ⟶ V \leftrightarrow P : (0 \dots 2) ⟶ V)$
20		df-f1	$⊢ P : (0 \dots 2) \underset{1-1}{⟶} V \leftrightarrow (P : (0 \dots 2) ⟶ V \land Fun P^{-1})$
21	20	simplbi2	$⊢ P : (0 \dots 2) ⟶ V \to (Fun P^{-1} \to P : (0 \dots 2) \underset{1-1}{⟶} V)$
22	21	a1i	$⊢ \|F\| = 2 \to (P : (0 \dots 2) ⟶ V \to (Fun P^{-1} \to P : (0 \dots 2) \underset{1-1}{⟶} V))$
23	19 22	sylbid	$⊢ \|F\| = 2 \to (P : (0 \dots \|F\|) ⟶ V \to (Fun P^{-1} \to P : (0 \dots 2) \underset{1-1}{⟶} V))$
24	23	adantl	$⊢ (G \in USGraph \land \|F\| = 2) \to (P : (0 \dots \|F\|) ⟶ V \to (Fun P^{-1} \to P : (0 \dots 2) \underset{1-1}{⟶} V))$
25	24	com3l	$⊢ P : (0 \dots \|F\|) ⟶ V \to (Fun P^{-1} \to ((G \in USGraph \land \|F\| = 2) \to P : (0 \dots 2) \underset{1-1}{⟶} V))$
26	25	3ad2ant2	$⊢ (F : (0 ..^\|F\|) \underset{1-1}{⟶} dom I \land P : (0 \dots \|F\|) ⟶ V \land \forall i \in (0 ..^\|F\|) I (F (i)) = \{P (i), P (i + 1)\}) \to (Fun P^{-1} \to ((G \in USGraph \land \|F\| = 2) \to P : (0 \dots 2) \underset{1-1}{⟶} V))$
27	26	imp	$⊢ ((F : (0 ..^\|F\|) \underset{1-1}{⟶} dom I \land P : (0 \dots \|F\|) ⟶ V \land \forall i \in (0 ..^\|F\|) I (F (i)) = \{P (i), P (i + 1)\}) \land Fun P^{-1}) \to ((G \in USGraph \land \|F\| = 2) \to P : (0 \dots 2) \underset{1-1}{⟶} V)$
28	27	adantl	$⊢ (G \in UPGraph \land ((F : (0 ..^\|F\|) \underset{1-1}{⟶} dom I \land P : (0 \dots \|F\|) ⟶ V \land \forall i \in (0 ..^\|F\|) I (F (i)) = \{P (i), P (i + 1)\}) \land Fun P^{-1})) \to ((G \in USGraph \land \|F\| = 2) \to P : (0 \dots 2) \underset{1-1}{⟶} V)$
29	1 2	usgr2pthlem	$⊢ (F : (0 ..^\|F\|) \underset{1-1}{⟶} dom I \land P : (0 \dots \|F\|) ⟶ V \land \forall i \in (0 ..^\|F\|) I (F (i)) = \{P (i), P (i + 1)\}) \to ((G \in USGraph \land \|F\| = 2) \to \exists x \in V \exists y \in (V ∖ \{x\}) \exists z \in (V ∖ \{x, y\}) ((P (0) = x \land P (1) = y \land P (2) = z) \land (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\})))$
30	29	ad2antrl	$⊢ (G \in UPGraph \land ((F : (0 ..^\|F\|) \underset{1-1}{⟶} dom I \land P : (0 \dots \|F\|) ⟶ V \land \forall i \in (0 ..^\|F\|) I (F (i)) = \{P (i), P (i + 1)\}) \land Fun P^{-1})) \to ((G \in USGraph \land \|F\| = 2) \to \exists x \in V \exists y \in (V ∖ \{x\}) \exists z \in (V ∖ \{x, y\}) ((P (0) = x \land P (1) = y \land P (2) = z) \land (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\})))$
31	17 28 30	3jcad	$⊢ (G \in UPGraph \land ((F : (0 ..^\|F\|) \underset{1-1}{⟶} dom I \land P : (0 \dots \|F\|) ⟶ V \land \forall i \in (0 ..^\|F\|) I (F (i)) = \{P (i), P (i + 1)\}) \land Fun P^{-1})) \to ((G \in USGraph \land \|F\| = 2) \to (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) = y \land P (2) = z) \land (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\}))))$
32	31	ex	$⊢ G \in UPGraph \to (((F : (0 ..^\|F\|) \underset{1-1}{⟶} dom I \land P : (0 \dots \|F\|) ⟶ V \land \forall i \in (0 ..^\|F\|) I (F (i)) = \{P (i), P (i + 1)\}) \land Fun P^{-1}) \to ((G \in USGraph \land \|F\| = 2) \to (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) = y \land P (2) = z) \land (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\})))))$
33	9 32	sylbid	$⊢ G \in UPGraph \to ((F Trails (G) P \land Fun P^{-1}) \to ((G \in USGraph \land \|F\| = 2) \to (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) = y \land P (2) = z) \land (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\})))))$
34	7 33	sylbid	$⊢ G \in UPGraph \to (F SPaths (G) P \to ((G \in USGraph \land \|F\| = 2) \to (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) = y \land P (2) = z) \land (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\})))))$
35	34	com23	$⊢ G \in UPGraph \to ((G \in USGraph \land \|F\| = 2) \to (F SPaths (G) P \to (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) = y \land P (2) = z) \land (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\})))))$
36	5 35	mpcom	$⊢ (G \in USGraph \land \|F\| = 2) \to (F SPaths (G) P \to (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) = y \land P (2) = z) \land (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\}))))$
37	3 36	sylbid	$⊢ (G \in USGraph \land \|F\| = 2) \to (F Paths (G) P \to (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) = y \land P (2) = z) \land (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\}))))$
38	37	ex	$⊢ G \in USGraph \to (\|F\| = 2 \to (F Paths (G) P \to (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) = y \land P (2) = z) \land (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\})))))$
39	38	impcomd	$⊢ G \in USGraph \to ((F Paths (G) P \land \|F\| = 2) \to (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) = y \land P (2) = z) \land (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\}))))$
40		2nn0	$⊢ 2 \in ℕ_{0}$
41		f1f	$⊢ F : (0 ..^2) \underset{1-1}{⟶} dom I \to F : (0 ..^2) ⟶ dom I$
42		fnfzo0hash	$⊢ (2 \in ℕ_{0} \land F : (0 ..^2) ⟶ dom I) \to \|F\| = 2$
43	40 41 42	sylancr	$⊢ F : (0 ..^2) \underset{1-1}{⟶} dom I \to \|F\| = 2$
44		oveq2	$⊢ 2 = \|F\| \to (0 ..^2) = (0 ..^\|F\|)$
45	44	eqcoms	$⊢ \|F\| = 2 \to (0 ..^2) = (0 ..^\|F\|)$
46		f1eq2	$⊢ (0 ..^2) = (0 ..^\|F\|) \to (F : (0 ..^2) \underset{1-1}{⟶} dom I \leftrightarrow F : (0 ..^\|F\|) \underset{1-1}{⟶} dom I)$
47	45 46	syl	$⊢ \|F\| = 2 \to (F : (0 ..^2) \underset{1-1}{⟶} dom I \leftrightarrow F : (0 ..^\|F\|) \underset{1-1}{⟶} dom I)$
48	47	biimpd	$⊢ \|F\| = 2 \to (F : (0 ..^2) \underset{1-1}{⟶} dom I \to F : (0 ..^\|F\|) \underset{1-1}{⟶} dom I)$
49	48	imp	$⊢ (\|F\| = 2 \land F : (0 ..^2) \underset{1-1}{⟶} dom I) \to F : (0 ..^\|F\|) \underset{1-1}{⟶} dom I$
50	49	adantr	$⊢ ((\|F\| = 2 \land F : (0 ..^2) \underset{1-1}{⟶} dom I) \land P : (0 \dots 2) \underset{1-1}{⟶} V) \to F : (0 ..^\|F\|) \underset{1-1}{⟶} dom I$
51	50	ad2antrr	$⊢ ((((\|F\| = 2 \land 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) = y \land P (2) = z) \land (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\}))) \land G \in USGraph) \to F : (0 ..^\|F\|) \underset{1-1}{⟶} dom I$
52		f1f	$⊢ P : (0 \dots 2) \underset{1-1}{⟶} V \to P : (0 \dots 2) ⟶ V$
53		oveq2	$⊢ 2 = \|F\| \to (0 \dots 2) = (0 \dots \|F\|)$
54	53	eqcoms	$⊢ \|F\| = 2 \to (0 \dots 2) = (0 \dots \|F\|)$
55	54	adantr	$⊢ (\|F\| = 2 \land F : (0 ..^2) \underset{1-1}{⟶} dom I) \to (0 \dots 2) = (0 \dots \|F\|)$
56	55	feq2d	$⊢ (\|F\| = 2 \land F : (0 ..^2) \underset{1-1}{⟶} dom I) \to (P : (0 \dots 2) ⟶ V \leftrightarrow P : (0 \dots \|F\|) ⟶ V)$
57	52 56	imbitrid	$⊢ (\|F\| = 2 \land F : (0 ..^2) \underset{1-1}{⟶} dom I) \to (P : (0 \dots 2) \underset{1-1}{⟶} V \to P : (0 \dots \|F\|) ⟶ V)$
58	57	imp	$⊢ ((\|F\| = 2 \land F : (0 ..^2) \underset{1-1}{⟶} dom I) \land P : (0 \dots 2) \underset{1-1}{⟶} V) \to P : (0 \dots \|F\|) ⟶ V$
59	58	ad2antrr	$⊢ ((((\|F\| = 2 \land 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) = y \land P (2) = z) \land (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\}))) \land G \in USGraph) \to P : (0 \dots \|F\|) ⟶ V$
60		eqcom	$⊢ P (0) = x \leftrightarrow x = P (0)$
61	60	biimpi	$⊢ P (0) = x \to x = P (0)$
62	61	3ad2ant1	$⊢ (P (0) = x \land P (1) = y \land P (2) = z) \to x = P (0)$
63		eqcom	$⊢ P (1) = y \leftrightarrow y = P (1)$
64	63	biimpi	$⊢ P (1) = y \to y = P (1)$
65	64	3ad2ant2	$⊢ (P (0) = x \land P (1) = y \land P (2) = z) \to y = P (1)$
66	62 65	preq12d	$⊢ (P (0) = x \land P (1) = y \land P (2) = z) \to \{x, y\} = \{P (0), P (1)\}$
67	66	eqeq2d	$⊢ (P (0) = x \land P (1) = y \land P (2) = z) \to (I (F (0)) = \{x, y\} \leftrightarrow I (F (0)) = \{P (0), P (1)\})$
68	67	biimpcd	$⊢ I (F (0)) = \{x, y\} \to ((P (0) = x \land P (1) = y \land P (2) = z) \to I (F (0)) = \{P (0), P (1)\})$
69	68	adantr	$⊢ (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\}) \to ((P (0) = x \land P (1) = y \land P (2) = z) \to I (F (0)) = \{P (0), P (1)\})$
70	69	impcom	$⊢ ((P (0) = x \land P (1) = y \land P (2) = z) \land (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\})) \to I (F (0)) = \{P (0), P (1)\}$
71		eqcom	$⊢ P (2) = z \leftrightarrow z = P (2)$
72	71	biimpi	$⊢ P (2) = z \to z = P (2)$
73	72	3ad2ant3	$⊢ (P (0) = x \land P (1) = y \land P (2) = z) \to z = P (2)$
74	65 73	preq12d	$⊢ (P (0) = x \land P (1) = y \land P (2) = z) \to \{y, z\} = \{P (1), P (2)\}$
75	74	eqeq2d	$⊢ (P (0) = x \land P (1) = y \land P (2) = z) \to (I (F (1)) = \{y, z\} \leftrightarrow I (F (1)) = \{P (1), P (2)\})$
76	75	biimpcd	$⊢ I (F (1)) = \{y, z\} \to ((P (0) = x \land P (1) = y \land P (2) = z) \to I (F (1)) = \{P (1), P (2)\})$
77	76	adantl	$⊢ (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\}) \to ((P (0) = x \land P (1) = y \land P (2) = z) \to I (F (1)) = \{P (1), P (2)\})$
78	77	impcom	$⊢ ((P (0) = x \land P (1) = y \land P (2) = z) \land (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\})) \to I (F (1)) = \{P (1), P (2)\}$
79	70 78	jca	$⊢ ((P (0) = x \land P (1) = y \land P (2) = z) \land (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\})) \to (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})$
80	79	rexlimivw	$⊢ \exists z \in (V ∖ \{x, y\}) ((P (0) = x \land P (1) = y \land P (2) = z) \land (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\})) \to (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})$
81	80	rexlimivw	$⊢ \exists y \in (V ∖ \{x\}) \exists z \in (V ∖ \{x, y\}) ((P (0) = x \land P (1) = y \land P (2) = z) \land (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\})) \to (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})$
82	81	rexlimivw	$⊢ \exists x \in V \exists y \in (V ∖ \{x\}) \exists z \in (V ∖ \{x, y\}) ((P (0) = x \land P (1) = y \land P (2) = z) \land (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\})) \to (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})$
83	82	a1i13	$⊢ \|F\| = 2 \to (\exists x \in V \exists y \in (V ∖ \{x\}) \exists z \in (V ∖ \{x, y\}) ((P (0) = x \land P (1) = y \land P (2) = z) \land (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\})) \to (G \in USGraph \to (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})))$
84		fzo0to2pr	$⊢ (0 ..^2) = \{0, 1\}$
85	10 84	eqtrdi	$⊢ \|F\| = 2 \to (0 ..^\|F\|) = \{0, 1\}$
86	85	raleqdv	$⊢ \|F\| = 2 \to (\forall i \in (0 ..^\|F\|) I (F (i)) = \{P (i), P (i + 1)\} \leftrightarrow \forall i \in \{0, 1\} I (F (i)) = \{P (i), P (i + 1)\})$
87		2wlklem	$⊢ \forall i \in \{0, 1\} I (F (i)) = \{P (i), P (i + 1)\} \leftrightarrow (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})$
88	86 87	bitrdi	$⊢ \|F\| = 2 \to (\forall i \in (0 ..^\|F\|) I (F (i)) = \{P (i), P (i + 1)\} \leftrightarrow (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\}))$
89	88	imbi2d	$⊢ \|F\| = 2 \to ((G \in USGraph \to \forall i \in (0 ..^\|F\|) I (F (i)) = \{P (i), P (i + 1)\}) \leftrightarrow (G \in USGraph \to (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})))$
90	83 89	sylibrd	$⊢ \|F\| = 2 \to (\exists x \in V \exists y \in (V ∖ \{x\}) \exists z \in (V ∖ \{x, y\}) ((P (0) = x \land P (1) = y \land P (2) = z) \land (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\})) \to (G \in USGraph \to \forall i \in (0 ..^\|F\|) I (F (i)) = \{P (i), P (i + 1)\}))$
91	90	ad2antrr	$⊢ ((\|F\| = 2 \land F : (0 ..^2) \underset{1-1}{⟶} dom I) \land P : (0 \dots 2) \underset{1-1}{⟶} V) \to (\exists x \in V \exists y \in (V ∖ \{x\}) \exists z \in (V ∖ \{x, y\}) ((P (0) = x \land P (1) = y \land P (2) = z) \land (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\})) \to (G \in USGraph \to \forall i \in (0 ..^\|F\|) I (F (i)) = \{P (i), P (i + 1)\}))$
92	91	imp	$⊢ (((\|F\| = 2 \land 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) = y \land P (2) = z) \land (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\}))) \to (G \in USGraph \to \forall i \in (0 ..^\|F\|) I (F (i)) = \{P (i), P (i + 1)\})$
93	92	imp	$⊢ ((((\|F\| = 2 \land 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) = y \land P (2) = z) \land (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\}))) \land G \in USGraph) \to \forall i \in (0 ..^\|F\|) I (F (i)) = \{P (i), P (i + 1)\}$
94	51 59 93	3jca	$⊢ ((((\|F\| = 2 \land 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) = y \land P (2) = z) \land (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\}))) \land G \in USGraph) \to (F : (0 ..^\|F\|) \underset{1-1}{⟶} dom I \land P : (0 \dots \|F\|) ⟶ V \land \forall i \in (0 ..^\|F\|) I (F (i)) = \{P (i), P (i + 1)\})$
95	20	simprbi	$⊢ P : (0 \dots 2) \underset{1-1}{⟶} V \to Fun P^{-1}$
96	95	adantl	$⊢ ((\|F\| = 2 \land F : (0 ..^2) \underset{1-1}{⟶} dom I) \land P : (0 \dots 2) \underset{1-1}{⟶} V) \to Fun P^{-1}$
97	96	ad2antrr	$⊢ ((((\|F\| = 2 \land 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) = y \land P (2) = z) \land (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\}))) \land G \in USGraph) \to Fun P^{-1}$
98	94 97	jca	$⊢ ((((\|F\| = 2 \land 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) = y \land P (2) = z) \land (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\}))) \land G \in USGraph) \to ((F : (0 ..^\|F\|) \underset{1-1}{⟶} dom I \land P : (0 \dots \|F\|) ⟶ V \land \forall i \in (0 ..^\|F\|) I (F (i)) = \{P (i), P (i + 1)\}) \land Fun P^{-1})$
99	7 9	bitrd	$⊢ G \in UPGraph \to (F SPaths (G) P \leftrightarrow ((F : (0 ..^\|F\|) \underset{1-1}{⟶} dom I \land P : (0 \dots \|F\|) ⟶ V \land \forall i \in (0 ..^\|F\|) I (F (i)) = \{P (i), P (i + 1)\}) \land Fun P^{-1}))$
100	4 99	syl	$⊢ G \in USGraph \to (F SPaths (G) P \leftrightarrow ((F : (0 ..^\|F\|) \underset{1-1}{⟶} dom I \land P : (0 \dots \|F\|) ⟶ V \land \forall i \in (0 ..^\|F\|) I (F (i)) = \{P (i), P (i + 1)\}) \land Fun P^{-1}))$
101	100	adantl	$⊢ ((((\|F\| = 2 \land 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) = y \land P (2) = z) \land (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\}))) \land G \in USGraph) \to (F SPaths (G) P \leftrightarrow ((F : (0 ..^\|F\|) \underset{1-1}{⟶} dom I \land P : (0 \dots \|F\|) ⟶ V \land \forall i \in (0 ..^\|F\|) I (F (i)) = \{P (i), P (i + 1)\}) \land Fun P^{-1}))$
102	98 101	mpbird	$⊢ ((((\|F\| = 2 \land 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) = y \land P (2) = z) \land (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\}))) \land G \in USGraph) \to F SPaths (G) P$
103		simpr	$⊢ ((((\|F\| = 2 \land 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) = y \land P (2) = z) \land (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\}))) \land G \in USGraph) \to G \in USGraph$
104		simp-4l	$⊢ ((((\|F\| = 2 \land 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) = y \land P (2) = z) \land (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\}))) \land G \in USGraph) \to \|F\| = 2$
105	103 104 3	syl2anc	$⊢ ((((\|F\| = 2 \land 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) = y \land P (2) = z) \land (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\}))) \land G \in USGraph) \to (F Paths (G) P \leftrightarrow F SPaths (G) P)$
106	102 105	mpbird	$⊢ ((((\|F\| = 2 \land 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) = y \land P (2) = z) \land (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\}))) \land G \in USGraph) \to F Paths (G) P$
107	106 104	jca	$⊢ ((((\|F\| = 2 \land 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) = y \land P (2) = z) \land (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\}))) \land G \in USGraph) \to (F Paths (G) P \land \|F\| = 2)$
108	107	ex	$⊢ (((\|F\| = 2 \land 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) = y \land P (2) = z) \land (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\}))) \to (G \in USGraph \to (F Paths (G) P \land \|F\| = 2))$
109	108	exp41	$⊢ \|F\| = 2 \to (F : (0 ..^2) \underset{1-1}{⟶} dom I \to (P : (0 \dots 2) \underset{1-1}{⟶} V \to (\exists x \in V \exists y \in (V ∖ \{x\}) \exists z \in (V ∖ \{x, y\}) ((P (0) = x \land P (1) = y \land P (2) = z) \land (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\})) \to (G \in USGraph \to (F Paths (G) P \land \|F\| = 2)))))$
110	43 109	mpcom	$⊢ F : (0 ..^2) \underset{1-1}{⟶} dom I \to (P : (0 \dots 2) \underset{1-1}{⟶} V \to (\exists x \in V \exists y \in (V ∖ \{x\}) \exists z \in (V ∖ \{x, y\}) ((P (0) = x \land P (1) = y \land P (2) = z) \land (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\})) \to (G \in USGraph \to (F Paths (G) P \land \|F\| = 2))))$
111	110	3imp	$⊢ (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) = y \land P (2) = z) \land (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\}))) \to (G \in USGraph \to (F Paths (G) P \land \|F\| = 2))$
112	111	com12	$⊢ 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 y \in (V ∖ \{x\}) \exists z \in (V ∖ \{x, y\}) ((P (0) = x \land P (1) = y \land P (2) = z) \land (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\}))) \to (F Paths (G) P \land \|F\| = 2))$
113	39 112	impbid	$⊢ 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) = y \land P (2) = z) \land (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\}))))$

Metamath Proof Explorer

Theorem usgr2pth

Proof