Theorem upgrimwlklem2

Description: Lemma 2 for upgrimwlk . (Contributed by AV, 25-Oct-2025)

	Ref	Expression
Hypotheses	upgrimwlk.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
	upgrimwlk.j	⊢ 𝐽 = ( iEdg ‘ 𝐻 )
	upgrimwlk.g	⊢ ( 𝜑 → 𝐺 ∈ USPGraph )
	upgrimwlk.h	⊢ ( 𝜑 → 𝐻 ∈ USPGraph )
	upgrimwlk.n	⊢ ( 𝜑 → 𝑁 ∈ ( 𝐺 GraphIso 𝐻 ) )
	upgrimwlk.e	⊢ 𝐸 = ( 𝑥 ∈ dom 𝐹 ↦ ( ◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) )
	upgrimwlk.f	⊢ ( 𝜑 → 𝐹 ∈ Word dom 𝐼 )
Assertion	upgrimwlklem2	⊢ ( 𝜑 → 𝐸 ∈ Word dom 𝐽 )

Proof

Step	Hyp	Ref	Expression
1		upgrimwlk.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
2		upgrimwlk.j	⊢ 𝐽 = ( iEdg ‘ 𝐻 )
3		upgrimwlk.g	⊢ ( 𝜑 → 𝐺 ∈ USPGraph )
4		upgrimwlk.h	⊢ ( 𝜑 → 𝐻 ∈ USPGraph )
5		upgrimwlk.n	⊢ ( 𝜑 → 𝑁 ∈ ( 𝐺 GraphIso 𝐻 ) )
6		upgrimwlk.e	⊢ 𝐸 = ( 𝑥 ∈ dom 𝐹 ↦ ( ◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) )
7		upgrimwlk.f	⊢ ( 𝜑 → 𝐹 ∈ Word dom 𝐼 )
8	4	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → 𝐻 ∈ USPGraph )
9	2	uspgrf1oedg	⊢ ( 𝐻 ∈ USPGraph → 𝐽 : dom 𝐽 –1-1-onto→ ( Edg ‘ 𝐻 ) )
10	8 9	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → 𝐽 : dom 𝐽 –1-1-onto→ ( Edg ‘ 𝐻 ) )
11		uspgruhgr	⊢ ( 𝐺 ∈ USPGraph → 𝐺 ∈ UHGraph )
12	3 11	syl	⊢ ( 𝜑 → 𝐺 ∈ UHGraph )
13		uspgruhgr	⊢ ( 𝐻 ∈ USPGraph → 𝐻 ∈ UHGraph )
14	4 13	syl	⊢ ( 𝜑 → 𝐻 ∈ UHGraph )
15	12 14	jca	⊢ ( 𝜑 → ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) )
16	15	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) )
17	5	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → 𝑁 ∈ ( 𝐺 GraphIso 𝐻 ) )
18	1	uhgrfun	⊢ ( 𝐺 ∈ UHGraph → Fun 𝐼 )
19	12 18	syl	⊢ ( 𝜑 → Fun 𝐼 )
20	19	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → Fun 𝐼 )
21		wrdf	⊢ ( 𝐹 ∈ Word dom 𝐼 → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐼 )
22	21	ffdmd	⊢ ( 𝐹 ∈ Word dom 𝐼 → 𝐹 : dom 𝐹 ⟶ dom 𝐼 )
23	7 22	syl	⊢ ( 𝜑 → 𝐹 : dom 𝐹 ⟶ dom 𝐼 )
24	23	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑥 ) ∈ dom 𝐼 )
25	1	iedgedg	⊢ ( ( Fun 𝐼 ∧ ( 𝐹 ‘ 𝑥 ) ∈ dom 𝐼 ) → ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ( Edg ‘ 𝐺 ) )
26	20 24 25	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ( Edg ‘ 𝐺 ) )
27		eqid	⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
28		eqid	⊢ ( Edg ‘ 𝐻 ) = ( Edg ‘ 𝐻 )
29	27 28	uhgrimedgi	⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ ( 𝑁 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ( Edg ‘ 𝐺 ) ) ) → ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∈ ( Edg ‘ 𝐻 ) )
30	16 17 26 29	syl12anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∈ ( Edg ‘ 𝐻 ) )
31		f1ocnvdm	⊢ ( ( 𝐽 : dom 𝐽 –1-1-onto→ ( Edg ‘ 𝐻 ) ∧ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∈ ( Edg ‘ 𝐻 ) ) → ( ◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) ∈ dom 𝐽 )
32	10 30 31	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → ( ◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) ∈ dom 𝐽 )
33	32 6	fmptd	⊢ ( 𝜑 → 𝐸 : dom 𝐹 ⟶ dom 𝐽 )
34	1 2 3 4 5 6 7	upgrimwlklem1	⊢ ( 𝜑 → ( ♯ ‘ 𝐸 ) = ( ♯ ‘ 𝐹 ) )
35	34	oveq2d	⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝐸 ) ) = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
36		iswrdb	⊢ ( 𝐹 ∈ Word dom 𝐼 ↔ 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐼 )
37		fdm	⊢ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐼 → dom 𝐹 = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
38	37	eqcomd	⊢ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐼 → ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = dom 𝐹 )
39	36 38	sylbi	⊢ ( 𝐹 ∈ Word dom 𝐼 → ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = dom 𝐹 )
40	7 39	syl	⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = dom 𝐹 )
41	35 40	eqtrd	⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝐸 ) ) = dom 𝐹 )
42	41	feq2d	⊢ ( 𝜑 → ( 𝐸 : ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ⟶ dom 𝐽 ↔ 𝐸 : dom 𝐹 ⟶ dom 𝐽 ) )
43	33 42	mpbird	⊢ ( 𝜑 → 𝐸 : ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ⟶ dom 𝐽 )
44		iswrdb	⊢ ( 𝐸 ∈ Word dom 𝐽 ↔ 𝐸 : ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ⟶ dom 𝐽 )
45	43 44	sylibr	⊢ ( 𝜑 → 𝐸 ∈ Word dom 𝐽 )