Theorem upgrimspths

Description: Graph isomorphisms between simple pseudographs map simple paths onto simple paths. (Contributed by AV, 31-Oct-2025)

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

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		upgrimspths.s	⊢ ( 𝜑 → 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 )
8		spthispth	⊢ ( 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 → 𝐹 ( Paths ‘ 𝐺 ) 𝑃 )
9		pthistrl	⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → 𝐹 ( Trails ‘ 𝐺 ) 𝑃 )
10	7 8 9	3syl	⊢ ( 𝜑 → 𝐹 ( Trails ‘ 𝐺 ) 𝑃 )
11	1 2 3 4 5 6 10	upgrimtrls	⊢ ( 𝜑 → 𝐸 ( Trails ‘ 𝐻 ) ( 𝑁 ∘ 𝑃 ) )
12		isspth	⊢ ( 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun ◡ 𝑃 ) )
13	12	simprbi	⊢ ( 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 → Fun ◡ 𝑃 )
14	7 13	syl	⊢ ( 𝜑 → Fun ◡ 𝑃 )
15		eqid	⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
16		eqid	⊢ ( Vtx ‘ 𝐻 ) = ( Vtx ‘ 𝐻 )
17	15 16	grimf1o	⊢ ( 𝑁 ∈ ( 𝐺 GraphIso 𝐻 ) → 𝑁 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) )
18		dff1o3	⊢ ( 𝑁 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) ↔ ( 𝑁 : ( Vtx ‘ 𝐺 ) –onto→ ( Vtx ‘ 𝐻 ) ∧ Fun ◡ 𝑁 ) )
19	18	simprbi	⊢ ( 𝑁 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) → Fun ◡ 𝑁 )
20	5 17 19	3syl	⊢ ( 𝜑 → Fun ◡ 𝑁 )
21		funco	⊢ ( ( Fun ◡ 𝑃 ∧ Fun ◡ 𝑁 ) → Fun ( ◡ 𝑃 ∘ ◡ 𝑁 ) )
22	14 20 21	syl2anc	⊢ ( 𝜑 → Fun ( ◡ 𝑃 ∘ ◡ 𝑁 ) )
23		cnvco	⊢ ◡ ( 𝑁 ∘ 𝑃 ) = ( ◡ 𝑃 ∘ ◡ 𝑁 )
24	23	funeqi	⊢ ( Fun ◡ ( 𝑁 ∘ 𝑃 ) ↔ Fun ( ◡ 𝑃 ∘ ◡ 𝑁 ) )
25	22 24	sylibr	⊢ ( 𝜑 → Fun ◡ ( 𝑁 ∘ 𝑃 ) )
26		isspth	⊢ ( 𝐸 ( SPaths ‘ 𝐻 ) ( 𝑁 ∘ 𝑃 ) ↔ ( 𝐸 ( Trails ‘ 𝐻 ) ( 𝑁 ∘ 𝑃 ) ∧ Fun ◡ ( 𝑁 ∘ 𝑃 ) ) )
27	11 25 26	sylanbrc	⊢ ( 𝜑 → 𝐸 ( SPaths ‘ 𝐻 ) ( 𝑁 ∘ 𝑃 ) )