upgrimtrlslem2

	Ref	Expression
Hypotheses	upgrimwlk.i	$⊢ I = iEdg (G)$
	upgrimwlk.j	$⊢ J = iEdg (H)$
	upgrimwlk.g	$⊢ φ \to G \in USHGraph$
	upgrimwlk.h	$⊢ φ \to H \in USHGraph$
	upgrimwlk.n	$⊢ φ \to N \in (G GraphIso H)$
	upgrimwlk.e	$⊢ E = (x \in dom F ⟼ J^{-1} (N [I (F (x))]))$
	upgrimtrls.t	$⊢ φ \to F Trails (G) P$
Assertion	upgrimtrlslem2	$⊢ (φ \land (x \in dom F \land y \in dom F)) \to (J^{-1} (N [I (F (x))]) = J^{-1} (N [I (F (y))]) \to x = y)$

Proof

Step	Hyp	Ref	Expression
1		upgrimwlk.i	$⊢ I = iEdg (G)$
2		upgrimwlk.j	$⊢ J = iEdg (H)$
3		upgrimwlk.g	$⊢ φ \to G \in USHGraph$
4		upgrimwlk.h	$⊢ φ \to H \in USHGraph$
5		upgrimwlk.n	$⊢ φ \to N \in (G GraphIso H)$
6		upgrimwlk.e	$⊢ E = (x \in dom F ⟼ J^{-1} (N [I (F (x))]))$
7		upgrimtrls.t	$⊢ φ \to F Trails (G) P$
8	2	uspgrf1oedg	$⊢ H \in USHGraph \to J : dom J \underset{1-1 onto}{⟶} Edg (H)$
9		f1of1	$⊢ J : dom J \underset{1-1 onto}{⟶} Edg (H) \to J : dom J \underset{1-1}{⟶} Edg (H)$
10	4 8 9	3syl	$⊢ φ \to J : dom J \underset{1-1}{⟶} Edg (H)$
11	1 2 3 4 5 6 7	upgrimtrlslem1	$⊢ (φ \land x \in dom F) \to N [I (F (x))] \in Edg (H)$
12		edgval	$⊢ Edg (H) = ran iEdg (H)$
13	2	eqcomi	$⊢ iEdg (H) = J$
14	13	rneqi	$⊢ ran iEdg (H) = ran J$
15	12 14	eqtri	$⊢ Edg (H) = ran J$
16	11 15	eleqtrdi	$⊢ (φ \land x \in dom F) \to N [I (F (x))] \in ran J$
17	1 2 3 4 5 6 7	upgrimtrlslem1	$⊢ (φ \land y \in dom F) \to N [I (F (y))] \in Edg (H)$
18	17 15	eleqtrdi	$⊢ (φ \land y \in dom F) \to N [I (F (y))] \in ran J$
19	16 18	anim12dan	$⊢ (φ \land (x \in dom F \land y \in dom F)) \to (N [I (F (x))] \in ran J \land N [I (F (y))] \in ran J)$
20		f1ocnvfvrneq	$⊢ (J : dom J \underset{1-1}{⟶} Edg (H) \land (N [I (F (x))] \in ran J \land N [I (F (y))] \in ran J)) \to (J^{-1} (N [I (F (x))]) = J^{-1} (N [I (F (y))]) \to N [I (F (x))] = N [I (F (y))])$
21	10 19 20	syl2an2r	$⊢ (φ \land (x \in dom F \land y \in dom F)) \to (J^{-1} (N [I (F (x))]) = J^{-1} (N [I (F (y))]) \to N [I (F (x))] = N [I (F (y))])$
22		eqid	$⊢ Vtx (G) = Vtx (G)$
23		eqid	$⊢ Vtx (H) = Vtx (H)$
24	22 23	grimf1o	$⊢ N \in (G GraphIso H) \to N : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H)$
25		f1of1	$⊢ N : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H) \to N : Vtx (G) \underset{1-1}{⟶} Vtx (H)$
26	5 24 25	3syl	$⊢ φ \to N : Vtx (G) \underset{1-1}{⟶} Vtx (H)$
27		uspgruhgr	$⊢ G \in USHGraph \to G \in UHGraph$
28	3 27	syl	$⊢ φ \to G \in UHGraph$
29		trliswlk	$⊢ F Trails (G) P \to F Walks (G) P$
30	1	wlkf	$⊢ F Walks (G) P \to F \in Word dom I$
31		wrdf	$⊢ F \in Word dom I \to F : (0 ..^\|F\|) ⟶ dom I$
32		id	$⊢ F : (0 ..^\|F\|) ⟶ dom I \to F : (0 ..^\|F\|) ⟶ dom I$
33	32	ffdmd	$⊢ F : (0 ..^\|F\|) ⟶ dom I \to F : dom F ⟶ dom I$
34	30 31 33	3syl	$⊢ F Walks (G) P \to F : dom F ⟶ dom I$
35	7 29 34	3syl	$⊢ φ \to F : dom F ⟶ dom I$
36	35	ffvelcdmda	$⊢ (φ \land x \in dom F) \to F (x) \in dom I$
37	22 1	uhgrss	$⊢ (G \in UHGraph \land F (x) \in dom I) \to I (F (x)) \subseteq Vtx (G)$
38	28 36 37	syl2an2r	$⊢ (φ \land x \in dom F) \to I (F (x)) \subseteq Vtx (G)$
39	35	ffvelcdmda	$⊢ (φ \land y \in dom F) \to F (y) \in dom I$
40	22 1	uhgrss	$⊢ (G \in UHGraph \land F (y) \in dom I) \to I (F (y)) \subseteq Vtx (G)$
41	28 39 40	syl2an2r	$⊢ (φ \land y \in dom F) \to I (F (y)) \subseteq Vtx (G)$
42	38 41	anim12dan	$⊢ (φ \land (x \in dom F \land y \in dom F)) \to (I (F (x)) \subseteq Vtx (G) \land I (F (y)) \subseteq Vtx (G))$
43		f1imaeq	$⊢ (N : Vtx (G) \underset{1-1}{⟶} Vtx (H) \land (I (F (x)) \subseteq Vtx (G) \land I (F (y)) \subseteq Vtx (G))) \to (N [I (F (x))] = N [I (F (y))] \leftrightarrow I (F (x)) = I (F (y)))$
44	26 42 43	syl2an2r	$⊢ (φ \land (x \in dom F \land y \in dom F)) \to (N [I (F (x))] = N [I (F (y))] \leftrightarrow I (F (x)) = I (F (y)))$
45	1	uspgrf1oedg	$⊢ G \in USHGraph \to I : dom I \underset{1-1 onto}{⟶} Edg (G)$
46		f1of1	$⊢ I : dom I \underset{1-1 onto}{⟶} Edg (G) \to I : dom I \underset{1-1}{⟶} Edg (G)$
47	3 45 46	3syl	$⊢ φ \to I : dom I \underset{1-1}{⟶} Edg (G)$
48	1	trlf1	$⊢ F Trails (G) P \to F : (0 ..^\|F\|) \underset{1-1}{⟶} dom I$
49		f1f	$⊢ F : (0 ..^\|F\|) \underset{1-1}{⟶} dom I \to F : (0 ..^\|F\|) ⟶ dom I$
50		fdm	$⊢ F : (0 ..^\|F\|) ⟶ dom I \to dom F = (0 ..^\|F\|)$
51	50	eqcomd	$⊢ F : (0 ..^\|F\|) ⟶ dom I \to (0 ..^\|F\|) = dom F$
52	49 51	syl	$⊢ F : (0 ..^\|F\|) \underset{1-1}{⟶} dom I \to (0 ..^\|F\|) = dom F$
53		f1eq2	$⊢ (0 ..^\|F\|) = dom F \to (F : (0 ..^\|F\|) \underset{1-1}{⟶} dom I \leftrightarrow F : dom F \underset{1-1}{⟶} dom I)$
54	53	biimpcd	$⊢ F : (0 ..^\|F\|) \underset{1-1}{⟶} dom I \to ((0 ..^\|F\|) = dom F \to F : dom F \underset{1-1}{⟶} dom I)$
55	52 54	mpd	$⊢ F : (0 ..^\|F\|) \underset{1-1}{⟶} dom I \to F : dom F \underset{1-1}{⟶} dom I$
56	7 48 55	3syl	$⊢ φ \to F : dom F \underset{1-1}{⟶} dom I$
57	47 56	jca	$⊢ φ \to (I : dom I \underset{1-1}{⟶} Edg (G) \land F : dom F \underset{1-1}{⟶} dom I)$
58		f1cofveqaeq	$⊢ ((I : dom I \underset{1-1}{⟶} Edg (G) \land F : dom F \underset{1-1}{⟶} dom I) \land (x \in dom F \land y \in dom F)) \to (I (F (x)) = I (F (y)) \to x = y)$
59	57 58	sylan	$⊢ (φ \land (x \in dom F \land y \in dom F)) \to (I (F (x)) = I (F (y)) \to x = y)$
60	44 59	sylbid	$⊢ (φ \land (x \in dom F \land y \in dom F)) \to (N [I (F (x))] = N [I (F (y))] \to x = y)$
61	21 60	syld	$⊢ (φ \land (x \in dom F \land y \in dom F)) \to (J^{-1} (N [I (F (x))]) = J^{-1} (N [I (F (y))]) \to x = y)$

Metamath Proof Explorer

Theorem upgrimtrlslem2

Proof