uspgr2wlkeq

Description: Conditions for two walks within the same simple pseudograph being the same. It is sufficient that the vertices (in the same order) are identical. (Contributed by AV, 3-Jul-2018) (Revised by AV, 14-Apr-2021)

		Ref	Expression
	Assertion	uspgr2wlkeq	$⊢ (G \in USHGraph \land (A \in Walks (G) \land B \in Walks (G)) \land N = \|1^{st} (A)\|) \to (A = B \leftrightarrow (N = \|1^{st} (B)\| \land \forall y \in (0 \dots N) 2^{nd} (A) (y) = 2^{nd} (B) (y)))$

Proof

Step	Hyp	Ref	Expression
1		3anan32	$⊢ (N = \|1^{st} (B)\| \land \forall y \in (0 ..^N) 1^{st} (A) (y) = 1^{st} (B) (y) \land \forall y \in (0 \dots N) 2^{nd} (A) (y) = 2^{nd} (B) (y)) \leftrightarrow ((N = \|1^{st} (B)\| \land \forall y \in (0 \dots N) 2^{nd} (A) (y) = 2^{nd} (B) (y)) \land \forall y \in (0 ..^N) 1^{st} (A) (y) = 1^{st} (B) (y))$
2	1	a1i	$⊢ (G \in USHGraph \land (A \in Walks (G) \land B \in Walks (G)) \land N = \|1^{st} (A)\|) \to ((N = \|1^{st} (B)\| \land \forall y \in (0 ..^N) 1^{st} (A) (y) = 1^{st} (B) (y) \land \forall y \in (0 \dots N) 2^{nd} (A) (y) = 2^{nd} (B) (y)) \leftrightarrow ((N = \|1^{st} (B)\| \land \forall y \in (0 \dots N) 2^{nd} (A) (y) = 2^{nd} (B) (y)) \land \forall y \in (0 ..^N) 1^{st} (A) (y) = 1^{st} (B) (y)))$
3		wlkeq	$⊢ (A \in Walks (G) \land B \in Walks (G) \land N = \|1^{st} (A)\|) \to (A = B \leftrightarrow (N = \|1^{st} (B)\| \land \forall y \in (0 ..^N) 1^{st} (A) (y) = 1^{st} (B) (y) \land \forall y \in (0 \dots N) 2^{nd} (A) (y) = 2^{nd} (B) (y)))$
4	3	3expa	$⊢ ((A \in Walks (G) \land B \in Walks (G)) \land N = \|1^{st} (A)\|) \to (A = B \leftrightarrow (N = \|1^{st} (B)\| \land \forall y \in (0 ..^N) 1^{st} (A) (y) = 1^{st} (B) (y) \land \forall y \in (0 \dots N) 2^{nd} (A) (y) = 2^{nd} (B) (y)))$
5	4	3adant1	$⊢ (G \in USHGraph \land (A \in Walks (G) \land B \in Walks (G)) \land N = \|1^{st} (A)\|) \to (A = B \leftrightarrow (N = \|1^{st} (B)\| \land \forall y \in (0 ..^N) 1^{st} (A) (y) = 1^{st} (B) (y) \land \forall y \in (0 \dots N) 2^{nd} (A) (y) = 2^{nd} (B) (y)))$
6		fzofzp1	$⊢ x \in (0 ..^N) \to x + 1 \in (0 \dots N)$
7	6	adantl	$⊢ (((G \in USHGraph \land (A \in Walks (G) \land B \in Walks (G)) \land N = \|1^{st} (A)\|) \land N = \|1^{st} (B)\|) \land x \in (0 ..^N)) \to x + 1 \in (0 \dots N)$
8		fveq2	$⊢ y = x + 1 \to 2^{nd} (A) (y) = 2^{nd} (A) (x + 1)$
9		fveq2	$⊢ y = x + 1 \to 2^{nd} (B) (y) = 2^{nd} (B) (x + 1)$
10	8 9	eqeq12d	$⊢ y = x + 1 \to (2^{nd} (A) (y) = 2^{nd} (B) (y) \leftrightarrow 2^{nd} (A) (x + 1) = 2^{nd} (B) (x + 1))$
11	10	adantl	$⊢ ((((G \in USHGraph \land (A \in Walks (G) \land B \in Walks (G)) \land N = \|1^{st} (A)\|) \land N = \|1^{st} (B)\|) \land x \in (0 ..^N)) \land y = x + 1) \to (2^{nd} (A) (y) = 2^{nd} (B) (y) \leftrightarrow 2^{nd} (A) (x + 1) = 2^{nd} (B) (x + 1))$
12	7 11	rspcdv	$⊢ (((G \in USHGraph \land (A \in Walks (G) \land B \in Walks (G)) \land N = \|1^{st} (A)\|) \land N = \|1^{st} (B)\|) \land x \in (0 ..^N)) \to (\forall y \in (0 \dots N) 2^{nd} (A) (y) = 2^{nd} (B) (y) \to 2^{nd} (A) (x + 1) = 2^{nd} (B) (x + 1))$
13	12	impancom	$⊢ (((G \in USHGraph \land (A \in Walks (G) \land B \in Walks (G)) \land N = \|1^{st} (A)\|) \land N = \|1^{st} (B)\|) \land \forall y \in (0 \dots N) 2^{nd} (A) (y) = 2^{nd} (B) (y)) \to (x \in (0 ..^N) \to 2^{nd} (A) (x + 1) = 2^{nd} (B) (x + 1))$
14	13	ralrimiv	$⊢ (((G \in USHGraph \land (A \in Walks (G) \land B \in Walks (G)) \land N = \|1^{st} (A)\|) \land N = \|1^{st} (B)\|) \land \forall y \in (0 \dots N) 2^{nd} (A) (y) = 2^{nd} (B) (y)) \to \forall x \in (0 ..^N) 2^{nd} (A) (x + 1) = 2^{nd} (B) (x + 1)$
15		fvoveq1	$⊢ y = x \to 2^{nd} (A) (y + 1) = 2^{nd} (A) (x + 1)$
16		fvoveq1	$⊢ y = x \to 2^{nd} (B) (y + 1) = 2^{nd} (B) (x + 1)$
17	15 16	eqeq12d	$⊢ y = x \to (2^{nd} (A) (y + 1) = 2^{nd} (B) (y + 1) \leftrightarrow 2^{nd} (A) (x + 1) = 2^{nd} (B) (x + 1))$
18	17	cbvralvw	$⊢ \forall y \in (0 ..^N) 2^{nd} (A) (y + 1) = 2^{nd} (B) (y + 1) \leftrightarrow \forall x \in (0 ..^N) 2^{nd} (A) (x + 1) = 2^{nd} (B) (x + 1)$
19	14 18	sylibr	$⊢ (((G \in USHGraph \land (A \in Walks (G) \land B \in Walks (G)) \land N = \|1^{st} (A)\|) \land N = \|1^{st} (B)\|) \land \forall y \in (0 \dots N) 2^{nd} (A) (y) = 2^{nd} (B) (y)) \to \forall y \in (0 ..^N) 2^{nd} (A) (y + 1) = 2^{nd} (B) (y + 1)$
20		fzossfz	$⊢ (0 ..^N) \subseteq (0 \dots N)$
21		ssralv	$⊢ (0 ..^N) \subseteq (0 \dots N) \to (\forall y \in (0 \dots N) 2^{nd} (A) (y) = 2^{nd} (B) (y) \to \forall y \in (0 ..^N) 2^{nd} (A) (y) = 2^{nd} (B) (y))$
22	20 21	mp1i	$⊢ ((G \in USHGraph \land (A \in Walks (G) \land B \in Walks (G)) \land N = \|1^{st} (A)\|) \land N = \|1^{st} (B)\|) \to (\forall y \in (0 \dots N) 2^{nd} (A) (y) = 2^{nd} (B) (y) \to \forall y \in (0 ..^N) 2^{nd} (A) (y) = 2^{nd} (B) (y))$
23		r19.26	$⊢ \forall y \in (0 ..^N) (2^{nd} (A) (y) = 2^{nd} (B) (y) \land 2^{nd} (A) (y + 1) = 2^{nd} (B) (y + 1)) \leftrightarrow (\forall y \in (0 ..^N) 2^{nd} (A) (y) = 2^{nd} (B) (y) \land \forall y \in (0 ..^N) 2^{nd} (A) (y + 1) = 2^{nd} (B) (y + 1))$
24		preq12	$⊢ (2^{nd} (A) (y) = 2^{nd} (B) (y) \land 2^{nd} (A) (y + 1) = 2^{nd} (B) (y + 1)) \to \{2^{nd} (A) (y), 2^{nd} (A) (y + 1)\} = \{2^{nd} (B) (y), 2^{nd} (B) (y + 1)\}$
25	24	a1i	$⊢ ((G \in USHGraph \land (A \in Walks (G) \land B \in Walks (G)) \land N = \|1^{st} (A)\|) \land N = \|1^{st} (B)\|) \to ((2^{nd} (A) (y) = 2^{nd} (B) (y) \land 2^{nd} (A) (y + 1) = 2^{nd} (B) (y + 1)) \to \{2^{nd} (A) (y), 2^{nd} (A) (y + 1)\} = \{2^{nd} (B) (y), 2^{nd} (B) (y + 1)\})$
26	25	ralimdv	$⊢ ((G \in USHGraph \land (A \in Walks (G) \land B \in Walks (G)) \land N = \|1^{st} (A)\|) \land N = \|1^{st} (B)\|) \to (\forall y \in (0 ..^N) (2^{nd} (A) (y) = 2^{nd} (B) (y) \land 2^{nd} (A) (y + 1) = 2^{nd} (B) (y + 1)) \to \forall y \in (0 ..^N) \{2^{nd} (A) (y), 2^{nd} (A) (y + 1)\} = \{2^{nd} (B) (y), 2^{nd} (B) (y + 1)\})$
27	23 26	syl5bir	$⊢ ((G \in USHGraph \land (A \in Walks (G) \land B \in Walks (G)) \land N = \|1^{st} (A)\|) \land N = \|1^{st} (B)\|) \to ((\forall y \in (0 ..^N) 2^{nd} (A) (y) = 2^{nd} (B) (y) \land \forall y \in (0 ..^N) 2^{nd} (A) (y + 1) = 2^{nd} (B) (y + 1)) \to \forall y \in (0 ..^N) \{2^{nd} (A) (y), 2^{nd} (A) (y + 1)\} = \{2^{nd} (B) (y), 2^{nd} (B) (y + 1)\})$
28	27	expd	$⊢ ((G \in USHGraph \land (A \in Walks (G) \land B \in Walks (G)) \land N = \|1^{st} (A)\|) \land N = \|1^{st} (B)\|) \to (\forall y \in (0 ..^N) 2^{nd} (A) (y) = 2^{nd} (B) (y) \to (\forall y \in (0 ..^N) 2^{nd} (A) (y + 1) = 2^{nd} (B) (y + 1) \to \forall y \in (0 ..^N) \{2^{nd} (A) (y), 2^{nd} (A) (y + 1)\} = \{2^{nd} (B) (y), 2^{nd} (B) (y + 1)\}))$
29	22 28	syld	$⊢ ((G \in USHGraph \land (A \in Walks (G) \land B \in Walks (G)) \land N = \|1^{st} (A)\|) \land N = \|1^{st} (B)\|) \to (\forall y \in (0 \dots N) 2^{nd} (A) (y) = 2^{nd} (B) (y) \to (\forall y \in (0 ..^N) 2^{nd} (A) (y + 1) = 2^{nd} (B) (y + 1) \to \forall y \in (0 ..^N) \{2^{nd} (A) (y), 2^{nd} (A) (y + 1)\} = \{2^{nd} (B) (y), 2^{nd} (B) (y + 1)\}))$
30	29	imp	$⊢ (((G \in USHGraph \land (A \in Walks (G) \land B \in Walks (G)) \land N = \|1^{st} (A)\|) \land N = \|1^{st} (B)\|) \land \forall y \in (0 \dots N) 2^{nd} (A) (y) = 2^{nd} (B) (y)) \to (\forall y \in (0 ..^N) 2^{nd} (A) (y + 1) = 2^{nd} (B) (y + 1) \to \forall y \in (0 ..^N) \{2^{nd} (A) (y), 2^{nd} (A) (y + 1)\} = \{2^{nd} (B) (y), 2^{nd} (B) (y + 1)\})$
31	19 30	mpd	$⊢ (((G \in USHGraph \land (A \in Walks (G) \land B \in Walks (G)) \land N = \|1^{st} (A)\|) \land N = \|1^{st} (B)\|) \land \forall y \in (0 \dots N) 2^{nd} (A) (y) = 2^{nd} (B) (y)) \to \forall y \in (0 ..^N) \{2^{nd} (A) (y), 2^{nd} (A) (y + 1)\} = \{2^{nd} (B) (y), 2^{nd} (B) (y + 1)\}$
32	31	ex	$⊢ ((G \in USHGraph \land (A \in Walks (G) \land B \in Walks (G)) \land N = \|1^{st} (A)\|) \land N = \|1^{st} (B)\|) \to (\forall y \in (0 \dots N) 2^{nd} (A) (y) = 2^{nd} (B) (y) \to \forall y \in (0 ..^N) \{2^{nd} (A) (y), 2^{nd} (A) (y + 1)\} = \{2^{nd} (B) (y), 2^{nd} (B) (y + 1)\})$
33		uspgrupgr	$⊢ G \in USHGraph \to G \in UPGraph$
34		eqid	$⊢ Vtx (G) = Vtx (G)$
35		eqid	$⊢ iEdg (G) = iEdg (G)$
36		eqid	$⊢ 1^{st} (A) = 1^{st} (A)$
37		eqid	$⊢ 2^{nd} (A) = 2^{nd} (A)$
38	34 35 36 37	upgrwlkcompim	$⊢ (G \in UPGraph \land A \in Walks (G)) \to (1^{st} (A) \in Word dom iEdg (G) \land 2^{nd} (A) : (0 \dots \|1^{st} (A)\|) ⟶ Vtx (G) \land \forall y \in (0 ..^\|1^{st} (A)\|) iEdg (G) (1^{st} (A) (y)) = \{2^{nd} (A) (y), 2^{nd} (A) (y + 1)\})$
39	38	ex	$⊢ G \in UPGraph \to (A \in Walks (G) \to (1^{st} (A) \in Word dom iEdg (G) \land 2^{nd} (A) : (0 \dots \|1^{st} (A)\|) ⟶ Vtx (G) \land \forall y \in (0 ..^\|1^{st} (A)\|) iEdg (G) (1^{st} (A) (y)) = \{2^{nd} (A) (y), 2^{nd} (A) (y + 1)\}))$
40	33 39	syl	$⊢ G \in USHGraph \to (A \in Walks (G) \to (1^{st} (A) \in Word dom iEdg (G) \land 2^{nd} (A) : (0 \dots \|1^{st} (A)\|) ⟶ Vtx (G) \land \forall y \in (0 ..^\|1^{st} (A)\|) iEdg (G) (1^{st} (A) (y)) = \{2^{nd} (A) (y), 2^{nd} (A) (y + 1)\}))$
41		eqid	$⊢ 1^{st} (B) = 1^{st} (B)$
42		eqid	$⊢ 2^{nd} (B) = 2^{nd} (B)$
43	34 35 41 42	upgrwlkcompim	$⊢ (G \in UPGraph \land B \in Walks (G)) \to (1^{st} (B) \in Word dom iEdg (G) \land 2^{nd} (B) : (0 \dots \|1^{st} (B)\|) ⟶ Vtx (G) \land \forall y \in (0 ..^\|1^{st} (B)\|) iEdg (G) (1^{st} (B) (y)) = \{2^{nd} (B) (y), 2^{nd} (B) (y + 1)\})$
44	43	ex	$⊢ G \in UPGraph \to (B \in Walks (G) \to (1^{st} (B) \in Word dom iEdg (G) \land 2^{nd} (B) : (0 \dots \|1^{st} (B)\|) ⟶ Vtx (G) \land \forall y \in (0 ..^\|1^{st} (B)\|) iEdg (G) (1^{st} (B) (y)) = \{2^{nd} (B) (y), 2^{nd} (B) (y + 1)\}))$
45	33 44	syl	$⊢ G \in USHGraph \to (B \in Walks (G) \to (1^{st} (B) \in Word dom iEdg (G) \land 2^{nd} (B) : (0 \dots \|1^{st} (B)\|) ⟶ Vtx (G) \land \forall y \in (0 ..^\|1^{st} (B)\|) iEdg (G) (1^{st} (B) (y)) = \{2^{nd} (B) (y), 2^{nd} (B) (y + 1)\}))$
46		oveq2	$⊢ \|1^{st} (B)\| = N \to (0 ..^\|1^{st} (B)\|) = (0 ..^N)$
47	46	eqcoms	$⊢ N = \|1^{st} (B)\| \to (0 ..^\|1^{st} (B)\|) = (0 ..^N)$
48	47	raleqdv	$⊢ N = \|1^{st} (B)\| \to (\forall y \in (0 ..^\|1^{st} (B)\|) iEdg (G) (1^{st} (B) (y)) = \{2^{nd} (B) (y), 2^{nd} (B) (y + 1)\} \leftrightarrow \forall y \in (0 ..^N) iEdg (G) (1^{st} (B) (y)) = \{2^{nd} (B) (y), 2^{nd} (B) (y + 1)\})$
49		oveq2	$⊢ \|1^{st} (A)\| = N \to (0 ..^\|1^{st} (A)\|) = (0 ..^N)$
50	49	eqcoms	$⊢ N = \|1^{st} (A)\| \to (0 ..^\|1^{st} (A)\|) = (0 ..^N)$
51	50	raleqdv	$⊢ N = \|1^{st} (A)\| \to (\forall y \in (0 ..^\|1^{st} (A)\|) iEdg (G) (1^{st} (A) (y)) = \{2^{nd} (A) (y), 2^{nd} (A) (y + 1)\} \leftrightarrow \forall y \in (0 ..^N) iEdg (G) (1^{st} (A) (y)) = \{2^{nd} (A) (y), 2^{nd} (A) (y + 1)\})$
52	48 51	bi2anan9r	$⊢ (N = \|1^{st} (A)\| \land N = \|1^{st} (B)\|) \to ((\forall y \in (0 ..^\|1^{st} (B)\|) iEdg (G) (1^{st} (B) (y)) = \{2^{nd} (B) (y), 2^{nd} (B) (y + 1)\} \land \forall y \in (0 ..^\|1^{st} (A)\|) iEdg (G) (1^{st} (A) (y)) = \{2^{nd} (A) (y), 2^{nd} (A) (y + 1)\}) \leftrightarrow (\forall y \in (0 ..^N) iEdg (G) (1^{st} (B) (y)) = \{2^{nd} (B) (y), 2^{nd} (B) (y + 1)\} \land \forall y \in (0 ..^N) iEdg (G) (1^{st} (A) (y)) = \{2^{nd} (A) (y), 2^{nd} (A) (y + 1)\}))$
53		r19.26	$⊢ \forall y \in (0 ..^N) (iEdg (G) (1^{st} (B) (y)) = \{2^{nd} (B) (y), 2^{nd} (B) (y + 1)\} \land iEdg (G) (1^{st} (A) (y)) = \{2^{nd} (A) (y), 2^{nd} (A) (y + 1)\}) \leftrightarrow (\forall y \in (0 ..^N) iEdg (G) (1^{st} (B) (y)) = \{2^{nd} (B) (y), 2^{nd} (B) (y + 1)\} \land \forall y \in (0 ..^N) iEdg (G) (1^{st} (A) (y)) = \{2^{nd} (A) (y), 2^{nd} (A) (y + 1)\})$
54		eqeq2	$⊢ \{2^{nd} (A) (y), 2^{nd} (A) (y + 1)\} = \{2^{nd} (B) (y), 2^{nd} (B) (y + 1)\} \to (iEdg (G) (1^{st} (A) (y)) = \{2^{nd} (A) (y), 2^{nd} (A) (y + 1)\} \leftrightarrow iEdg (G) (1^{st} (A) (y)) = \{2^{nd} (B) (y), 2^{nd} (B) (y + 1)\})$
55		eqeq2	$⊢ \{2^{nd} (B) (y), 2^{nd} (B) (y + 1)\} = iEdg (G) (1^{st} (A) (y)) \to (iEdg (G) (1^{st} (B) (y)) = \{2^{nd} (B) (y), 2^{nd} (B) (y + 1)\} \leftrightarrow iEdg (G) (1^{st} (B) (y)) = iEdg (G) (1^{st} (A) (y)))$
56	55	eqcoms	$⊢ iEdg (G) (1^{st} (A) (y)) = \{2^{nd} (B) (y), 2^{nd} (B) (y + 1)\} \to (iEdg (G) (1^{st} (B) (y)) = \{2^{nd} (B) (y), 2^{nd} (B) (y + 1)\} \leftrightarrow iEdg (G) (1^{st} (B) (y)) = iEdg (G) (1^{st} (A) (y)))$
57	56	biimpd	$⊢ iEdg (G) (1^{st} (A) (y)) = \{2^{nd} (B) (y), 2^{nd} (B) (y + 1)\} \to (iEdg (G) (1^{st} (B) (y)) = \{2^{nd} (B) (y), 2^{nd} (B) (y + 1)\} \to iEdg (G) (1^{st} (B) (y)) = iEdg (G) (1^{st} (A) (y)))$
58	54 57	syl6bi	$⊢ \{2^{nd} (A) (y), 2^{nd} (A) (y + 1)\} = \{2^{nd} (B) (y), 2^{nd} (B) (y + 1)\} \to (iEdg (G) (1^{st} (A) (y)) = \{2^{nd} (A) (y), 2^{nd} (A) (y + 1)\} \to (iEdg (G) (1^{st} (B) (y)) = \{2^{nd} (B) (y), 2^{nd} (B) (y + 1)\} \to iEdg (G) (1^{st} (B) (y)) = iEdg (G) (1^{st} (A) (y))))$
59	58	com13	$⊢ iEdg (G) (1^{st} (B) (y)) = \{2^{nd} (B) (y), 2^{nd} (B) (y + 1)\} \to (iEdg (G) (1^{st} (A) (y)) = \{2^{nd} (A) (y), 2^{nd} (A) (y + 1)\} \to (\{2^{nd} (A) (y), 2^{nd} (A) (y + 1)\} = \{2^{nd} (B) (y), 2^{nd} (B) (y + 1)\} \to iEdg (G) (1^{st} (B) (y)) = iEdg (G) (1^{st} (A) (y))))$
60	59	imp	$⊢ (iEdg (G) (1^{st} (B) (y)) = \{2^{nd} (B) (y), 2^{nd} (B) (y + 1)\} \land iEdg (G) (1^{st} (A) (y)) = \{2^{nd} (A) (y), 2^{nd} (A) (y + 1)\}) \to (\{2^{nd} (A) (y), 2^{nd} (A) (y + 1)\} = \{2^{nd} (B) (y), 2^{nd} (B) (y + 1)\} \to iEdg (G) (1^{st} (B) (y)) = iEdg (G) (1^{st} (A) (y)))$
61	60	ral2imi	$⊢ \forall y \in (0 ..^N) (iEdg (G) (1^{st} (B) (y)) = \{2^{nd} (B) (y), 2^{nd} (B) (y + 1)\} \land iEdg (G) (1^{st} (A) (y)) = \{2^{nd} (A) (y), 2^{nd} (A) (y + 1)\}) \to (\forall y \in (0 ..^N) \{2^{nd} (A) (y), 2^{nd} (A) (y + 1)\} = \{2^{nd} (B) (y), 2^{nd} (B) (y + 1)\} \to \forall y \in (0 ..^N) iEdg (G) (1^{st} (B) (y)) = iEdg (G) (1^{st} (A) (y)))$
62	53 61	sylbir	$⊢ (\forall y \in (0 ..^N) iEdg (G) (1^{st} (B) (y)) = \{2^{nd} (B) (y), 2^{nd} (B) (y + 1)\} \land \forall y \in (0 ..^N) iEdg (G) (1^{st} (A) (y)) = \{2^{nd} (A) (y), 2^{nd} (A) (y + 1)\}) \to (\forall y \in (0 ..^N) \{2^{nd} (A) (y), 2^{nd} (A) (y + 1)\} = \{2^{nd} (B) (y), 2^{nd} (B) (y + 1)\} \to \forall y \in (0 ..^N) iEdg (G) (1^{st} (B) (y)) = iEdg (G) (1^{st} (A) (y)))$
63	52 62	syl6bi	$⊢ (N = \|1^{st} (A)\| \land N = \|1^{st} (B)\|) \to ((\forall y \in (0 ..^\|1^{st} (B)\|) iEdg (G) (1^{st} (B) (y)) = \{2^{nd} (B) (y), 2^{nd} (B) (y + 1)\} \land \forall y \in (0 ..^\|1^{st} (A)\|) iEdg (G) (1^{st} (A) (y)) = \{2^{nd} (A) (y), 2^{nd} (A) (y + 1)\}) \to (\forall y \in (0 ..^N) \{2^{nd} (A) (y), 2^{nd} (A) (y + 1)\} = \{2^{nd} (B) (y), 2^{nd} (B) (y + 1)\} \to \forall y \in (0 ..^N) iEdg (G) (1^{st} (B) (y)) = iEdg (G) (1^{st} (A) (y))))$
64	63	com12	$⊢ (\forall y \in (0 ..^\|1^{st} (B)\|) iEdg (G) (1^{st} (B) (y)) = \{2^{nd} (B) (y), 2^{nd} (B) (y + 1)\} \land \forall y \in (0 ..^\|1^{st} (A)\|) iEdg (G) (1^{st} (A) (y)) = \{2^{nd} (A) (y), 2^{nd} (A) (y + 1)\}) \to ((N = \|1^{st} (A)\| \land N = \|1^{st} (B)\|) \to (\forall y \in (0 ..^N) \{2^{nd} (A) (y), 2^{nd} (A) (y + 1)\} = \{2^{nd} (B) (y), 2^{nd} (B) (y + 1)\} \to \forall y \in (0 ..^N) iEdg (G) (1^{st} (B) (y)) = iEdg (G) (1^{st} (A) (y))))$
65	64	ex	$⊢ \forall y \in (0 ..^\|1^{st} (B)\|) iEdg (G) (1^{st} (B) (y)) = \{2^{nd} (B) (y), 2^{nd} (B) (y + 1)\} \to (\forall y \in (0 ..^\|1^{st} (A)\|) iEdg (G) (1^{st} (A) (y)) = \{2^{nd} (A) (y), 2^{nd} (A) (y + 1)\} \to ((N = \|1^{st} (A)\| \land N = \|1^{st} (B)\|) \to (\forall y \in (0 ..^N) \{2^{nd} (A) (y), 2^{nd} (A) (y + 1)\} = \{2^{nd} (B) (y), 2^{nd} (B) (y + 1)\} \to \forall y \in (0 ..^N) iEdg (G) (1^{st} (B) (y)) = iEdg (G) (1^{st} (A) (y)))))$
66	65	3ad2ant3	$⊢ (1^{st} (B) \in Word dom iEdg (G) \land 2^{nd} (B) : (0 \dots \|1^{st} (B)\|) ⟶ Vtx (G) \land \forall y \in (0 ..^\|1^{st} (B)\|) iEdg (G) (1^{st} (B) (y)) = \{2^{nd} (B) (y), 2^{nd} (B) (y + 1)\}) \to (\forall y \in (0 ..^\|1^{st} (A)\|) iEdg (G) (1^{st} (A) (y)) = \{2^{nd} (A) (y), 2^{nd} (A) (y + 1)\} \to ((N = \|1^{st} (A)\| \land N = \|1^{st} (B)\|) \to (\forall y \in (0 ..^N) \{2^{nd} (A) (y), 2^{nd} (A) (y + 1)\} = \{2^{nd} (B) (y), 2^{nd} (B) (y + 1)\} \to \forall y \in (0 ..^N) iEdg (G) (1^{st} (B) (y)) = iEdg (G) (1^{st} (A) (y)))))$
67	66	com12	$⊢ \forall y \in (0 ..^\|1^{st} (A)\|) iEdg (G) (1^{st} (A) (y)) = \{2^{nd} (A) (y), 2^{nd} (A) (y + 1)\} \to ((1^{st} (B) \in Word dom iEdg (G) \land 2^{nd} (B) : (0 \dots \|1^{st} (B)\|) ⟶ Vtx (G) \land \forall y \in (0 ..^\|1^{st} (B)\|) iEdg (G) (1^{st} (B) (y)) = \{2^{nd} (B) (y), 2^{nd} (B) (y + 1)\}) \to ((N = \|1^{st} (A)\| \land N = \|1^{st} (B)\|) \to (\forall y \in (0 ..^N) \{2^{nd} (A) (y), 2^{nd} (A) (y + 1)\} = \{2^{nd} (B) (y), 2^{nd} (B) (y + 1)\} \to \forall y \in (0 ..^N) iEdg (G) (1^{st} (B) (y)) = iEdg (G) (1^{st} (A) (y)))))$
68	67	3ad2ant3	$⊢ (1^{st} (A) \in Word dom iEdg (G) \land 2^{nd} (A) : (0 \dots \|1^{st} (A)\|) ⟶ Vtx (G) \land \forall y \in (0 ..^\|1^{st} (A)\|) iEdg (G) (1^{st} (A) (y)) = \{2^{nd} (A) (y), 2^{nd} (A) (y + 1)\}) \to ((1^{st} (B) \in Word dom iEdg (G) \land 2^{nd} (B) : (0 \dots \|1^{st} (B)\|) ⟶ Vtx (G) \land \forall y \in (0 ..^\|1^{st} (B)\|) iEdg (G) (1^{st} (B) (y)) = \{2^{nd} (B) (y), 2^{nd} (B) (y + 1)\}) \to ((N = \|1^{st} (A)\| \land N = \|1^{st} (B)\|) \to (\forall y \in (0 ..^N) \{2^{nd} (A) (y), 2^{nd} (A) (y + 1)\} = \{2^{nd} (B) (y), 2^{nd} (B) (y + 1)\} \to \forall y \in (0 ..^N) iEdg (G) (1^{st} (B) (y)) = iEdg (G) (1^{st} (A) (y)))))$
69	68	imp	$⊢ ((1^{st} (A) \in Word dom iEdg (G) \land 2^{nd} (A) : (0 \dots \|1^{st} (A)\|) ⟶ Vtx (G) \land \forall y \in (0 ..^\|1^{st} (A)\|) iEdg (G) (1^{st} (A) (y)) = \{2^{nd} (A) (y), 2^{nd} (A) (y + 1)\}) \land (1^{st} (B) \in Word dom iEdg (G) \land 2^{nd} (B) : (0 \dots \|1^{st} (B)\|) ⟶ Vtx (G) \land \forall y \in (0 ..^\|1^{st} (B)\|) iEdg (G) (1^{st} (B) (y)) = \{2^{nd} (B) (y), 2^{nd} (B) (y + 1)\})) \to ((N = \|1^{st} (A)\| \land N = \|1^{st} (B)\|) \to (\forall y \in (0 ..^N) \{2^{nd} (A) (y), 2^{nd} (A) (y + 1)\} = \{2^{nd} (B) (y), 2^{nd} (B) (y + 1)\} \to \forall y \in (0 ..^N) iEdg (G) (1^{st} (B) (y)) = iEdg (G) (1^{st} (A) (y))))$
70	69	expd	$⊢ ((1^{st} (A) \in Word dom iEdg (G) \land 2^{nd} (A) : (0 \dots \|1^{st} (A)\|) ⟶ Vtx (G) \land \forall y \in (0 ..^\|1^{st} (A)\|) iEdg (G) (1^{st} (A) (y)) = \{2^{nd} (A) (y), 2^{nd} (A) (y + 1)\}) \land (1^{st} (B) \in Word dom iEdg (G) \land 2^{nd} (B) : (0 \dots \|1^{st} (B)\|) ⟶ Vtx (G) \land \forall y \in (0 ..^\|1^{st} (B)\|) iEdg (G) (1^{st} (B) (y)) = \{2^{nd} (B) (y), 2^{nd} (B) (y + 1)\})) \to (N = \|1^{st} (A)\| \to (N = \|1^{st} (B)\| \to (\forall y \in (0 ..^N) \{2^{nd} (A) (y), 2^{nd} (A) (y + 1)\} = \{2^{nd} (B) (y), 2^{nd} (B) (y + 1)\} \to \forall y \in (0 ..^N) iEdg (G) (1^{st} (B) (y)) = iEdg (G) (1^{st} (A) (y)))))$
71	70	a1i	$⊢ G \in USHGraph \to (((1^{st} (A) \in Word dom iEdg (G) \land 2^{nd} (A) : (0 \dots \|1^{st} (A)\|) ⟶ Vtx (G) \land \forall y \in (0 ..^\|1^{st} (A)\|) iEdg (G) (1^{st} (A) (y)) = \{2^{nd} (A) (y), 2^{nd} (A) (y + 1)\}) \land (1^{st} (B) \in Word dom iEdg (G) \land 2^{nd} (B) : (0 \dots \|1^{st} (B)\|) ⟶ Vtx (G) \land \forall y \in (0 ..^\|1^{st} (B)\|) iEdg (G) (1^{st} (B) (y)) = \{2^{nd} (B) (y), 2^{nd} (B) (y + 1)\})) \to (N = \|1^{st} (A)\| \to (N = \|1^{st} (B)\| \to (\forall y \in (0 ..^N) \{2^{nd} (A) (y), 2^{nd} (A) (y + 1)\} = \{2^{nd} (B) (y), 2^{nd} (B) (y + 1)\} \to \forall y \in (0 ..^N) iEdg (G) (1^{st} (B) (y)) = iEdg (G) (1^{st} (A) (y))))))$
72	40 45 71	syl2and	$⊢ G \in USHGraph \to ((A \in Walks (G) \land B \in Walks (G)) \to (N = \|1^{st} (A)\| \to (N = \|1^{st} (B)\| \to (\forall y \in (0 ..^N) \{2^{nd} (A) (y), 2^{nd} (A) (y + 1)\} = \{2^{nd} (B) (y), 2^{nd} (B) (y + 1)\} \to \forall y \in (0 ..^N) iEdg (G) (1^{st} (B) (y)) = iEdg (G) (1^{st} (A) (y))))))$
73	72	3imp1	$⊢ ((G \in USHGraph \land (A \in Walks (G) \land B \in Walks (G)) \land N = \|1^{st} (A)\|) \land N = \|1^{st} (B)\|) \to (\forall y \in (0 ..^N) \{2^{nd} (A) (y), 2^{nd} (A) (y + 1)\} = \{2^{nd} (B) (y), 2^{nd} (B) (y + 1)\} \to \forall y \in (0 ..^N) iEdg (G) (1^{st} (B) (y)) = iEdg (G) (1^{st} (A) (y)))$
74		eqcom	$⊢ iEdg (G) (1^{st} (B) (y)) = iEdg (G) (1^{st} (A) (y)) \leftrightarrow iEdg (G) (1^{st} (A) (y)) = iEdg (G) (1^{st} (B) (y))$
75	35	uspgrf1oedg	$⊢ G \in USHGraph \to iEdg (G) : dom iEdg (G) \underset{1-1 onto}{⟶} Edg (G)$
76		f1of1	$⊢ iEdg (G) : dom iEdg (G) \underset{1-1 onto}{⟶} Edg (G) \to iEdg (G) : dom iEdg (G) \underset{1-1}{⟶} Edg (G)$
77	75 76	syl	$⊢ G \in USHGraph \to iEdg (G) : dom iEdg (G) \underset{1-1}{⟶} Edg (G)$
78		eqidd	$⊢ G \in USHGraph \to iEdg (G) = iEdg (G)$
79		eqidd	$⊢ G \in USHGraph \to dom iEdg (G) = dom iEdg (G)$
80		edgval	$⊢ Edg (G) = ran iEdg (G)$
81	80	eqcomi	$⊢ ran iEdg (G) = Edg (G)$
82	81	a1i	$⊢ G \in USHGraph \to ran iEdg (G) = Edg (G)$
83	78 79 82	f1eq123d	$⊢ G \in USHGraph \to (iEdg (G) : dom iEdg (G) \underset{1-1}{⟶} ran iEdg (G) \leftrightarrow iEdg (G) : dom iEdg (G) \underset{1-1}{⟶} Edg (G))$
84	77 83	mpbird	$⊢ G \in USHGraph \to iEdg (G) : dom iEdg (G) \underset{1-1}{⟶} ran iEdg (G)$
85	84	3ad2ant1	$⊢ (G \in USHGraph \land (A \in Walks (G) \land B \in Walks (G)) \land N = \|1^{st} (A)\|) \to iEdg (G) : dom iEdg (G) \underset{1-1}{⟶} ran iEdg (G)$
86	85	adantr	$⊢ ((G \in USHGraph \land (A \in Walks (G) \land B \in Walks (G)) \land N = \|1^{st} (A)\|) \land N = \|1^{st} (B)\|) \to iEdg (G) : dom iEdg (G) \underset{1-1}{⟶} ran iEdg (G)$
87	34 35 36 37	wlkelwrd	$⊢ A \in Walks (G) \to (1^{st} (A) \in Word dom iEdg (G) \land 2^{nd} (A) : (0 \dots \|1^{st} (A)\|) ⟶ Vtx (G))$
88	34 35 41 42	wlkelwrd	$⊢ B \in Walks (G) \to (1^{st} (B) \in Word dom iEdg (G) \land 2^{nd} (B) : (0 \dots \|1^{st} (B)\|) ⟶ Vtx (G))$
89		oveq2	$⊢ N = \|1^{st} (A)\| \to (0 ..^N) = (0 ..^\|1^{st} (A)\|)$
90	89	eleq2d	$⊢ N = \|1^{st} (A)\| \to (y \in (0 ..^N) \leftrightarrow y \in (0 ..^\|1^{st} (A)\|))$
91		wrdsymbcl	$⊢ (1^{st} (A) \in Word dom iEdg (G) \land y \in (0 ..^\|1^{st} (A)\|)) \to 1^{st} (A) (y) \in dom iEdg (G)$
92	91	expcom	$⊢ y \in (0 ..^\|1^{st} (A)\|) \to (1^{st} (A) \in Word dom iEdg (G) \to 1^{st} (A) (y) \in dom iEdg (G))$
93	90 92	syl6bi	$⊢ N = \|1^{st} (A)\| \to (y \in (0 ..^N) \to (1^{st} (A) \in Word dom iEdg (G) \to 1^{st} (A) (y) \in dom iEdg (G)))$
94	93	adantr	$⊢ (N = \|1^{st} (A)\| \land N = \|1^{st} (B)\|) \to (y \in (0 ..^N) \to (1^{st} (A) \in Word dom iEdg (G) \to 1^{st} (A) (y) \in dom iEdg (G)))$
95	94	imp	$⊢ ((N = \|1^{st} (A)\| \land N = \|1^{st} (B)\|) \land y \in (0 ..^N)) \to (1^{st} (A) \in Word dom iEdg (G) \to 1^{st} (A) (y) \in dom iEdg (G))$
96	95	com12	$⊢ 1^{st} (A) \in Word dom iEdg (G) \to (((N = \|1^{st} (A)\| \land N = \|1^{st} (B)\|) \land y \in (0 ..^N)) \to 1^{st} (A) (y) \in dom iEdg (G))$
97	96	adantl	$⊢ (1^{st} (B) \in Word dom iEdg (G) \land 1^{st} (A) \in Word dom iEdg (G)) \to (((N = \|1^{st} (A)\| \land N = \|1^{st} (B)\|) \land y \in (0 ..^N)) \to 1^{st} (A) (y) \in dom iEdg (G))$
98		oveq2	$⊢ N = \|1^{st} (B)\| \to (0 ..^N) = (0 ..^\|1^{st} (B)\|)$
99	98	eleq2d	$⊢ N = \|1^{st} (B)\| \to (y \in (0 ..^N) \leftrightarrow y \in (0 ..^\|1^{st} (B)\|))$
100		wrdsymbcl	$⊢ (1^{st} (B) \in Word dom iEdg (G) \land y \in (0 ..^\|1^{st} (B)\|)) \to 1^{st} (B) (y) \in dom iEdg (G)$
101	100	expcom	$⊢ y \in (0 ..^\|1^{st} (B)\|) \to (1^{st} (B) \in Word dom iEdg (G) \to 1^{st} (B) (y) \in dom iEdg (G))$
102	99 101	syl6bi	$⊢ N = \|1^{st} (B)\| \to (y \in (0 ..^N) \to (1^{st} (B) \in Word dom iEdg (G) \to 1^{st} (B) (y) \in dom iEdg (G)))$
103	102	adantl	$⊢ (N = \|1^{st} (A)\| \land N = \|1^{st} (B)\|) \to (y \in (0 ..^N) \to (1^{st} (B) \in Word dom iEdg (G) \to 1^{st} (B) (y) \in dom iEdg (G)))$
104	103	imp	$⊢ ((N = \|1^{st} (A)\| \land N = \|1^{st} (B)\|) \land y \in (0 ..^N)) \to (1^{st} (B) \in Word dom iEdg (G) \to 1^{st} (B) (y) \in dom iEdg (G))$
105	104	com12	$⊢ 1^{st} (B) \in Word dom iEdg (G) \to (((N = \|1^{st} (A)\| \land N = \|1^{st} (B)\|) \land y \in (0 ..^N)) \to 1^{st} (B) (y) \in dom iEdg (G))$
106	105	adantr	$⊢ (1^{st} (B) \in Word dom iEdg (G) \land 1^{st} (A) \in Word dom iEdg (G)) \to (((N = \|1^{st} (A)\| \land N = \|1^{st} (B)\|) \land y \in (0 ..^N)) \to 1^{st} (B) (y) \in dom iEdg (G))$
107	97 106	jcad	$⊢ (1^{st} (B) \in Word dom iEdg (G) \land 1^{st} (A) \in Word dom iEdg (G)) \to (((N = \|1^{st} (A)\| \land N = \|1^{st} (B)\|) \land y \in (0 ..^N)) \to (1^{st} (A) (y) \in dom iEdg (G) \land 1^{st} (B) (y) \in dom iEdg (G)))$
108	107	ex	$⊢ 1^{st} (B) \in Word dom iEdg (G) \to (1^{st} (A) \in Word dom iEdg (G) \to (((N = \|1^{st} (A)\| \land N = \|1^{st} (B)\|) \land y \in (0 ..^N)) \to (1^{st} (A) (y) \in dom iEdg (G) \land 1^{st} (B) (y) \in dom iEdg (G))))$
109	108	adantr	$⊢ (1^{st} (B) \in Word dom iEdg (G) \land 2^{nd} (B) : (0 \dots \|1^{st} (B)\|) ⟶ Vtx (G)) \to (1^{st} (A) \in Word dom iEdg (G) \to (((N = \|1^{st} (A)\| \land N = \|1^{st} (B)\|) \land y \in (0 ..^N)) \to (1^{st} (A) (y) \in dom iEdg (G) \land 1^{st} (B) (y) \in dom iEdg (G))))$
110	109	com12	$⊢ 1^{st} (A) \in Word dom iEdg (G) \to ((1^{st} (B) \in Word dom iEdg (G) \land 2^{nd} (B) : (0 \dots \|1^{st} (B)\|) ⟶ Vtx (G)) \to (((N = \|1^{st} (A)\| \land N = \|1^{st} (B)\|) \land y \in (0 ..^N)) \to (1^{st} (A) (y) \in dom iEdg (G) \land 1^{st} (B) (y) \in dom iEdg (G))))$
111	110	adantr	$⊢ (1^{st} (A) \in Word dom iEdg (G) \land 2^{nd} (A) : (0 \dots \|1^{st} (A)\|) ⟶ Vtx (G)) \to ((1^{st} (B) \in Word dom iEdg (G) \land 2^{nd} (B) : (0 \dots \|1^{st} (B)\|) ⟶ Vtx (G)) \to (((N = \|1^{st} (A)\| \land N = \|1^{st} (B)\|) \land y \in (0 ..^N)) \to (1^{st} (A) (y) \in dom iEdg (G) \land 1^{st} (B) (y) \in dom iEdg (G))))$
112	111	imp	$⊢ ((1^{st} (A) \in Word dom iEdg (G) \land 2^{nd} (A) : (0 \dots \|1^{st} (A)\|) ⟶ Vtx (G)) \land (1^{st} (B) \in Word dom iEdg (G) \land 2^{nd} (B) : (0 \dots \|1^{st} (B)\|) ⟶ Vtx (G))) \to (((N = \|1^{st} (A)\| \land N = \|1^{st} (B)\|) \land y \in (0 ..^N)) \to (1^{st} (A) (y) \in dom iEdg (G) \land 1^{st} (B) (y) \in dom iEdg (G)))$
113	87 88 112	syl2an	$⊢ (A \in Walks (G) \land B \in Walks (G)) \to (((N = \|1^{st} (A)\| \land N = \|1^{st} (B)\|) \land y \in (0 ..^N)) \to (1^{st} (A) (y) \in dom iEdg (G) \land 1^{st} (B) (y) \in dom iEdg (G)))$
114	113	expd	$⊢ (A \in Walks (G) \land B \in Walks (G)) \to ((N = \|1^{st} (A)\| \land N = \|1^{st} (B)\|) \to (y \in (0 ..^N) \to (1^{st} (A) (y) \in dom iEdg (G) \land 1^{st} (B) (y) \in dom iEdg (G))))$
115	114	expd	$⊢ (A \in Walks (G) \land B \in Walks (G)) \to (N = \|1^{st} (A)\| \to (N = \|1^{st} (B)\| \to (y \in (0 ..^N) \to (1^{st} (A) (y) \in dom iEdg (G) \land 1^{st} (B) (y) \in dom iEdg (G)))))$
116	115	imp	$⊢ ((A \in Walks (G) \land B \in Walks (G)) \land N = \|1^{st} (A)\|) \to (N = \|1^{st} (B)\| \to (y \in (0 ..^N) \to (1^{st} (A) (y) \in dom iEdg (G) \land 1^{st} (B) (y) \in dom iEdg (G))))$
117	116	3adant1	$⊢ (G \in USHGraph \land (A \in Walks (G) \land B \in Walks (G)) \land N = \|1^{st} (A)\|) \to (N = \|1^{st} (B)\| \to (y \in (0 ..^N) \to (1^{st} (A) (y) \in dom iEdg (G) \land 1^{st} (B) (y) \in dom iEdg (G))))$
118	117	imp	$⊢ ((G \in USHGraph \land (A \in Walks (G) \land B \in Walks (G)) \land N = \|1^{st} (A)\|) \land N = \|1^{st} (B)\|) \to (y \in (0 ..^N) \to (1^{st} (A) (y) \in dom iEdg (G) \land 1^{st} (B) (y) \in dom iEdg (G)))$
119	118	imp	$⊢ (((G \in USHGraph \land (A \in Walks (G) \land B \in Walks (G)) \land N = \|1^{st} (A)\|) \land N = \|1^{st} (B)\|) \land y \in (0 ..^N)) \to (1^{st} (A) (y) \in dom iEdg (G) \land 1^{st} (B) (y) \in dom iEdg (G))$
120		f1veqaeq	$⊢ (iEdg (G) : dom iEdg (G) \underset{1-1}{⟶} ran iEdg (G) \land (1^{st} (A) (y) \in dom iEdg (G) \land 1^{st} (B) (y) \in dom iEdg (G))) \to (iEdg (G) (1^{st} (A) (y)) = iEdg (G) (1^{st} (B) (y)) \to 1^{st} (A) (y) = 1^{st} (B) (y))$
121	86 119 120	syl2an2r	$⊢ (((G \in USHGraph \land (A \in Walks (G) \land B \in Walks (G)) \land N = \|1^{st} (A)\|) \land N = \|1^{st} (B)\|) \land y \in (0 ..^N)) \to (iEdg (G) (1^{st} (A) (y)) = iEdg (G) (1^{st} (B) (y)) \to 1^{st} (A) (y) = 1^{st} (B) (y))$
122	74 121	syl5bi	$⊢ (((G \in USHGraph \land (A \in Walks (G) \land B \in Walks (G)) \land N = \|1^{st} (A)\|) \land N = \|1^{st} (B)\|) \land y \in (0 ..^N)) \to (iEdg (G) (1^{st} (B) (y)) = iEdg (G) (1^{st} (A) (y)) \to 1^{st} (A) (y) = 1^{st} (B) (y))$
123	122	ralimdva	$⊢ ((G \in USHGraph \land (A \in Walks (G) \land B \in Walks (G)) \land N = \|1^{st} (A)\|) \land N = \|1^{st} (B)\|) \to (\forall y \in (0 ..^N) iEdg (G) (1^{st} (B) (y)) = iEdg (G) (1^{st} (A) (y)) \to \forall y \in (0 ..^N) 1^{st} (A) (y) = 1^{st} (B) (y))$
124	32 73 123	3syld	$⊢ ((G \in USHGraph \land (A \in Walks (G) \land B \in Walks (G)) \land N = \|1^{st} (A)\|) \land N = \|1^{st} (B)\|) \to (\forall y \in (0 \dots N) 2^{nd} (A) (y) = 2^{nd} (B) (y) \to \forall y \in (0 ..^N) 1^{st} (A) (y) = 1^{st} (B) (y))$
125	124	expimpd	$⊢ (G \in USHGraph \land (A \in Walks (G) \land B \in Walks (G)) \land N = \|1^{st} (A)\|) \to ((N = \|1^{st} (B)\| \land \forall y \in (0 \dots N) 2^{nd} (A) (y) = 2^{nd} (B) (y)) \to \forall y \in (0 ..^N) 1^{st} (A) (y) = 1^{st} (B) (y))$
126	125	pm4.71d	$⊢ (G \in USHGraph \land (A \in Walks (G) \land B \in Walks (G)) \land N = \|1^{st} (A)\|) \to ((N = \|1^{st} (B)\| \land \forall y \in (0 \dots N) 2^{nd} (A) (y) = 2^{nd} (B) (y)) \leftrightarrow ((N = \|1^{st} (B)\| \land \forall y \in (0 \dots N) 2^{nd} (A) (y) = 2^{nd} (B) (y)) \land \forall y \in (0 ..^N) 1^{st} (A) (y) = 1^{st} (B) (y)))$
127	2 5 126	3bitr4d	$⊢ (G \in USHGraph \land (A \in Walks (G) \land B \in Walks (G)) \land N = \|1^{st} (A)\|) \to (A = B \leftrightarrow (N = \|1^{st} (B)\| \land \forall y \in (0 \dots N) 2^{nd} (A) (y) = 2^{nd} (B) (y)))$

Metamath Proof Explorer

Theorem uspgr2wlkeq

Proof